Changeset 1451 for src/LTL/semantics.ma


Ignore:
Timestamp:
Oct 22, 2011, 4:18:11 AM (8 years ago)
Author:
sacerdot
Message:
  1. All axioms in LIN/semantics.ma closed
  2. succ_pc and pointer_of_label moved to more_sem_params1; their type have been changed too to implement LIN/semantics.ma
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/LTL/semantics.ma

    r1383 r1451  
    22include "LTL/LTL.ma". (* CSC: syntax.ma in RTLabs *)
    33
    4 definition ltl_fullexec
    5  ltl_lin_fullexec … (graph_succ_p …) pointer_of_label …
    6   (graph_fetch_statement … (ltl_lin_sem_params …)).
     4definition ltl_fullexec : fullexec io_out io_in
     5 ltl_lin_fullexec … graph_succ_p (graph_fetch_statement … (ltl_lin_sem_params …))
     6  (graph_pointer_of_label …).
Note: See TracChangeset for help on using the changeset viewer.