--- a/src/HOLCF/IOA/meta_theory/SimCorrectness.ML Thu Mar 05 10:47:27 1998 +0100
+++ b/src/HOLCF/IOA/meta_theory/SimCorrectness.ML Fri Mar 06 15:19:29 1998 +0100
@@ -156,6 +156,7 @@
Lemma 1 :Traces coincide
------------------------------------------------------- *)
+Delsplits[expand_if];
goal thy
"!!f.[|is_simulation R C A; ext C = ext A|] ==> \
\ !s s'. reachable C s & is_exec_frag C (s,ex) & (s,s'): R --> \
@@ -178,6 +179,7 @@
rewrite_rule [Let_def] move_subprop4_sim]
setloop split_tac [expand_if] ) 1);
qed_spec_mp"traces_coincide_sim";
+Addsplits[expand_if];
(* ----------------------------------------------------------- *)