Changeset 1324 for src/LTL/semantics.ma
- Timestamp:
- Oct 7, 2011, 3:32:07 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/LTL/semantics.ma
r1312 r1324 35 35 axiom ltl_set_result: list val → state ltl_sem_params → res (state ltl_sem_params). 36 36 37 definition ltl_exec_extended: ∀globals. genv globals (ltl_params globals) → False → state ltl_sem_params → IO io_out io_in (trace × (state ltl_sem_params))37 definition ltl_exec_extended: ∀globals. genv globals (ltl_params globals) → False → label → state ltl_sem_params → IO io_out io_in (trace × (state ltl_sem_params)) 38 38 ≝ λglobals,ge,abs. ⊥. 39 39 @abs qed.
Note: See TracChangeset
for help on using the changeset viewer.