Ignore:
Timestamp:
Aug 3, 2011, 1:04:49 PM (9 years ago)
Author:
campbell
Message:

Checkpoint labels work on branch again.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.3/id-lookup-branch/Cminor/syntax.ma

    r1096 r1097  
    129129] qed.
    130130
     131lemma 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
    131134(* Get labels from a Cminor statement. *)
    132135let rec labels_of (s:stmt) : list (identifier Label) ≝
Note: See TracChangeset for help on using the changeset viewer.