Changeset 1071 for src/RTLabs/syntax.ma


Ignore:
Timestamp:
Jul 15, 2011, 2:40:40 PM (8 years ago)
Author:
mulligan
Message:

changes the specific form that the added proofs take to use None, not Some, hence removing the exitential

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/syntax.ma

    r1070 r1071  
    3535; f_stacksize : nat
    3636; f_graph     : graph statement
    37 ; f_entry     : Σl:label. ∃s. lookup ?? f_graph l = Some ? s
    38 ; f_exit      : Σl:label. ∃s. lookup ?? f_graph l = Some ? s
     37; f_entry     : Σl:label. lookup ?? f_graph l ≠ None ?
     38; f_exit      : Σl:label. lookup ?? f_graph l ≠ None ?
    3939}.
    4040
Note: See TracChangeset for help on using the changeset viewer.