--- a/src/HOLCF/IOA/meta_theory/RefCorrectness.ML Mon Apr 27 16:46:56 1998 +0200
+++ b/src/HOLCF/IOA/meta_theory/RefCorrectness.ML Mon Apr 27 16:47:50 1998 +0200
@@ -129,7 +129,7 @@
(* ------------------------------------------------------
Lemma 1 :Traces coincide
------------------------------------------------------- *)
-Delsplits[expand_if];
+Delsplits[split_if];
goalw thy [corresp_ex_def]
"!!f.[|is_ref_map f C A; ext C = ext A|] ==> \
\ !s. reachable C s & is_exec_frag C (s,xs) --> \
@@ -144,9 +144,9 @@
by (eres_inst_tac [("x","y")] allE 1);
by (Asm_full_simp_tac 1);
by (asm_full_simp_tac (simpset() addsimps [move_subprop4]
- setloop split_tac [expand_if] ) 1);
+ addsplits [split_if]) 1);
qed"lemma_1";
-Addsplits[expand_if];
+Addsplits[split_if];
(* ------------------------------------------------------------------ *)
(* The following lemmata contribute to *)