--- a/src/HOLCF/IOA/meta_theory/SimCorrectness.ML Mon Apr 27 16:46:56 1998 +0200
+++ b/src/HOLCF/IOA/meta_theory/SimCorrectness.ML Mon Apr 27 16:47:50 1998 +0200
@@ -156,7 +156,7 @@
Lemma 1 :Traces coincide
------------------------------------------------------- *)
-Delsplits[expand_if];
+Delsplits[split_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 --> \
@@ -177,9 +177,9 @@
by (asm_full_simp_tac (simpset() addsimps
[rewrite_rule [Let_def] move_subprop5_sim,
rewrite_rule [Let_def] move_subprop4_sim]
- setloop split_tac [expand_if] ) 1);
+ addsplits [split_if]) 1);
qed_spec_mp"traces_coincide_sim";
-Addsplits[expand_if];
+Addsplits[split_if];
(* ----------------------------------------------------------- *)