# HG changeset patch
# User oheimb
# Date 893172102 -7200
# Node ID b8a32ef742d99573c4527ceaa2d8c8c05ae61e09
# Parent  0277a026f99d9bcf9575d5a8673695d000a558b3
removed split_all_tac from claset() globally within IOA

diff -r 0277a026f99d -r b8a32ef742d9 src/HOLCF/IOA/NTP/Correctness.ML
--- 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,
diff -r 0277a026f99d -r b8a32ef742d9 src/HOLCF/IOA/meta_theory/TLS.ML
--- 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                          *)
diff -r 0277a026f99d -r b8a32ef742d9 src/HOLCF/IOA/meta_theory/Traces.ML
--- 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];