equal
deleted
inserted
replaced
4 Copyright 1996 TU Muenchen |
4 Copyright 1996 TU Muenchen |
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 (* global changes to simpset() and claset(), see also TLS.ML *) |
9 Delsimps (ex_simps @ all_simps); |
10 Delsimps (ex_simps @ all_simps); |
10 Delsimps [split_paired_Ex]; |
11 Delsimps [split_paired_Ex]; |
|
12 Addsimps [Let_def]; |
|
13 claset_ref() := claset() delSWrapper "split_all_tac"; |
11 |
14 |
12 val exec_rws = [executions_def,is_exec_frag_def]; |
15 val exec_rws = [executions_def,is_exec_frag_def]; |
13 |
16 |
14 |
17 |
15 |
18 |