src/HOLCF/IOA/meta_theory/RefCorrectness.ML

 
 
 (* ------------------------------------------------------
                  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) --> \
 \            mk_trace C`xs = mk_trace A`(snd (corresp_ex A f (s,xs)))";
 

 by (forward_tac [reachable.reachable_n] 1);
 by (assume_tac 1);
 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              *)
 (*              TRACE INCLUSION Part 2: corresp_ex is execution       *)
 (* ------------------------------------------------------------------ *)