# HG changeset patch
# User paulson
# Date 878732626 -3600
# Node ID e534c4c32d54f35fbe16c086ac060555dcb8f484
# Parent  451104c223e2369855e0b46f0509451f7f32279f
Ran expandshort, especially to introduce Safe_tac

diff -r 451104c223e2 -r e534c4c32d54 src/HOL/Auth/Yahalom2.ML
--- a/src/HOL/Auth/Yahalom2.ML	Wed Nov 05 13:14:15 1997 +0100
+++ b/src/HOL/Auth/Yahalom2.ML	Wed Nov 05 13:23:46 1997 +0100
@@ -400,7 +400,7 @@
 \        ==> EX X. Says A B {|X, Crypt K (Nonce NB)|} : set evs";
 by (etac (Says_imp_spies RS parts.Inj RS MPair_parts) 1);
 by (dtac B_trusts_YM4_shrK 1);
-by (safe_tac (claset()));
+by Safe_tac;
 by (rtac lemma 1);
 by (rtac Spy_not_see_encrypted_key 2);
 by (REPEAT_FIRST assume_tac);
diff -r 451104c223e2 -r e534c4c32d54 src/HOL/AxClasses/Lattice/CLattice.ML
--- a/src/HOL/AxClasses/Lattice/CLattice.ML	Wed Nov 05 13:14:15 1997 +0100
+++ b/src/HOL/AxClasses/Lattice/CLattice.ML	Wed Nov 05 13:23:46 1997 +0100
@@ -7,46 +7,46 @@
 (* unique existence *)
 
 goalw thy [Inf_def] "is_Inf A (Inf A)";
-  br (ex_Inf RS spec RS selectI1) 1;
+  by (rtac (ex_Inf RS spec RS selectI1) 1);
 qed "Inf_is_Inf";
 
 goal thy "is_Inf A inf --> Inf A = inf";
-  br impI 1;
-  br (is_Inf_uniq RS mp) 1;
-  br conjI 1;
-  br Inf_is_Inf 1;
-  ba 1;
+  by (rtac impI 1);
+  by (rtac (is_Inf_uniq RS mp) 1);
+  by (rtac conjI 1);
+  by (rtac Inf_is_Inf 1);
+  by (assume_tac 1);
 qed "Inf_uniq";
 
 goalw thy [Ex1_def] "ALL A. EX! inf::'a::clattice. is_Inf A inf";
-  by (safe_tac (claset()));
+  by Safe_tac;
   by (Step_tac 1);
   by (Step_tac 1);
-  br Inf_is_Inf 1;
-  br (Inf_uniq RS mp RS sym) 1;
-  ba 1;
+  by (rtac Inf_is_Inf 1);
+  by (rtac (Inf_uniq RS mp RS sym) 1);
+  by (assume_tac 1);
 qed "ex1_Inf";
 
 
 goalw thy [Sup_def] "is_Sup A (Sup A)";
-  br (ex_Sup RS spec RS selectI1) 1;
+  by (rtac (ex_Sup RS spec RS selectI1) 1);
 qed "Sup_is_Sup";
 
 goal thy "is_Sup A sup --> Sup A = sup";
-  br impI 1;
-  br (is_Sup_uniq RS mp) 1;
-  br conjI 1;
-  br Sup_is_Sup 1;
-  ba 1;
+  by (rtac impI 1);
+  by (rtac (is_Sup_uniq RS mp) 1);
+  by (rtac conjI 1);
+  by (rtac Sup_is_Sup 1);
+  by (assume_tac 1);
 qed "Sup_uniq";
 
 goalw thy [Ex1_def] "ALL A. EX! sup::'a::clattice. is_Sup A sup";
-  by (safe_tac (claset()));
+  by Safe_tac;
   by (Step_tac 1);
   by (Step_tac 1);
-  br Sup_is_Sup 1;
-  br (Sup_uniq RS mp RS sym) 1;
-  ba 1;
+  by (rtac Sup_is_Sup 1);
+  by (rtac (Sup_uniq RS mp RS sym) 1);
+  by (assume_tac 1);
 qed "ex1_Sup";
 
 
@@ -54,68 +54,68 @@
 
 val prems = goalw thy [Inf_def] "x:A ==> Inf A [= x";
   by (cut_facts_tac prems 1);
-  br selectI2 1;
-  br Inf_is_Inf 1;
+  by (rtac selectI2 1);
+  by (rtac Inf_is_Inf 1);
   by (rewtac is_Inf_def);
   by (Fast_tac 1);
 qed "Inf_lb";
 
 val [prem] = goalw thy [Inf_def] "(!!x. x:A ==> z [= x) ==> z [= Inf A";
-  br selectI2 1;
-  br Inf_is_Inf 1;
+  by (rtac selectI2 1);
+  by (rtac Inf_is_Inf 1);
   by (rewtac is_Inf_def);
   by (Step_tac 1);
   by (Step_tac 1);
-  be mp 1;
-  br ballI 1;
-  be prem 1;
+  by (etac mp 1);
+  by (rtac ballI 1);
+  by (etac prem 1);
 qed "Inf_ub_lbs";
 
 
 val prems = goalw thy [Sup_def] "x:A ==> x [= Sup A";
   by (cut_facts_tac prems 1);
-  br selectI2 1;
-  br Sup_is_Sup 1;
+  by (rtac selectI2 1);
+  by (rtac Sup_is_Sup 1);
   by (rewtac is_Sup_def);
   by (Fast_tac 1);
 qed "Sup_ub";
 
 val [prem] = goalw thy [Sup_def] "(!!x. x:A ==> x [= z) ==> Sup A [= z";
-  br selectI2 1;
-  br Sup_is_Sup 1;
+  by (rtac selectI2 1);
+  by (rtac Sup_is_Sup 1);
   by (rewtac is_Sup_def);
   by (Step_tac 1);
   by (Step_tac 1);
-  be mp 1;
-  br ballI 1;
-  be prem 1;
+  by (etac mp 1);
+  by (rtac ballI 1);
+  by (etac prem 1);
 qed "Sup_lb_ubs";
 
 
 (** minorized Infs / majorized Sups **)
 
 goal thy "(x [= Inf A) = (ALL y:A. x [= y)";
-  br iffI 1;
+  by (rtac iffI 1);
   (*==>*)
-    br ballI 1;
-    br (le_trans RS mp) 1;
-    be conjI 1;
-    be Inf_lb 1;
+    by (rtac ballI 1);
+    by (rtac (le_trans RS mp) 1);
+    by (etac conjI 1);
+    by (etac Inf_lb 1);
   (*<==*)
-    br Inf_ub_lbs 1;
+    by (rtac Inf_ub_lbs 1);
     by (Fast_tac 1);
 qed "le_Inf_eq";
 
 goal thy "(Sup A [= x) = (ALL y:A. y [= x)";
-  br iffI 1;
+  by (rtac iffI 1);
   (*==>*)
-    br ballI 1;
-    br (le_trans RS mp) 1;
-    br conjI 1;
-    be Sup_ub 1;
-    ba 1;
+    by (rtac ballI 1);
+    by (rtac (le_trans RS mp) 1);
+    by (rtac conjI 1);
+    by (etac Sup_ub 1);
+    by (assume_tac 1);
   (*<==*)
-    br Sup_lb_ubs 1;
+    by (rtac Sup_lb_ubs 1);
     by (Fast_tac 1);
 qed "ge_Sup_eq";
 
@@ -124,60 +124,60 @@
 (** Subsets and limits **)
 
 goal thy "A <= B --> Inf B [= Inf A";
-  br impI 1;
+  by (rtac impI 1);
   by (stac le_Inf_eq 1);
   by (rewtac Ball_def);
-  by (safe_tac (claset()));
-  bd subsetD 1;
-  ba 1;
-  be Inf_lb 1;
+  by Safe_tac;
+  by (dtac subsetD 1);
+  by (assume_tac 1);
+  by (etac Inf_lb 1);
 qed "Inf_subset_antimon";
 
 goal thy "A <= B --> Sup A [= Sup B";
-  br impI 1;
+  by (rtac impI 1);
   by (stac ge_Sup_eq 1);
   by (rewtac Ball_def);
-  by (safe_tac (claset()));
-  bd subsetD 1;
-  ba 1;
-  be Sup_ub 1;
+  by Safe_tac;
+  by (dtac subsetD 1);
+  by (assume_tac 1);
+  by (etac Sup_ub 1);
 qed "Sup_subset_mon";
 
 
 (** singleton / empty limits **)
 
 goal thy "Inf {x} = x";
-  br (Inf_uniq RS mp) 1;
+  by (rtac (Inf_uniq RS mp) 1);
   by (rewtac is_Inf_def);
-  by (safe_tac (claset()));
-  br le_refl 1;
+  by Safe_tac;
+  by (rtac le_refl 1);
   by (Fast_tac 1);
 qed "sing_Inf_eq";
 
 goal thy "Sup {x} = x";
-  br (Sup_uniq RS mp) 1;
+  by (rtac (Sup_uniq RS mp) 1);
   by (rewtac is_Sup_def);
-  by (safe_tac (claset()));
-  br le_refl 1;
+  by Safe_tac;
+  by (rtac le_refl 1);
   by (Fast_tac 1);
 qed "sing_Sup_eq";
 
 
 goal thy "Inf {} = Sup {x. True}";
-  br (Inf_uniq RS mp) 1;
+  by (rtac (Inf_uniq RS mp) 1);
   by (rewtac is_Inf_def);
-  by (safe_tac (claset()));
-  br (sing_Sup_eq RS subst) 1;
+  by Safe_tac;
+  by (rtac (sing_Sup_eq RS subst) 1);
   back();
-  br (Sup_subset_mon RS mp) 1;
+  by (rtac (Sup_subset_mon RS mp) 1);
   by (Fast_tac 1);
 qed "empty_Inf_eq";
 
 goal thy "Sup {} = Inf {x. True}";
-  br (Sup_uniq RS mp) 1;
+  by (rtac (Sup_uniq RS mp) 1);
   by (rewtac is_Sup_def);
-  by (safe_tac (claset()));
-  br (sing_Inf_eq RS subst) 1;
-  br (Inf_subset_antimon RS mp) 1;
+  by Safe_tac;
+  by (rtac (sing_Inf_eq RS subst) 1);
+  by (rtac (Inf_subset_antimon RS mp) 1);
   by (Fast_tac 1);
 qed "empty_Sup_eq";
diff -r 451104c223e2 -r e534c4c32d54 src/HOL/AxClasses/Lattice/LatInsts.ML
--- a/src/HOL/AxClasses/Lattice/LatInsts.ML	Wed Nov 05 13:14:15 1997 +0100
+++ b/src/HOL/AxClasses/Lattice/LatInsts.ML	Wed Nov 05 13:23:46 1997 +0100
@@ -3,15 +3,15 @@
 
 
 goal thy "Inf {x, y} = x && y";
-  br (Inf_uniq RS mp) 1;
+  by (rtac (Inf_uniq RS mp) 1);
   by (stac bin_is_Inf_eq 1);
-  br inf_is_inf 1;
+  by (rtac inf_is_inf 1);
 qed "bin_Inf_eq";
 
 goal thy "Sup {x, y} = x || y";
-  br (Sup_uniq RS mp) 1;
+  by (rtac (Sup_uniq RS mp) 1);
   by (stac bin_is_Sup_eq 1);
-  br sup_is_sup 1;
+  by (rtac sup_is_sup 1);
 qed "bin_Sup_eq";
 
 
@@ -19,39 +19,39 @@
 (* Unions and limits *)
 
 goal thy "Inf (A Un B) = Inf A && Inf B";
-  br (Inf_uniq RS mp) 1;
+  by (rtac (Inf_uniq RS mp) 1);
   by (rewtac is_Inf_def);
-  by (safe_tac (claset()));
+  by Safe_tac;
 
-  br (conjI RS (le_trans RS mp)) 1;
-  br inf_lb1 1;
-  be Inf_lb 1;
+  by (rtac (conjI RS (le_trans RS mp)) 1);
+  by (rtac inf_lb1 1);
+  by (etac Inf_lb 1);
 
-  br (conjI RS (le_trans RS mp)) 1;
-  br inf_lb2 1;
-  be Inf_lb 1;
+  by (rtac (conjI RS (le_trans RS mp)) 1);
+  by (rtac inf_lb2 1);
+  by (etac Inf_lb 1);
 
   by (stac le_inf_eq 1);
-  br conjI 1;
-  br Inf_ub_lbs 1;
+  by (rtac conjI 1);
+  by (rtac Inf_ub_lbs 1);
   by (Fast_tac 1);
-  br Inf_ub_lbs 1;
+  by (rtac Inf_ub_lbs 1);
   by (Fast_tac 1);
 qed "Inf_Un_eq";
 
 goal thy "Inf (UN i:A. B i) = Inf {Inf (B i) |i. i:A}";
-  br (Inf_uniq RS mp) 1;
+  by (rtac (Inf_uniq RS mp) 1);
   by (rewtac is_Inf_def);
-  by (safe_tac (claset()));
+  by Safe_tac;
   (*level 3*)
-  br (conjI RS (le_trans RS mp)) 1;
-  be Inf_lb 2;
-  br (sing_Inf_eq RS subst) 1;
-  br (Inf_subset_antimon RS mp) 1;
+  by (rtac (conjI RS (le_trans RS mp)) 1);
+  by (etac Inf_lb 2);
+  by (rtac (sing_Inf_eq RS subst) 1);
+  by (rtac (Inf_subset_antimon RS mp) 1);
   by (Fast_tac 1);
   (*level 8*)
   by (stac le_Inf_eq 1);
-  by (safe_tac (claset()));
+  by Safe_tac;
   by (stac le_Inf_eq 1);
   by (Fast_tac 1);
 qed "Inf_UN_eq";
@@ -59,40 +59,40 @@
 
 
 goal thy "Sup (A Un B) = Sup A || Sup B";
-  br (Sup_uniq RS mp) 1;
+  by (rtac (Sup_uniq RS mp) 1);
   by (rewtac is_Sup_def);
-  by (safe_tac (claset()));
+  by Safe_tac;
 
-  br (conjI RS (le_trans RS mp)) 1;
-  be Sup_ub 1;
-  br sup_ub1 1;
+  by (rtac (conjI RS (le_trans RS mp)) 1);
+  by (etac Sup_ub 1);
+  by (rtac sup_ub1 1);
 
-  br (conjI RS (le_trans RS mp)) 1;
-  be Sup_ub 1;
-  br sup_ub2 1;
+  by (rtac (conjI RS (le_trans RS mp)) 1);
+  by (etac Sup_ub 1);
+  by (rtac sup_ub2 1);
 
   by (stac ge_sup_eq 1);
-  br conjI 1;
-  br Sup_lb_ubs 1;
+  by (rtac conjI 1);
+  by (rtac Sup_lb_ubs 1);
   by (Fast_tac 1);
-  br Sup_lb_ubs 1;
+  by (rtac Sup_lb_ubs 1);
   by (Fast_tac 1);
 qed "Sup_Un_eq";
 
 goal thy "Sup (UN i:A. B i) = Sup {Sup (B i) |i. i:A}";
-  br (Sup_uniq RS mp) 1;
+  by (rtac (Sup_uniq RS mp) 1);
   by (rewtac is_Sup_def);
-  by (safe_tac (claset()));
+  by Safe_tac;
   (*level 3*)
-  br (conjI RS (le_trans RS mp)) 1;
-  be Sup_ub 1;
-  br (sing_Sup_eq RS subst) 1;
+  by (rtac (conjI RS (le_trans RS mp)) 1);
+  by (etac Sup_ub 1);
+  by (rtac (sing_Sup_eq RS subst) 1);
   back();
-  br (Sup_subset_mon RS mp) 1;
+  by (rtac (Sup_subset_mon RS mp) 1);
   by (Fast_tac 1);
   (*level 8*)
   by (stac ge_Sup_eq 1);
-  by (safe_tac (claset()));
+  by Safe_tac;
   by (stac ge_Sup_eq 1);
   by (Fast_tac 1);
 qed "Sup_UN_eq";
diff -r 451104c223e2 -r e534c4c32d54 src/HOL/AxClasses/Lattice/LatMorph.ML
--- a/src/HOL/AxClasses/Lattice/LatMorph.ML	Wed Nov 05 13:14:15 1997 +0100
+++ b/src/HOL/AxClasses/Lattice/LatMorph.ML	Wed Nov 05 13:23:46 1997 +0100
@@ -5,49 +5,49 @@
 (** monotone functions vs. "&&"- / "||"-semi-morphisms **)
 
 goalw thy [is_mono_def] "is_mono f = (ALL x y. f (x && y) [= f x && f y)";
-  by (safe_tac (claset()));
+  by Safe_tac;
   (*==> (level 1)*)
     by (stac le_inf_eq 1);
-    br conjI 1;
+    by (rtac conjI 1);
     by (Step_tac 1);
     by (Step_tac 1);
-    be mp 1;
-    br inf_lb1 1;
+    by (etac mp 1);
+    by (rtac inf_lb1 1);
     by (Step_tac 1);
     by (Step_tac 1);
-    be mp 1;
-    br inf_lb2 1;
+    by (etac mp 1);
+    by (rtac inf_lb2 1);
   (*==> (level 11)*)
-    br (conjI RS (le_trans RS mp)) 1;
-    br inf_lb2 2;
+    by (rtac (conjI RS (le_trans RS mp)) 1);
+    by (rtac inf_lb2 2);
     by (subgoal_tac "x && y = x" 1);
-    be subst 1;
+    by (etac subst 1);
     by (Fast_tac 1);
     by (stac inf_connect 1);
-    ba 1;
+    by (assume_tac 1);
 qed "mono_inf_eq";
 
 goalw thy [is_mono_def] "is_mono f = (ALL x y. f x || f y [= f (x || y))";
-  by (safe_tac (claset()));
+  by Safe_tac;
   (*==> (level 1)*)
     by (stac ge_sup_eq 1);
-    br conjI 1;
+    by (rtac conjI 1);
     by (Step_tac 1);
     by (Step_tac 1);
-    be mp 1;
-    br sup_ub1 1;
+    by (etac mp 1);
+    by (rtac sup_ub1 1);
     by (Step_tac 1);
     by (Step_tac 1);
-    be mp 1;
-    br sup_ub2 1;
+    by (etac mp 1);
+    by (rtac sup_ub2 1);
   (*==> (level 11)*)
-    br (conjI RS (le_trans RS mp)) 1;
-    br sup_ub1 1;
+    by (rtac (conjI RS (le_trans RS mp)) 1);
+    by (rtac sup_ub1 1);
     by (subgoal_tac "x || y = y" 1);
-    be subst 1;
+    by (etac subst 1);
     by (Fast_tac 1);
     by (stac sup_connect 1);
-    ba 1;
+    by (assume_tac 1);
 qed "mono_sup_eq";
 
 
diff -r 451104c223e2 -r e534c4c32d54 src/HOL/AxClasses/Lattice/LatPreInsts.ML
--- a/src/HOL/AxClasses/Lattice/LatPreInsts.ML	Wed Nov 05 13:14:15 1997 +0100
+++ b/src/HOL/AxClasses/Lattice/LatPreInsts.ML	Wed Nov 05 13:23:46 1997 +0100
@@ -5,13 +5,13 @@
 (** complete lattices **)
 
 goal thy "is_inf x y (Inf {x, y})";
-  br (bin_is_Inf_eq RS subst) 1;
-  br Inf_is_Inf 1;
+  by (rtac (bin_is_Inf_eq RS subst) 1);
+  by (rtac Inf_is_Inf 1);
 qed "Inf_is_inf";
 
 goal thy "is_sup x y (Sup {x, y})";
-  br (bin_is_Sup_eq RS subst) 1;
-  br Sup_is_Sup 1;
+  by (rtac (bin_is_Sup_eq RS subst) 1);
+  by (rtac Sup_is_Sup 1);
 qed "Sup_is_sup";
 
 
@@ -22,13 +22,13 @@
 
 goalw thy [is_inf_def, le_prod_def] "is_inf p q (fst p && fst q, snd p && snd q)";
   by (Simp_tac 1);
-  by (safe_tac (claset()));
+  by Safe_tac;
   by (REPEAT_FIRST (fn i => resolve_tac [inf_lb1, inf_lb2, inf_ub_lbs] i ORELSE atac i));
 qed "prod_is_inf";
 
 goalw thy [is_sup_def, le_prod_def] "is_sup p q (fst p || fst q, snd p || snd q)";
   by (Simp_tac 1);
-  by (safe_tac (claset()));
+  by Safe_tac;
   by (REPEAT_FIRST (fn i => resolve_tac [sup_ub1, sup_ub2, sup_lb_ubs] i ORELSE atac i));
 qed "prod_is_sup";
 
@@ -36,18 +36,18 @@
 (* functions *)
 
 goalw thy [is_inf_def, le_fun_def] "is_inf f g (%x. f x && g x)";
-  by (safe_tac (claset()));
-  br inf_lb1 1;
-  br inf_lb2 1;
-  br inf_ub_lbs 1;
+  by Safe_tac;
+  by (rtac inf_lb1 1);
+  by (rtac inf_lb2 1);
+  by (rtac inf_ub_lbs 1);
   by (REPEAT_FIRST (Fast_tac));
 qed "fun_is_inf";
 
 goalw thy [is_sup_def, le_fun_def] "is_sup f g (%x. f x || g x)";
-  by (safe_tac (claset()));
-  br sup_ub1 1;
-  br sup_ub2 1;
-  br sup_lb_ubs 1;
+  by Safe_tac;
+  by (rtac sup_ub1 1);
+  by (rtac sup_ub2 1);
+  by (rtac sup_lb_ubs 1);
   by (REPEAT_FIRST (Fast_tac));
 qed "fun_is_sup";
 
@@ -57,20 +57,20 @@
 
 goalw thy [is_inf_def, le_dual_def] "is_inf x y (Abs_dual (Rep_dual x || Rep_dual y))";
   by (stac Abs_dual_inverse' 1);
-  by (safe_tac (claset()));
-  br sup_ub1 1;
-  br sup_ub2 1;
-  br sup_lb_ubs 1;
-  ba 1;
-  ba 1;
+  by Safe_tac;
+  by (rtac sup_ub1 1);
+  by (rtac sup_ub2 1);
+  by (rtac sup_lb_ubs 1);
+  by (assume_tac 1);
+  by (assume_tac 1);
 qed "dual_is_inf";
 
 goalw thy [is_sup_def, le_dual_def] "is_sup x y (Abs_dual (Rep_dual x && Rep_dual y))";
   by (stac Abs_dual_inverse' 1);
-  by (safe_tac (claset()));
-  br inf_lb1 1;
-  br inf_lb2 1;
-  br inf_ub_lbs 1;
-  ba 1;
-  ba 1;
+  by Safe_tac;
+  by (rtac inf_lb1 1);
+  by (rtac inf_lb2 1);
+  by (rtac inf_ub_lbs 1);
+  by (assume_tac 1);
+  by (assume_tac 1);
 qed "dual_is_sup";
diff -r 451104c223e2 -r e534c4c32d54 src/HOL/AxClasses/Lattice/Lattice.ML
--- a/src/HOL/AxClasses/Lattice/Lattice.ML	Wed Nov 05 13:14:15 1997 +0100
+++ b/src/HOL/AxClasses/Lattice/Lattice.ML	Wed Nov 05 13:23:46 1997 +0100
@@ -7,46 +7,46 @@
 (* unique existence *)
 
 goalw thy [inf_def] "is_inf x y (x && y)";
-  br (ex_inf RS spec RS spec RS selectI1) 1;
+  by (rtac (ex_inf RS spec RS spec RS selectI1) 1);
 qed "inf_is_inf";
 
 goal thy "is_inf x y inf --> x && y = inf";
-  br impI 1;
-  br (is_inf_uniq RS mp) 1;
-  br conjI 1;
-  br inf_is_inf 1;
-  ba 1;
+  by (rtac impI 1);
+  by (rtac (is_inf_uniq RS mp) 1);
+  by (rtac conjI 1);
+  by (rtac inf_is_inf 1);
+  by (assume_tac 1);
 qed "inf_uniq";
 
 goalw thy [Ex1_def] "ALL x y. EX! inf::'a::lattice. is_inf x y inf";
-  by (safe_tac (claset()));
+  by Safe_tac;
   by (Step_tac 1);
   by (Step_tac 1);
-  br inf_is_inf 1;
-  br (inf_uniq RS mp RS sym) 1;
-  ba 1;
+  by (rtac inf_is_inf 1);
+  by (rtac (inf_uniq RS mp RS sym) 1);
+  by (assume_tac 1);
 qed "ex1_inf";
 
 
 goalw thy [sup_def] "is_sup x y (x || y)";
-  br (ex_sup RS spec RS spec RS selectI1) 1;
+  by (rtac (ex_sup RS spec RS spec RS selectI1) 1);
 qed "sup_is_sup";
 
 goal thy "is_sup x y sup --> x || y = sup";
-  br impI 1;
-  br (is_sup_uniq RS mp) 1;
-  br conjI 1;
-  br sup_is_sup 1;
-  ba 1;
+  by (rtac impI 1);
+  by (rtac (is_sup_uniq RS mp) 1);
+  by (rtac conjI 1);
+  by (rtac sup_is_sup 1);
+  by (assume_tac 1);
 qed "sup_uniq";
 
 goalw thy [Ex1_def] "ALL x y. EX! sup::'a::lattice. is_sup x y sup";
-  by (safe_tac (claset()));
+  by Safe_tac;
   by (Step_tac 1);
   by (Step_tac 1);
-  br sup_is_sup 1;
-  br (sup_uniq RS mp RS sym) 1;
-  ba 1;
+  by (rtac sup_is_sup 1);
+  by (rtac (sup_uniq RS mp RS sym) 1);
+  by (assume_tac 1);
 qed "ex1_sup";
 
 
@@ -96,30 +96,30 @@
 (* the Connection Theorems: "[=" expressed via "&&" or "||" *)
 
 goal thy "(x && y = x) = (x [= y)";
-  br iffI 1;
+  by (rtac iffI 1);
   (*==>*)
-    be subst 1;
-    br inf_lb2 1;
+    by (etac subst 1);
+    by (rtac inf_lb2 1);
   (*<==*)
-    br (inf_uniq RS mp) 1;
+    by (rtac (inf_uniq RS mp) 1);
     by (rewtac is_inf_def);
     by (REPEAT_FIRST (rtac conjI));
-    br le_refl 1;
-    ba 1;
+    by (rtac le_refl 1);
+    by (assume_tac 1);
     by (Fast_tac 1);
 qed "inf_connect";
 
 goal thy "(x || y = y) = (x [= y)";
-  br iffI 1;
+  by (rtac iffI 1);
   (*==>*)
-    be subst 1;
-    br sup_ub1 1;
+    by (etac subst 1);
+    by (rtac sup_ub1 1);
   (*<==*)
-    br (sup_uniq RS mp) 1;
+    by (rtac (sup_uniq RS mp) 1);
     by (rewtac is_sup_def);
     by (REPEAT_FIRST (rtac conjI));
-    ba 1;
-    br le_refl 1;
+    by (assume_tac 1);
+    by (rtac le_refl 1);
     by (Fast_tac 1);
 qed "sup_connect";
 
@@ -127,37 +127,37 @@
 (* minorized infs / majorized sups *)
 
 goal thy "(x [= y && z) = (x [= y & x [= z)";
-  br iffI 1;
+  by (rtac iffI 1);
   (*==> (level 1)*)
     by (cut_facts_tac [inf_lb1, inf_lb2] 1);
-    br conjI 1;
-    br (le_trans RS mp) 1;
-    be conjI 1;
-    ba 1;
-    br (le_trans RS mp) 1;
-    be conjI 1;
-    ba 1;
+    by (rtac conjI 1);
+    by (rtac (le_trans RS mp) 1);
+    by (etac conjI 1);
+    by (assume_tac 1);
+    by (rtac (le_trans RS mp) 1);
+    by (etac conjI 1);
+    by (assume_tac 1);
   (*<== (level 9)*)
-    be conjE 1;
-    be inf_ub_lbs 1;
-    ba 1;
+    by (etac conjE 1);
+    by (etac inf_ub_lbs 1);
+    by (assume_tac 1);
 qed "le_inf_eq";
 
 goal thy "(x || y [= z) = (x [= z & y [= z)";
-  br iffI 1;
+  by (rtac iffI 1);
   (*==> (level 1)*)
     by (cut_facts_tac [sup_ub1, sup_ub2] 1);
-    br conjI 1;
-    br (le_trans RS mp) 1;
-    be conjI 1;
-    ba 1;
-    br (le_trans RS mp) 1;
-    be conjI 1;
-    ba 1;
+    by (rtac conjI 1);
+    by (rtac (le_trans RS mp) 1);
+    by (etac conjI 1);
+    by (assume_tac 1);
+    by (rtac (le_trans RS mp) 1);
+    by (etac conjI 1);
+    by (assume_tac 1);
   (*<== (level 9)*)
-    be conjE 1;
-    be sup_lb_ubs 1;
-    ba 1;
+    by (etac conjE 1);
+    by (etac sup_lb_ubs 1);
+    by (assume_tac 1);
 qed "ge_sup_eq";
 
 
@@ -175,8 +175,8 @@
   back();
   back();
   back();
-  br refl 2;
-  br (is_inf_assoc RS mp) 1;
+  by (rtac refl 2);
+  by (rtac (is_inf_assoc RS mp) 1);
   by (REPEAT_FIRST (rtac conjI));
   by (REPEAT_FIRST (rtac inf_is_inf));
 qed "inf_assoc";
@@ -191,8 +191,8 @@
   back();
   back();
   back();
-  br refl 2;
-  br (is_sup_assoc RS mp) 1;
+  by (rtac refl 2);
+  by (rtac (is_sup_assoc RS mp) 1);
   by (REPEAT_FIRST (rtac conjI));
   by (REPEAT_FIRST (rtac sup_is_sup));
 qed "sup_assoc";
@@ -202,12 +202,12 @@
 
 goalw thy [inf_def] "x && y = y && x";
   by (stac (is_inf_commut RS ext) 1);
-  br refl 1;
+  by (rtac refl 1);
 qed "inf_commut";
 
 goalw thy [sup_def] "x || y = y || x";
   by (stac (is_sup_commut RS ext) 1);
-  br refl 1;
+  by (rtac refl 1);
 qed "sup_commut";
 
 
@@ -215,12 +215,12 @@
 
 goal thy "x && x = x";
   by (stac inf_connect 1);
-  br le_refl 1;
+  by (rtac le_refl 1);
 qed "inf_idemp";
 
 goal thy "x || x = x";
   by (stac sup_connect 1);
-  br le_refl 1;
+  by (rtac le_refl 1);
 qed "sup_idemp";
 
 
@@ -229,12 +229,12 @@
 goal thy "x || (x && y) = x";
   by (stac sup_commut 1);
   by (stac sup_connect 1);
-  br inf_lb1 1;
+  by (rtac inf_lb1 1);
 qed "sup_inf_absorb";
 
 goal thy "x && (x || y) = x";
   by (stac inf_connect 1);
-  br sup_ub1 1;
+  by (rtac sup_ub1 1);
 qed "inf_sup_absorb";
 
 
@@ -243,27 +243,27 @@
 val prems = goal thy "[| a [= b; x [= y |] ==> a && x [= b && y";
   by (cut_facts_tac prems 1);
   by (stac le_inf_eq 1);
-  br conjI 1;
-  br (le_trans RS mp) 1;
-  br conjI 1;
-  br inf_lb1 1;
-  ba 1;
-  br (le_trans RS mp) 1;
-  br conjI 1;
-  br inf_lb2 1;
-  ba 1;
+  by (rtac conjI 1);
+  by (rtac (le_trans RS mp) 1);
+  by (rtac conjI 1);
+  by (rtac inf_lb1 1);
+  by (assume_tac 1);
+  by (rtac (le_trans RS mp) 1);
+  by (rtac conjI 1);
+  by (rtac inf_lb2 1);
+  by (assume_tac 1);
 qed "inf_mon";
 
 val prems = goal thy "[| a [= b; x [= y |] ==> a || x [= b || y";
   by (cut_facts_tac prems 1);
   by (stac ge_sup_eq 1);
-  br conjI 1;
-  br (le_trans RS mp) 1;
-  br conjI 1;
-  ba 1;
-  br sup_ub1 1;
-  br (le_trans RS mp) 1;
-  br conjI 1;
-  ba 1;
-  br sup_ub2 1;
+  by (rtac conjI 1);
+  by (rtac (le_trans RS mp) 1);
+  by (rtac conjI 1);
+  by (assume_tac 1);
+  by (rtac sup_ub1 1);
+  by (rtac (le_trans RS mp) 1);
+  by (rtac conjI 1);
+  by (assume_tac 1);
+  by (rtac sup_ub2 1);
 qed "sup_mon";
diff -r 451104c223e2 -r e534c4c32d54 src/HOL/AxClasses/Lattice/OrdDefs.ML
--- a/src/HOL/AxClasses/Lattice/OrdDefs.ML	Wed Nov 05 13:14:15 1997 +0100
+++ b/src/HOL/AxClasses/Lattice/OrdDefs.ML	Wed Nov 05 13:23:46 1997 +0100
@@ -7,47 +7,47 @@
 (* pairs *)
 
 goalw thy [le_prod_def] "x [= (x::'a::quasi_order*'b::quasi_order)";
-  br conjI 1;
-  br le_refl 1;
-  br le_refl 1;
+  by (rtac conjI 1);
+  by (rtac le_refl 1);
+  by (rtac le_refl 1);
 qed "le_prod_refl";
 
 goalw thy [le_prod_def] "x [= y & y [= z --> x [= (z::'a::quasi_order*'b::quasi_order)";
-  by (safe_tac (claset()));
-  be (conjI RS (le_trans RS mp)) 1;
-  ba 1;
-  be (conjI RS (le_trans RS mp)) 1;
-  ba 1;
+  by Safe_tac;
+  by (etac (conjI RS (le_trans RS mp)) 1);
+  by (assume_tac 1);
+  by (etac (conjI RS (le_trans RS mp)) 1);
+  by (assume_tac 1);
 qed "le_prod_trans";
 
 goalw thy [le_prod_def] "x [= y & y [= x --> x = (y::'a::partial_order*'b::partial_order)";
-  by (safe_tac (claset()));
+  by Safe_tac;
   by (stac Pair_fst_snd_eq 1);
-  br conjI 1;
-  be (conjI RS (le_antisym RS mp)) 1;
-  ba 1;
-  be (conjI RS (le_antisym RS mp)) 1;
-  ba 1;
+  by (rtac conjI 1);
+  by (etac (conjI RS (le_antisym RS mp)) 1);
+  by (assume_tac 1);
+  by (etac (conjI RS (le_antisym RS mp)) 1);
+  by (assume_tac 1);
 qed "le_prod_antisym";
 
 
 (* functions *)
 
 goalw thy [le_fun_def] "f [= (f::'a=>'b::quasi_order)";
-  br allI 1;
-  br le_refl 1;
+  by (rtac allI 1);
+  by (rtac le_refl 1);
 qed "le_fun_refl";
 
 goalw thy [le_fun_def] "f [= g & g [= h --> f [= (h::'a=>'b::quasi_order)";
-  by (safe_tac (claset()));
-  br (le_trans RS mp) 1;
+  by Safe_tac;
+  by (rtac (le_trans RS mp) 1);
   by (Fast_tac 1);
 qed "le_fun_trans";
 
 goalw thy [le_fun_def] "f [= g & g [= f --> f = (g::'a=>'b::partial_order)";
-  by (safe_tac (claset()));
-  br ext 1;
-  br (le_antisym RS mp) 1;
+  by Safe_tac;
+  by (rtac ext 1);
+  by (rtac (le_antisym RS mp) 1);
   by (Fast_tac 1);
 qed "le_fun_antisym";
 
@@ -57,32 +57,32 @@
 
 (*"'a dual" is even an isotype*)
 goal thy "Rep_dual (Abs_dual y) = y";
-  br Abs_dual_inverse 1;
+  by (rtac Abs_dual_inverse 1);
   by (rewtac dual_def);
   by (Fast_tac 1);
 qed "Abs_dual_inverse'";
 
 
 goalw thy [le_dual_def] "x [= (x::'a::quasi_order dual)";
-  br le_refl 1;
+  by (rtac le_refl 1);
 qed "le_dual_refl";
 
 goalw thy [le_dual_def] "x [= y & y [= z --> x [= (z::'a::quasi_order dual)";
   by (stac conj_commut 1);
-  br le_trans 1;
+  by (rtac le_trans 1);
 qed "le_dual_trans";
 
 goalw thy [le_dual_def] "x [= y & y [= x --> x = (y::'a::partial_order dual)";
-  by (safe_tac (claset()));
-  br (Rep_dual_inverse RS subst) 1;
-  br sym 1;
-  br (Rep_dual_inverse RS subst) 1;
-  br arg_cong 1;
+  by Safe_tac;
+  by (rtac (Rep_dual_inverse RS subst) 1);
+  by (rtac sym 1);
+  by (rtac (Rep_dual_inverse RS subst) 1);
+  by (rtac arg_cong 1);
   back();
-  be (conjI RS (le_antisym RS mp)) 1;
-  ba 1;
+  by (etac (conjI RS (le_antisym RS mp)) 1);
+  by (assume_tac 1);
 qed "le_dual_antisym";
 
 goalw thy [le_dual_def] "x [= y | y [= (x::'a::linear_order dual)";
-  br le_linear 1;
+  by (rtac le_linear 1);
 qed "le_dual_linear";
diff -r 451104c223e2 -r e534c4c32d54 src/HOL/AxClasses/Lattice/Order.ML
--- a/src/HOL/AxClasses/Lattice/Order.ML	Wed Nov 05 13:14:15 1997 +0100
+++ b/src/HOL/AxClasses/Lattice/Order.ML	Wed Nov 05 13:23:46 1997 +0100
@@ -45,70 +45,70 @@
 (* associativity *)
 
 goalw thy [is_inf_def] "is_inf x y xy & is_inf y z yz & is_inf xy z xyz --> is_inf x yz xyz";
-  by (safe_tac (claset()));
+  by Safe_tac;
   (*level 1*)
-    br (le_trans RS mp) 1;
-    be conjI 1;
-    ba 1;
+    by (rtac (le_trans RS mp) 1);
+    by (etac conjI 1);
+    by (assume_tac 1);
   (*level 4*)
     by (Step_tac 1);
     back();
-    be mp 1;
-    br conjI 1;
-    br (le_trans RS mp) 1;
-    be conjI 1;
-    ba 1;
-    ba 1;
+    by (etac mp 1);
+    by (rtac conjI 1);
+    by (rtac (le_trans RS mp) 1);
+    by (etac conjI 1);
+    by (assume_tac 1);
+    by (assume_tac 1);
   (*level 11*)
     by (Step_tac 1);
     back();
     back();
-    be mp 1;
-    br conjI 1;
+    by (etac mp 1);
+    by (rtac conjI 1);
     by (Step_tac 1);
-    be mp 1;
-    be conjI 1;
-    br (le_trans RS mp) 1;
-    be conjI 1;
-    ba 1;
-    br (le_trans RS mp) 1;
-    be conjI 1;
+    by (etac mp 1);
+    by (etac conjI 1);
+    by (rtac (le_trans RS mp) 1);
+    by (etac conjI 1);
+    by (assume_tac 1);
+    by (rtac (le_trans RS mp) 1);
+    by (etac conjI 1);
     back();     (* !! *)
-    ba 1;
+    by (assume_tac 1);
 qed "is_inf_assoc";
 
 
 goalw thy [is_sup_def] "is_sup x y xy & is_sup y z yz & is_sup xy z xyz --> is_sup x yz xyz";
-  by (safe_tac (claset()));
+  by Safe_tac;
   (*level 1*)
-    br (le_trans RS mp) 1;
-    be conjI 1;
-    ba 1;
+    by (rtac (le_trans RS mp) 1);
+    by (etac conjI 1);
+    by (assume_tac 1);
   (*level 4*)
     by (Step_tac 1);
     back();
-    be mp 1;
-    br conjI 1;
-    br (le_trans RS mp) 1;
-    be conjI 1;
-    ba 1;
-    ba 1;
+    by (etac mp 1);
+    by (rtac conjI 1);
+    by (rtac (le_trans RS mp) 1);
+    by (etac conjI 1);
+    by (assume_tac 1);
+    by (assume_tac 1);
   (*level 11*)
     by (Step_tac 1);
     back();
     back();
-    be mp 1;
-    br conjI 1;
+    by (etac mp 1);
+    by (rtac conjI 1);
     by (Step_tac 1);
-    be mp 1;
-    be conjI 1;
-    br (le_trans RS mp) 1;
-    be conjI 1;
+    by (etac mp 1);
+    by (etac conjI 1);
+    by (rtac (le_trans RS mp) 1);
+    by (etac conjI 1);
     back();     (* !! *)
-    ba 1;
-    br (le_trans RS mp) 1;
-    be conjI 1;
-    ba 1;
+    by (assume_tac 1);
+    by (rtac (le_trans RS mp) 1);
+    by (etac conjI 1);
+    by (assume_tac 1);
 qed "is_sup_assoc";
 
 
@@ -118,15 +118,15 @@
   by (stac expand_if 1);
   by (REPEAT_FIRST (resolve_tac [conjI, impI]));
   (*case "x [= y"*)
-    br le_refl 1;
-    ba 1;
+    by (rtac le_refl 1);
+    by (assume_tac 1);
     by (Fast_tac 1);
   (*case "~ x [= y"*)
-    br (le_linear RS disjE) 1;
-    ba 1;
-    be notE 1;
-    ba 1;
-    br le_refl 1;
+    by (rtac (le_linear RS disjE) 1);
+    by (assume_tac 1);
+    by (etac notE 1);
+    by (assume_tac 1);
+    by (rtac le_refl 1);
     by (Fast_tac 1);
 qed "min_is_inf";
 
@@ -134,15 +134,15 @@
   by (stac expand_if 1);
   by (REPEAT_FIRST (resolve_tac [conjI, impI]));
   (*case "x [= y"*)
-    ba 1;
-    br le_refl 1;
+    by (assume_tac 1);
+    by (rtac le_refl 1);
     by (Fast_tac 1);
   (*case "~ x [= y"*)
-    br le_refl 1;
-    br (le_linear RS disjE) 1;
-    ba 1;
-    be notE 1;
-    ba 1;
+    by (rtac le_refl 1);
+    by (rtac (le_linear RS disjE) 1);
+    by (assume_tac 1);
+    by (etac notE 1);
+    by (assume_tac 1);
     by (Fast_tac 1);
 qed "max_is_sup";
 
@@ -151,23 +151,23 @@
 (** general vs. binary limits **)
 
 goalw thy [is_inf_def, is_Inf_def] "is_Inf {x, y} inf = is_inf x y inf";
-  br iffI 1;
+  by (rtac iffI 1);
   (*==>*)
     by (Fast_tac 1);
   (*<==*)
-    by (safe_tac (claset()));
+    by Safe_tac;
     by (Step_tac 1);
-    be mp 1;
+    by (etac mp 1);
     by (Fast_tac 1);
 qed "bin_is_Inf_eq";
 
 goalw thy [is_sup_def, is_Sup_def] "is_Sup {x, y} sup = is_sup x y sup";
-  br iffI 1;
+  by (rtac iffI 1);
   (*==>*)
     by (Fast_tac 1);
   (*<==*)
-    by (safe_tac (claset()));
+    by Safe_tac;
     by (Step_tac 1);
-    be mp 1;
+    by (etac mp 1);
     by (Fast_tac 1);
 qed "bin_is_Sup_eq";
diff -r 451104c223e2 -r e534c4c32d54 src/HOL/Finite.ML
--- a/src/HOL/Finite.ML	Wed Nov 05 13:14:15 1997 +0100
+++ b/src/HOL/Finite.ML	Wed Nov 05 13:23:46 1997 +0100
@@ -154,8 +154,8 @@
 
 val [prem] = goal Finite.thy
  "finite A ==> (!a:A. finite(B a)) --> finite(UN a:A. B a)";
-br (prem RS finite_induct) 1;
-by(ALLGOALS Asm_simp_tac);
+by (rtac (prem RS finite_induct) 1);
+by (ALLGOALS Asm_simp_tac);
 bind_thm("finite_UnionI", ballI RSN (2, result() RS mp));
 Addsimps [finite_UnionI];
 
@@ -163,7 +163,7 @@
 
 goalw Finite.thy [Sigma_def]
  "!!A. [| finite A; !a:A. finite(B a) |] ==> finite(SIGMA a:A. B a)";
-by(blast_tac (claset() addSIs [finite_UnionI]) 1);
+by (blast_tac (claset() addSIs [finite_UnionI]) 1);
 bind_thm("finite_SigmaI", ballI RSN (2,result()));
 Addsimps [finite_SigmaI];
 
@@ -250,15 +250,15 @@
 by (etac equalityE 1);
 by (asm_full_simp_tac
      (simpset() addsimps [subset_insert,Collect_conv_insert, less_Suc_eq]) 1);
-by (safe_tac (claset()));
+by Safe_tac;
   by (Asm_full_simp_tac 1);
   by (res_inst_tac [("x","%i. if f i = f m then a else f i")] exI 1);
-  by (SELECT_GOAL(safe_tac (claset()))1);
+  by (SELECT_GOAL Safe_tac 1);
    by (subgoal_tac "x ~= f m" 1);
     by (Blast_tac 2);
    by (subgoal_tac "? k. f k = x & k<m" 1);
     by (Blast_tac 2);
-   by (SELECT_GOAL(safe_tac (claset()))1);
+   by (SELECT_GOAL Safe_tac 1);
    by (res_inst_tac [("x","k")] exI 1);
    by (Asm_simp_tac 1);
   by (simp_tac (simpset() addsplits [expand_if]) 1);
@@ -267,18 +267,18 @@
  by (rotate_tac ~1 1);
  by (Asm_full_simp_tac 1);
  by (res_inst_tac [("x","%i. if f i = f m then a else f i")] exI 1);
- by (SELECT_GOAL(safe_tac (claset()))1);
+ by (SELECT_GOAL Safe_tac 1);
   by (subgoal_tac "x ~= f m" 1);
    by (Blast_tac 2);
   by (subgoal_tac "? k. f k = x & k<m" 1);
    by (Blast_tac 2);
-  by (SELECT_GOAL(safe_tac (claset()))1);
+  by (SELECT_GOAL Safe_tac 1);
   by (res_inst_tac [("x","k")] exI 1);
   by (Asm_simp_tac 1);
  by (simp_tac (simpset() addsplits [expand_if]) 1);
  by (Blast_tac 1);
 by (res_inst_tac [("x","%j. if f j = f i then f m else f j")] exI 1);
-by (SELECT_GOAL(safe_tac (claset()))1);
+by (SELECT_GOAL Safe_tac 1);
  by (subgoal_tac "x ~= f i" 1);
   by (Blast_tac 2);
  by (case_tac "x = f m" 1);
@@ -286,7 +286,7 @@
   by (Asm_simp_tac 1);
  by (subgoal_tac "? k. f k = x & k<m" 1);
   by (Blast_tac 2);
- by (SELECT_GOAL(safe_tac (claset()))1);
+ by (SELECT_GOAL Safe_tac 1);
  by (res_inst_tac [("x","k")] exI 1);
  by (Asm_simp_tac 1);
 by (simp_tac (simpset() addsplits [expand_if]) 1);
@@ -335,7 +335,7 @@
 by (Clarify_tac 1);
 by (case_tac "x:B" 1);
  by (dres_inst_tac [("A","B")] mk_disjoint_insert 1);
- by (SELECT_GOAL(safe_tac (claset()))1);
+ by (SELECT_GOAL Safe_tac 1);
  by (rotate_tac ~1 1);
  by (asm_full_simp_tac (simpset() addsimps [subset_insert_iff,finite_subset]) 1);
 by (rotate_tac ~1 1);
diff -r 451104c223e2 -r e534c4c32d54 src/HOL/Hoare/Examples.ML
--- a/src/HOL/Hoare/Examples.ML	Wed Nov 05 13:14:15 1997 +0100
+++ b/src/HOL/Hoare/Examples.ML	Wed Nov 05 13:23:46 1997 +0100
@@ -36,7 +36,7 @@
 
 by (hoare_tac 1);
 (*Now prove the verification conditions*)
-by (safe_tac (claset()));
+by Safe_tac;
 by (etac less_imp_diff_positive 1);
 by (asm_simp_tac (simpset() addsimps [less_imp_le, gcd_diff_r]) 1);
 by (asm_full_simp_tac (simpset() addsimps [not_less_iff_le, gcd_diff_l]) 2);
@@ -67,7 +67,7 @@
 
 by (simp_tac ((simpset_of Arith.thy) addsimps [pow_0]) 3);
 
-by (safe_tac (claset()));
+by Safe_tac;
 
 by (subgoal_tac "a*a=a pow 2" 1);
 by (Asm_simp_tac 1);
@@ -103,7 +103,7 @@
 \ {b = fac A}";
 
 by (hoare_tac 1);
-by (safe_tac (claset()));
+by Safe_tac;
 by (res_inst_tac [("n","a")] natE 1);
 by (ALLGOALS
     (asm_simp_tac
diff -r 451104c223e2 -r e534c4c32d54 src/HOL/Hoare/List_Examples.ML
--- a/src/HOL/Hoare/List_Examples.ML	Wed Nov 05 13:14:15 1997 +0100
+++ b/src/HOL/Hoare/List_Examples.ML	Wed Nov 05 13:23:46 1997 +0100
@@ -8,7 +8,7 @@
 \{y=rev(X)}";
 by (hoare_tac 1);
 by (asm_full_simp_tac (simpset() addsimps [neq_Nil_conv]) 1);
-by (safe_tac (claset()));
+by Safe_tac;
 by (Asm_full_simp_tac 1);
 by (Asm_full_simp_tac 1);
 qed "imperative_reverse";
@@ -23,7 +23,7 @@
 \{y = X@Y}";
 by (hoare_tac 1);
 by (asm_full_simp_tac (simpset() addsimps [neq_Nil_conv]) 1);
-by (safe_tac (claset()));
+by Safe_tac;
 by (Asm_full_simp_tac 1);
 by (Asm_full_simp_tac 1);
 qed "imperative_append";
diff -r 451104c223e2 -r e534c4c32d54 src/HOL/IMP/Hoare.ML
--- a/src/HOL/IMP/Hoare.ML	Wed Nov 05 13:14:15 1997 +0100
+++ b/src/HOL/IMP/Hoare.ML	Wed Nov 05 13:23:46 1997 +0100
@@ -71,7 +71,7 @@
 by (rtac iffI 1);
  by (rtac weak_coinduct 1);
   by (etac CollectI 1);
- by (safe_tac (claset()));
+ by Safe_tac;
   by (rotate_tac ~1 1);
   by (Asm_full_simp_tac 1);
  by (rotate_tac ~1 1);
diff -r 451104c223e2 -r e534c4c32d54 src/HOL/IMP/Transition.ML
--- a/src/HOL/IMP/Transition.ML	Wed Nov 05 13:14:15 1997 +0100
+++ b/src/HOL/IMP/Transition.ML	Wed Nov 05 13:23:46 1997 +0100
@@ -87,7 +87,7 @@
 
 (* ASSIGN *)
 by (fast_tac (claset() addSDs [hlemma]  addSEs [rel_pow_E2]
-                      addss simpset()) 1);
+                       addss simpset()) 1);
 
 (* SEMI *)
 by (fast_tac (claset() addSDs [lemma2,rel_pow_imp_rtrancl]) 1);
@@ -98,8 +98,7 @@
 by (fast_tac (claset() addSDs [rel_pow_imp_rtrancl]) 1);
 
 (* WHILE, induction on the length of the computation *)
-by (rotate_tac 1 1);
-by (etac rev_mp 1);
+by (eres_inst_tac [("P","?X -n-> ?Y")] rev_mp 1);
 by (res_inst_tac [("x","s")] spec 1);
 by (res_inst_tac [("n","n")] less_induct 1);
 by (strip_tac 1);
diff -r 451104c223e2 -r e534c4c32d54 src/HOL/IOA/IOA.ML
--- a/src/HOL/IOA/IOA.ML	Wed Nov 05 13:14:15 1997 +0100
+++ b/src/HOL/IOA/IOA.ML	Wed Nov 05 13:23:46 1997 +0100
@@ -55,7 +55,7 @@
 goalw IOA.thy (reachable_def::exec_rws)
 "!!A. [| reachable A s; (s,a,t) : trans_of(A) |] ==> reachable A t";
   by (asm_full_simp_tac (simpset() delsimps bex_simps) 1);
-  by (safe_tac (claset()));
+  by Safe_tac;
   by (res_inst_tac [("x","(%i. if i<n then fst ex i                    \
 \                            else (if i=n then Some a else None),    \
 \                         %i. if i<Suc n then snd ex i else t)")] bexI 1);
@@ -77,13 +77,13 @@
 \     !!s t a. [|reachable A s; P(s)|] ==> (s,a,t): trans_of(A) --> P(t) |] \
 \  ==> invariant A P";
   by (rewrite_goals_tac(reachable_def::Let_def::exec_rws));
-  by (safe_tac (claset()));
+  by Safe_tac;
   by (res_inst_tac [("Q","reachable A (snd ex n)")] conjunct1 1);
   by (nat_ind_tac "n" 1);
   by (fast_tac (claset() addIs [p1,reachable_0]) 1);
   by (eres_inst_tac[("x","n")]allE 1);
   by (exhaust_tac "fst ex n" 1 THEN ALLGOALS Asm_full_simp_tac);
-  by (safe_tac (claset()));
+  by Safe_tac;
   by (etac (p2 RS mp) 1);
   by (ALLGOALS(fast_tac(claset() addDs [reachable_n])));
 qed "invariantI";
diff -r 451104c223e2 -r e534c4c32d54 src/HOL/IOA/Solve.ML
--- a/src/HOL/IOA/Solve.ML	Wed Nov 05 13:14:15 1997 +0100
+++ b/src/HOL/IOA/Solve.ML	Wed Nov 05 13:23:46 1997 +0100
@@ -15,7 +15,7 @@
 \          is_weak_pmap f C A |] ==> traces(C) <= traces(A)";
 
   by (simp_tac(simpset() addsimps [has_trace_def])1);
-  by (safe_tac (claset()));
+  by Safe_tac;
 
   (* choose same trace, therefore same NF *)
   by (res_inst_tac[("x","mk_trace  C (fst ex)")] exI 1);
@@ -32,7 +32,7 @@
 
   (* Now show that it's an execution *)
   by (asm_full_simp_tac(simpset() addsimps [executions_def]) 1);
-  by (safe_tac (claset()));
+  by Safe_tac;
 
   (* Start states map to start states *)
   by (dtac bspec 1);
@@ -40,7 +40,7 @@
 
   (* Show that it's an execution fragment *)
   by (asm_full_simp_tac (simpset() addsimps [is_execution_fragment_def])1);
-  by (safe_tac (claset()));
+  by Safe_tac;
 
   by (eres_inst_tac [("x","snd ex n")] allE 1);
   by (eres_inst_tac [("x","snd ex (Suc n)")] allE 1);
@@ -51,7 +51,7 @@
 (* Lemmata *)
 
 val prems = goal HOL.thy "(P ==> Q-->R) ==> P&Q --> R";
-  by(fast_tac (claset() addDs prems) 1);
+  by (fast_tac (claset() addDs prems) 1);
 val imp_conj_lemma = result();
 
 
@@ -120,7 +120,7 @@
 by (simp_tac (simpset() addsimps [externals_of_par_extra]) 1);
 by (simp_tac (simpset() addsimps [par_def]) 1);
 by (asm_full_simp_tac (simpset() addsimps [trans_of_def]) 1);
-by (rtac (expand_if RS ssubst) 1);
+by (stac expand_if 1);
 by (rtac conjI 1);
 by (rtac impI 1); 
 by (etac disjE 1);
@@ -142,7 +142,7 @@
 by (Fast_tac 2);
 by (simp_tac (simpset() addsimps [conj_disj_distribR] addcongs [conj_cong]
                  addsplits [expand_if]) 1);
-by(REPEAT((resolve_tac [conjI,impI] 1 ORELSE etac conjE 1) THEN
+by (REPEAT((resolve_tac [conjI,impI] 1 ORELSE etac conjE 1) THEN
         asm_full_simp_tac(simpset() addsimps[comp1_reachable,
                                       comp2_reachable])1));
 qed"fxg_is_weak_pmap_of_product_IOA";
@@ -174,8 +174,8 @@
 by (rtac imp_conj_lemma 1);
 by (simp_tac (simpset() addsimps [rename_def]) 1);
 by (asm_full_simp_tac (simpset() addsimps [externals_def,asig_inputs_def,asig_outputs_def,asig_of_def,trans_of_def]) 1);
-by (safe_tac (claset()));
-by (rtac (expand_if RS ssubst) 1);
+by Safe_tac;
+by (stac expand_if 1);
  by (rtac conjI 1);
  by (rtac impI 1);
  by (etac disjE 1);
diff -r 451104c223e2 -r e534c4c32d54 src/HOL/MiniML/Generalize.ML
--- a/src/HOL/MiniML/Generalize.ML	Wed Nov 05 13:14:15 1997 +0100
+++ b/src/HOL/MiniML/Generalize.ML	Wed Nov 05 13:23:46 1997 +0100
@@ -95,7 +95,7 @@
 
 goalw Generalize.thy [le_type_scheme_def,is_bound_typ_instance]
   "gen ($ S A) ($ S t) <= $ S (gen A t)";
-by (safe_tac (claset()));
+by Safe_tac;
 by (rename_tac "R" 1);
 by (res_inst_tac [("x", "(%a. bound_typ_inst R (gen ($S A) (S a)))")] exI 1);
 by (typ.induct_tac "t" 1);
@@ -105,7 +105,7 @@
 
 goalw Generalize.thy [le_type_scheme_def,is_bound_typ_instance]
   "!!A B. free_tv B <= free_tv A ==> gen A t <= gen B t";
-by (safe_tac (claset()));
+by Safe_tac;
 by (rename_tac "S" 1);
 by (res_inst_tac [("x","%b. if b:free_tv A then TVar b else S b")] exI 1);
 by (typ.induct_tac "t" 1);
diff -r 451104c223e2 -r e534c4c32d54 src/HOL/MiniML/Instance.ML
--- a/src/HOL/MiniML/Instance.ML	Wed Nov 05 13:14:15 1997 +0100
+++ b/src/HOL/MiniML/Instance.ML	Wed Nov 05 13:23:46 1997 +0100
@@ -50,7 +50,7 @@
 \         (? S. !x:bound_tv sch. B x = mk_scheme (S x))";
 by (type_scheme.induct_tac "sch" 1);
 by (Simp_tac 1);
-by (safe_tac (claset()));
+by Safe_tac;
 by (rtac exI 1);
 by (rtac ballI 1);
 by (rtac sym 1);
@@ -62,10 +62,10 @@
 by (dtac sym 1);
 by (dtac sym 1);
 by (REPEAT ((dtac mp 1) THEN (Fast_tac 1)));
-by (safe_tac (claset()));
+by Safe_tac;
 by (rename_tac "S1 S2" 1);
 by (res_inst_tac [("x","%x. if x:bound_tv type_scheme1 then (S1 x) else (S2 x)")] exI 1);
-by (safe_tac (claset()));
+by Safe_tac;
 by (asm_simp_tac (simpset() addsplits [expand_if]) 1);
 by (asm_simp_tac (simpset() addsplits [expand_if]) 1);
 by (strip_tac 1);
@@ -123,7 +123,7 @@
 by (asm_full_simp_tac (simpset() addsimps [subst_to_scheme_inverse]) 1);
 by (res_inst_tac [("x","(subst_to_scheme (%k. if n <= k then BVar (k - n) else FVar k)) o S")] exI 1);
 by (asm_simp_tac (simpset() addsimps [aux2]) 1);
-by (safe_tac (claset()));
+by Safe_tac;
 by (res_inst_tac [("x","%n. bound_typ_inst S (B n)")] exI 1);
 by (type_scheme.induct_tac "sch" 1);
 by (Simp_tac 1);
@@ -162,7 +162,7 @@
   "(sch # A <= sch' # B) = (sch <= (sch'::type_scheme) & A <= B)";
 by (Simp_tac 1);
 by (rtac iffI 1);
- by (SELECT_GOAL(safe_tac (claset()))1);
+ by (SELECT_GOAL Safe_tac 1);
   by (eres_inst_tac [("x","0")] allE 1);
   by (Asm_full_simp_tac 1);
  by (eres_inst_tac [("x","Suc i")] allE 1);
@@ -220,7 +220,7 @@
 by (type_scheme.induct_tac "sch" 1);
   by (Simp_tac 1);
  by (Simp_tac 1);
- by (SELECT_GOAL(safe_tac(claset()))1);
+ by (SELECT_GOAL Safe_tac 1);
  by (eres_inst_tac [("x","TVar n -> TVar n")] allE 1);
  by (Asm_full_simp_tac 1);
  by (Fast_tac 1);
diff -r 451104c223e2 -r e534c4c32d54 src/HOL/MiniML/Type.ML
--- a/src/HOL/MiniML/Type.ML	Wed Nov 05 13:14:15 1997 +0100
+++ b/src/HOL/MiniML/Type.ML	Wed Nov 05 13:23:46 1997 +0100
@@ -444,7 +444,7 @@
 (* all greater variables are also new *)
 goalw thy [new_tv_def] 
   "!!n m. n<=m ==> new_tv n t ==> new_tv m t";
-by (safe_tac (claset()));
+by Safe_tac;
 by (dtac spec 1);
 by (mp_tac 1);
 by (trans_tac 1);
@@ -547,7 +547,7 @@
 
 goalw thy [max_def] "!!n::nat. m < n ==> m < max n n'";
 by (simp_tac (simpset() addsplits [expand_if]) 1);
-by (safe_tac (claset()));
+by Safe_tac;
 by (trans_tac 1);
 qed "less_maxL";
 
diff -r 451104c223e2 -r e534c4c32d54 src/HOL/NatDef.ML
--- a/src/HOL/NatDef.ML	Wed Nov 05 13:14:15 1997 +0100
+++ b/src/HOL/NatDef.ML	Wed Nov 05 13:23:46 1997 +0100
@@ -628,11 +628,11 @@
         hyp_subst_tac 1,
         rewtac Least_nat_def,
         rtac (select_equality RS arg_cong RS sym) 1,
-        safe_tac (claset()),
+        Safe_tac,
         dtac Suc_mono 1,
         Blast_tac 1,
         cut_facts_tac [less_linear] 1,
-        safe_tac (claset()),
+        Safe_tac,
         atac 2,
         Blast_tac 2,
         dtac Suc_mono 1,
diff -r 451104c223e2 -r e534c4c32d54 src/HOL/Subst/Unify.ML
--- a/src/HOL/Subst/Unify.ML	Wed Nov 05 13:14:15 1997 +0100
+++ b/src/HOL/Subst/Unify.ML	Wed Nov 05 13:23:46 1997 +0100
@@ -225,7 +225,7 @@
 by (rotate_tac ~2 1);
 by (asm_full_simp_tac 
     (simpset() addsimps [MGUnifier_def, Unifier_def, MoreGeneral_def]) 1);
-by (safe_tac (claset()) THEN rename_tac "theta sigma gamma" 1);
+by (Safe_tac THEN rename_tac "theta sigma gamma" 1);
 by (eres_inst_tac [("x","gamma")] allE 1 THEN mp_tac 1);
 by (etac exE 1 THEN rename_tac "delta" 1);
 by (eres_inst_tac [("x","delta")] allE 1);
@@ -248,7 +248,7 @@
        (simpset() addsimps [Var_Idem] 
 	         addsplits [expand_if,split_option_case])));
 (*Comb-Comb case*)
-by (safe_tac (claset()));
+by Safe_tac;
 by (REPEAT (dtac spec 1 THEN mp_tac 1));
 by (safe_tac (claset() addSDs [rewrite_rule [MGUnifier_def] unify_gives_MGU]));
 by (rtac Idem_comp 1);
diff -r 451104c223e2 -r e534c4c32d54 src/HOL/Trancl.ML
--- a/src/HOL/Trancl.ML	Wed Nov 05 13:14:15 1997 +0100
+++ b/src/HOL/Trancl.ML	Wed Nov 05 13:23:46 1997 +0100
@@ -78,7 +78,7 @@
 
 (*transitivity of transitive closure!! -- by induction.*)
 goalw Trancl.thy [trans_def] "trans(r^*)";
-by (safe_tac (claset()));
+by Safe_tac;
 by (eres_inst_tac [("b","z")] rtrancl_induct 1);
 by (ALLGOALS(blast_tac (claset() addIs [rtrancl_into_rtrancl])));
 qed "trans_rtrancl";
diff -r 451104c223e2 -r e534c4c32d54 src/HOL/Univ.ML
--- a/src/HOL/Univ.ML	Wed Nov 05 13:14:15 1997 +0100
+++ b/src/HOL/Univ.ML	Wed Nov 05 13:23:46 1997 +0100
@@ -226,7 +226,7 @@
     "ndepth (Push_Node i n) = Suc(ndepth(n))";
 by (stac (Rep_Node RS Node_Push_I RS Abs_Node_inverse) 1);
 by (cut_facts_tac [rewrite_rule [Node_def] Rep_Node] 1);
-by (safe_tac (claset()));
+by Safe_tac;
 by (etac ssubst 1);  (*instantiates type variables!*)
 by (Simp_tac 1);
 by (rtac Least_equality 1);
@@ -546,7 +546,7 @@
 (*Dependent version*)
 goal Univ.thy
     "(Sigma A B <**> Sigma C D) <= Sigma (A<*>C) (Split(%x y. B(x)<*>D(y)))";
-by (safe_tac (claset()));
+by Safe_tac;
 by (stac Split 1);
 by (Blast_tac 1);
 qed "dprod_subset_Sigma2";
diff -r 451104c223e2 -r e534c4c32d54 src/HOL/WF.ML
--- a/src/HOL/WF.ML	Wed Nov 05 13:14:15 1997 +0100
+++ b/src/HOL/WF.ML	Wed Nov 05 13:23:46 1997 +0100
@@ -111,7 +111,7 @@
  by (blast_tac (claset() addEs [wf_trancl RS wf_irrefl] addIs
       [rtrancl_into_trancl1,wf_subset,impOfSubs rtrancl_mono]) 1);
 by (asm_full_simp_tac (simpset() addsimps [wf_eq_minimal]) 1);
-by (safe_tac (claset()));
+by Safe_tac;
 by (EVERY1[rtac allE, atac, etac impE, Blast_tac]);
 by (etac bexE 1);
 by (rename_tac "a" 1);
@@ -327,5 +327,5 @@
 
 goal WF.thy "!M R f. (f=wfrec R M) --> wf R --> (!x. f x = M (cut f R x) x)";
 by (Clarify_tac 1);
-be wfrec 1;
+by (etac wfrec 1);
 qed "tfl_wfrec";
diff -r 451104c223e2 -r e534c4c32d54 src/HOL/ex/MT.ML
--- a/src/HOL/ex/MT.ML	Wed Nov 05 13:14:15 1997 +0100
+++ b/src/HOL/ex/MT.ML	Wed Nov 05 13:23:46 1997 +0100
@@ -230,7 +230,7 @@
 by (rtac eval_fun_mono 1);
 by (rewtac eval_fun_def);
 by (dtac CollectD 1);
-by (safe_tac (claset()));
+by Safe_tac;
 by (ALLGOALS (resolve_tac prems));
 by (ALLGOALS (Blast_tac));
 qed "eval_ind0";
@@ -336,7 +336,7 @@
 by (rtac elab_fun_mono 1);
 by (rewtac elab_fun_def);
 by (dtac CollectD 1);
-by (safe_tac (claset()));
+by Safe_tac;
 by (ALLGOALS (resolve_tac prems));
 by (ALLGOALS (Blast_tac));
 qed "elab_ind0";
@@ -387,7 +387,7 @@
 by (rtac elab_fun_mono 1);
 by (rewtac elab_fun_def);
 by (dtac CollectD 1);
-by (safe_tac (claset()));
+by Safe_tac;
 by (ALLGOALS (resolve_tac prems));
 by (ALLGOALS (Blast_tac));
 qed "elab_elim0";
@@ -552,7 +552,7 @@
 by (rewtac hasty_fun_def);
 by (dtac CollectD 1);
 by (fold_goals_tac [hasty_fun_def]);
-by (safe_tac (claset()));
+by Safe_tac;
 by (REPEAT (ares_tac prems 1));
 qed "hasty_rel_elim0";
 
@@ -690,7 +690,7 @@
 \   |] ==> \
 \   v_const(c_app c1 c2) hasty t";
 by (dtac elab_app_elim 1);
-by (safe_tac (claset()));
+by Safe_tac;
 by (rtac hasty_const 1);
 by (rtac isof_app 1);
 by (rtac hasty_elim_const 1);
@@ -711,7 +711,7 @@
 \   |] ==> \
 \   v hasty t";
 by (dtac elab_app_elim 1);
-by (safe_tac (claset()));
+by Safe_tac;
 by ((etac allE 1) THEN (etac allE 1) THEN (etac impE 1));
 by (assume_tac 1);
 by (etac impE 1);
@@ -721,7 +721,7 @@
 by (etac impE 1);
 by (assume_tac 1);
 by (dtac hasty_elim_clos 1);
-by (safe_tac (claset()));
+by Safe_tac;
 by (dtac elab_fn_elim 1);
 by (blast_tac (claset() addIs [hasty_env1] addSDs [t_fun_inj]) 1);
 qed "consistency_app2";
@@ -733,7 +733,7 @@
 (* Proof by induction on the structure of evaluations *)
 
 by (rtac (major RS eval_ind) 1);
-by (safe_tac (claset()));
+by Safe_tac;
 by (DEPTH_SOLVE 
     (ares_tac [consistency_const, consistency_var, consistency_fn,
                consistency_fix, consistency_app1, consistency_app2] 1));
@@ -746,7 +746,7 @@
 val prems = goalw MT.thy [isof_env_def,hasty_env_def] 
   "ve isofenv te ==> ve hastyenv te";
 by (cut_facts_tac prems 1);
-by (safe_tac (claset()));
+by Safe_tac;
 by (etac allE 1);
 by (etac impE 1);
 by (assume_tac 1);
diff -r 451104c223e2 -r e534c4c32d54 src/HOL/ex/Primrec.ML
--- a/src/HOL/ex/Primrec.ML	Wed Nov 05 13:14:15 1997 +0100
+++ b/src/HOL/ex/Primrec.ML	Wed Nov 05 13:23:46 1997 +0100
@@ -200,7 +200,7 @@
 \      ==> EX k. ALL l. list_add (map(%f. f l) fs) < ack(k, list_add l)";
 by (etac lists.induct 1);
 by (res_inst_tac [("x","0")] exI 1 THEN Asm_simp_tac 1);
-by (safe_tac (claset()));
+by Safe_tac;
 by (Asm_simp_tac 1);
 by (blast_tac (claset() addIs [add_less_mono, ack_add_bound, less_trans]) 1);
 qed "COMP_map_lemma";
diff -r 451104c223e2 -r e534c4c32d54 src/HOL/ex/cla.ML
--- a/src/HOL/ex/cla.ML	Wed Nov 05 13:14:15 1997 +0100
+++ b/src/HOL/ex/cla.ML	Wed Nov 05 13:23:46 1997 +0100
@@ -381,7 +381,7 @@
   the type constraint ensures that x,y,z have the same type as a,b,u. *)
 goal HOL.thy "(? x y::'a. ! z. z=x | z=y) & P(a) & P(b) & (~a=b) \
 \               --> (! u::'a. P(u))";
-by (Classical.safe_tac (claset()));
+by (Classical.Safe_tac);
 by (res_inst_tac [("x","a")] allE 1);
 by (assume_tac 1);
 by (res_inst_tac [("x","b")] allE 1);
diff -r 451104c223e2 -r e534c4c32d54 src/HOL/ex/meson.ML
--- a/src/HOL/ex/meson.ML	Wed Nov 05 13:14:15 1997 +0100
+++ b/src/HOL/ex/meson.ML	Wed Nov 05 13:23:46 1997 +0100
@@ -430,7 +430,7 @@
 
 (*First, breaks the goal into independent units*)
 val safe_best_meson_tac =
-     SELECT_GOAL (TRY (safe_tac (claset())) THEN 
+     SELECT_GOAL (TRY Safe_tac THEN 
                   TRYALL (best_meson_tac size_of_subgoals));
 
 (** Depth-first search version **)
@@ -464,7 +464,7 @@
                            (prolog_step_tac' (make_horns cls))));
 
 val safe_meson_tac =
-     SELECT_GOAL (TRY (safe_tac (claset())) THEN 
+     SELECT_GOAL (TRY Safe_tac THEN 
                   TRYALL (iter_deepen_meson_tac));
 
 
diff -r 451104c223e2 -r e534c4c32d54 src/HOL/ex/set.ML
--- a/src/HOL/ex/set.ML	Wed Nov 05 13:14:15 1997 +0100
+++ b/src/HOL/ex/set.ML	Wed Nov 05 13:23:46 1997 +0100
@@ -9,15 +9,14 @@
 
 writeln"File HOL/ex/set.";
 
-context Set.thy;
+context Lfp.thy;
 
-(*Nice demonstration of blast_tac--and its overloading problems*)
+(*Nice demonstration of blast_tac--and its limitations*)
 goal Set.thy "!!S::'a set set. ALL x:S. ALL y:S. x<=y ==> EX z. S <= {z}";
-let val insertCI' = read_instantiate [("'a", "?'a set")] insertCI
-in    (*Type instantiation is required so that blast_tac can apply equalityI
-        to the subgoal arising from insertCI*)
-by(blast_tac (claset() addSIs [insertCI']) 1)
-end;
+(*for some unfathomable reason, UNIV_I increases the search space greatly*)
+by (blast_tac (claset() delrules [UNIV_I]) 1);
+result();
+
 
 (*** A unique fixpoint theorem --- fast/best/meson all fail ***)