Changeset 1097 for Deliverables/D3.3/id-lookup-branch/Cminor/syntax.ma
- Timestamp:
- Aug 3, 2011, 1:04:49 PM (10 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
Deliverables/D3.3/id-lookup-branch/Cminor/syntax.ma
r1096 r1097 129 129 ] qed. 130 130 131 lemma stmt_labels_mp : ∀P,Q. (∀l. P l → Q l) → ∀s. stmt_labels P s → stmt_labels Q s. 132 #P #Q #H #s elim s normalize /2/ qed. 133 131 134 (* Get labels from a Cminor statement. *) 132 135 let rec labels_of (s:stmt) : list (identifier Label) ≝
Note: See TracChangeset
for help on using the changeset viewer.