# HG changeset patch
# User paulson
# Date 875526135 -7200
# Node ID 2543df678ab27309da8d3c23269dca0e0bab4ea1
# Parent  c7fa890d0d9213a4f5d56b8fd985fa96fcf7ac20
fast_tac HOL_cs -> Fast_tac, etc.

diff -r c7fa890d0d92 -r 2543df678ab2 src/HOLCF/Lift2.ML
--- a/src/HOLCF/Lift2.ML	Mon Sep 29 11:40:03 1997 +0200
+++ b/src/HOLCF/Lift2.ML	Mon Sep 29 11:42:15 1997 +0200
@@ -58,8 +58,8 @@
 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);
@@ -85,7 +85,7 @@
 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); 
@@ -112,9 +112,9 @@
 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);
diff -r c7fa890d0d92 -r 2543df678ab2 src/HOLCF/Pcpo.ML
--- a/src/HOLCF/Pcpo.ML	Mon Sep 29 11:40:03 1997 +0200
+++ b/src/HOLCF/Pcpo.ML	Mon Sep 29 11:42:15 1997 +0200
@@ -121,7 +121,7 @@
         (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),
@@ -146,11 +146,11 @@
         (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);\
@@ -175,7 +175,7 @@
 (* ------------------------------------------------------------------------ *)
 
 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 =>
@@ -261,8 +261,8 @@
  (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),
@@ -292,9 +292,9 @@
         (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 *)