src/HOLCF/Pcpo.ML

         (rtac ub_rangeI 1),
         (strip_tac 1),
         (case_tac "x<i" 1),
         (res_inst_tac [("s","Y(i)"),("t","X(i)")] subst 1),
         (rtac sym 1),
-        (fast_tac HOL_cs 1),
+        (Fast_tac 1),
         (rtac is_ub_thelub 1),
         (resolve_tac prems 1),
         (res_inst_tac [("y","X(Suc(x))")] trans_less 1),
         (rtac (chain_mono RS mp) 1),
         (resolve_tac prems 1),

         (rtac antisym_less 1),
         (rtac lub_mono2 1),
         (REPEAT (resolve_tac prems 1)),
         (cut_facts_tac prems 1),
         (rtac lub_mono2 1),
-        (safe_tac HOL_cs),
-        (step_tac HOL_cs 1),
-        (safe_tac HOL_cs),
+        Safe_tac,
+        (Step_tac 1),
+        Safe_tac,
         (rtac sym 1),
-        (fast_tac HOL_cs 1)
+        (Fast_tac 1)
         ]);
 
 qed_goal "lub_mono3" thy "[|is_chain(Y::nat=>'a::cpo);is_chain(X);\
 \! i. ? j. Y(i)<< X(j)|]==> lub(range(Y))<<lub(range(X))"
  (fn prems =>

 (* ------------------------------------------------------------------------ *)
 (* usefull lemmas about UU                                                  *)
 (* ------------------------------------------------------------------------ *)
 
 val eq_UU_sym = prove_goal thy "(UU = x) = (x = UU)" (fn _ => [
-        fast_tac HOL_cs 1]);
+        Fast_tac 1]);
 
 qed_goal "eq_UU_iff" thy "(x=UU)=(x<<UU)"
  (fn prems =>
         [
         (rtac iffI 1),

 "[|? j.~Y(j)=UU;is_chain(Y::nat=>'a::pcpo)|]\
 \ ==> ? j.!i.j<i-->~Y(i)=UU"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
-        (safe_tac HOL_cs),
-        (step_tac HOL_cs 1),
+        Safe_tac,
+        (Step_tac 1),
         (strip_tac 1),
         (rtac notUU_I 1),
         (atac 2),
         (etac (chain_mono RS mp) 1),
         (atac 1)

  	(etac exE 1),
         (res_inst_tac [("x","i")] exI 1),
         (strip_tac 1),
         (dres_inst_tac [("x","i"),("y","j")] chain_mono 1),
         (etac (le_imp_less_or_eq RS disjE) 1),
-	(safe_tac HOL_cs),
+	Safe_tac,
 	(dtac (ax_flat RS spec RS spec RS mp) 1),
-	(fast_tac HOL_cs 1)
+	(Fast_tac 1)
         ]);
 
 (* flat subclass of chfin --> adm_flat not needed *)
 
 qed_goal "flat_eq" thy "(a::'a::flat) ~= UU ==> a << b = (a = b)"