|
Last change
on this file since 1624 was
1451,
checked in by sacerdot, 9 years ago
|
- All axioms in LIN/semantics.ma closed
- succ_pc and pointer_of_label moved to more_sem_params1; their type have
been changed too to implement LIN/semantics.ma
|
|
File size:
267 bytes
|
| Line | |
|---|
| 1 | include "LIN/joint_LTL_LIN_semantics.ma". |
|---|
| 2 | include "LTL/LTL.ma". (* CSC: syntax.ma in RTLabs *) |
|---|
| 3 | |
|---|
| 4 | definition 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
TracBrowser
for help on using the repository browser.
