equal
deleted
inserted
replaced
8 imports Sequence Automata |
8 imports Sequence Automata |
9 begin |
9 begin |
10 |
10 |
11 default_sort type |
11 default_sort type |
12 |
12 |
13 types |
13 type_synonym |
14 ('a,'s)pairs = "('a * 's) Seq" |
14 ('a,'s)pairs = "('a * 's) Seq" |
|
15 |
|
16 type_synonym |
15 ('a,'s)execution = "'s * ('a,'s)pairs" |
17 ('a,'s)execution = "'s * ('a,'s)pairs" |
|
18 |
|
19 type_synonym |
16 'a trace = "'a Seq" |
20 'a trace = "'a Seq" |
17 |
21 |
|
22 type_synonym |
18 ('a,'s)execution_module = "('a,'s)execution set * 'a signature" |
23 ('a,'s)execution_module = "('a,'s)execution set * 'a signature" |
|
24 |
|
25 type_synonym |
19 'a schedule_module = "'a trace set * 'a signature" |
26 'a schedule_module = "'a trace set * 'a signature" |
|
27 |
|
28 type_synonym |
20 'a trace_module = "'a trace set * 'a signature" |
29 'a trace_module = "'a trace set * 'a signature" |
21 |
30 |
22 consts |
31 consts |
23 |
32 |
24 (* Executions *) |
33 (* Executions *) |