src/HOLCF/Lift2.ML

 (* Tailoring chain_mono2 of Pcpo.ML to Undef *)
 
 goal Lift2.thy
 "!!Y. [|? j.~Y(j)=Undef;is_chain(Y::nat=>('a)lift)|] \
 \ ==> ? j.!i.j<i-->~Y(i)=Undef";
-by (safe_tac HOL_cs);
-by (step_tac HOL_cs 1);
+by Safe_tac;
+by (Step_tac 1);
 by (strip_tac 1);
 by (rtac notUndef_I 1);
 by (atac 2);
 by (etac (chain_mono RS mp) 1);
 by (atac 1);

 by (etac spec 1); 
 
 by (subgoal_tac "!x y.x<<(y::('a)lift) --> x=Undef | x=y" 1);
 by (simp_tac (!simpset addsimps [inst_lift_po]) 2);
 by (rtac (chain_mono2_po RS exE) 1); 
-by (fast_tac HOL_cs 1); 
+by (Fast_tac 1); 
 by (atac 1); 
 by (res_inst_tac [("x","Suc(x)")] exI 1); 
 by (strip_tac 1); 
 by (rtac disjE 1); 
 by (atac 3); 

 (* Main Lemma: cpo_lift *)
 
 goal Lift2.thy  
   "!!Y. is_chain(Y::nat=>('a)lift) ==> ? x.range(Y) <<|x";
 by (cut_inst_tac [] flat_imp_chain_finite_poo 1);
-by (step_tac HOL_cs 1);
-by (safe_tac HOL_cs);
-by (step_tac HOL_cs 1); 
+by (Step_tac 1);
+by Safe_tac;
+by (Step_tac 1); 
 by (rtac exI 1);
 by (rtac lub_finch1 1);
 by (atac 1);
 by (atac 1);
 qed"cpo_lift";