- Timestamp:
- Mar 26, 2013, 7:09:29 PM (8 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/LIN/joint_LTL_LIN_semantics.ma
r2956 r2969 34 34 axiom ltl_lin_fetch_external_args: external_function → state LTL_LIN_state → ℕ → res (list val). 35 35 axiom ltl_lin_set_result: list val → unit → state LTL_LIN_state → res (state LTL_LIN_state). 36 37 (* TODO (needs another bit to be added to hdw) *)38 axiom eval_ltl_lin_seq : ltl_lin_seq → state LTL_LIN_state → IO io_out io_in (state LTL_LIN_state).39 36 40 37 definition LTL_LIN_save_frame :
Note: See TracChangeset
for help on using the changeset viewer.