Changeset 1097 for Deliverables/D3.3/id-lookup-branch/Cminor/syntax.ma

Timestamp:

Aug 3, 2011, 1:04:49 PM (9 years ago)

Author:

campbell

Message:

Checkpoint labels work on branch again.

File:

• Deliverables/D3.3/id-lookup-branch/Cminor/syntax.ma (modified) (1 diff)

Deliverables/D3.3/id-lookup-branch/Cminor/syntax.ma

@@ -129 +129 @@
 ] qed.
 
+lemma stmt_labels_mp : ∀P,Q. (∀l. P l → Q l) → ∀s. stmt_labels P s → stmt_labels Q s.
+#P #Q #H #s elim s normalize /2/ qed.
+
 (* Get labels from a Cminor statement. *)
 let rec labels_of (s:stmt) : list (identifier Label) ≝