Ignore:
Timestamp:
Apr 3, 2013, 5:54:34 PM (7 years ago)
Author:
campbell
Message:

Tidy up recent work a little.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Cminor/toRTLabsCorrectness.ma

    r3063 r3081  
    122122| #r #tr #s' #ST #CL normalize in CL; destruct
    123123] qed.
     124
     125(* Build the simulation record for FEMeasurable.  Note that sim_call_label is
     126   made up of the single step for the call combined with a single step for the
     127   label. *)
    124128
    125129definition cminor_rtlabs_meas_sim : meas_sim ≝
Note: See TracChangeset for help on using the changeset viewer.