--- a/src/HOLCF/IOA/NTP/Correctness.ML Tue Apr 21 17:20:54 1998 +0200
+++ b/src/HOLCF/IOA/NTP/Correctness.ML Tue Apr 21 17:21:42 1998 +0200
@@ -6,6 +6,8 @@
The main correctness proof: Impl implements Spec
*)
+(* repeated from Traces.ML *)
+claset_ref() := claset() delSWrapper "split_all_tac";
val hom_ioas = [Spec.ioa_def, Spec.trans_def,
--- a/src/HOLCF/IOA/meta_theory/TLS.ML Tue Apr 21 17:20:54 1998 +0200
+++ b/src/HOLCF/IOA/meta_theory/TLS.ML Tue Apr 21 17:21:42 1998 +0200
@@ -6,6 +6,12 @@
Temporal Logic of Steps -- tailored for I/O automata
*)
+(* global changes to simpset() and claset(), repeated from Traces.ML *)
+Delsimps (ex_simps @ all_simps);
+Delsimps [split_paired_Ex];
+Addsimps [Let_def];
+claset_ref() := claset() delSWrapper "split_all_tac";
+
(* ---------------------------------------------------------------- *)
(* ex2seqC *)
--- a/src/HOLCF/IOA/meta_theory/Traces.ML Tue Apr 21 17:20:54 1998 +0200
+++ b/src/HOLCF/IOA/meta_theory/Traces.ML Tue Apr 21 17:21:42 1998 +0200
@@ -6,8 +6,11 @@
Theorems about Executions and Traces of I/O automata in HOLCF.
*)
+(* global changes to simpset() and claset(), see also TLS.ML *)
Delsimps (ex_simps @ all_simps);
Delsimps [split_paired_Ex];
+Addsimps [Let_def];
+claset_ref() := claset() delSWrapper "split_all_tac";
val exec_rws = [executions_def,is_exec_frag_def];