Ignore:
Timestamp:
Jan 29, 2013, 11:20:53 AM (8 years ago)
Author:
piccolo
Message:

main lemma of ERTLptr in place

File:
1 edited

Legend:

Unmodified
Added
Removed

  • src/ERTLptr/ERTLtoERTLptr.ma

    r2570 r2592  
    1616include "ERTLptr/ERTLptr.ma".
    1717include "joint/TranslateUtils.ma".
    18 
     18 
    1919definition translate_step_seq :
    2020∀globals.(joint_seq ERTL globals) → (joint_seq ERTLptr globals) ≝
Note: See TracChangeset for help on using the changeset viewer.