Ignore:
Timestamp:
Mar 1, 2013, 1:05:21 PM (7 years ago)
Author:
sacerdot
Message:

WARNING: this commit breaks things, sorry, Paolo is going to fix compiler.ma
in a minute...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/Measurable.ma

    r2727 r2756  
    2424definition trace_is_label_to_return : ∀C. list (cs_state … C × trace) → Prop ≝
    2525λC,x. ∃tr1,s1,x',tr2,s2. x = 〈s1,tr1〉::(x'@[〈s2,tr2〉]) ∧ bool_to_Prop (cs_labelled C s1) ∧ cs_classify C s2 = cl_return.
    26 
    27 (* For intensional_event; should separate out definition *)
    28 include "common/StatusSimulation.ma".
    2926
    3027definition intensional_event_of_event : event → list intensional_event ≝
Note: See TracChangeset for help on using the changeset viewer.