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];