| changeset 4536 | 74f7c556fd90 |
| parent 4477 | b3e5857d8d99 |
| child 4559 | 8e604d885b54 |
| 4535:f24cebc299e4 | 4536:74f7c556fd90 |
|---|---|
5 |
5 |
6 Theorems about Executions and Traces of I/O automata in HOLCF. |
6 Theorems about Executions and Traces of I/O automata in HOLCF. |
7 *) |
7 *) |
8 |
8 |
9 Delsimps (ex_simps @ all_simps); |
9 Delsimps (ex_simps @ all_simps); |
10 Delsimps [split_paired_Ex]; |
|
10 |
11 |
11 val exec_rws = [executions_def,is_exec_frag_def]; |
12 val exec_rws = [executions_def,is_exec_frag_def]; |
12 |
13 |
13 |
14 |
14 |
15 |