Ran expandshort, especially to introduce Safe_tac
authorpaulson
Wed Nov 05 13:23:46 1997 +0100 (1997-11-05)
changeset 4153e534c4c32d54
parent 4152 451104c223e2
child 4154 17a3a2c5a35f
Ran expandshort, especially to introduce Safe_tac
src/HOL/Auth/Yahalom2.ML
src/HOL/AxClasses/Lattice/CLattice.ML
src/HOL/AxClasses/Lattice/LatInsts.ML
src/HOL/AxClasses/Lattice/LatMorph.ML
src/HOL/AxClasses/Lattice/LatPreInsts.ML
src/HOL/AxClasses/Lattice/Lattice.ML
src/HOL/AxClasses/Lattice/OrdDefs.ML
src/HOL/AxClasses/Lattice/Order.ML
src/HOL/Finite.ML
src/HOL/Hoare/Examples.ML
src/HOL/Hoare/List_Examples.ML
src/HOL/IMP/Hoare.ML
src/HOL/IMP/Transition.ML
src/HOL/IOA/IOA.ML
src/HOL/IOA/Solve.ML
src/HOL/MiniML/Generalize.ML
src/HOL/MiniML/Instance.ML
src/HOL/MiniML/Type.ML
src/HOL/NatDef.ML
src/HOL/Subst/Unify.ML
src/HOL/Trancl.ML
src/HOL/Univ.ML
src/HOL/WF.ML
src/HOL/ex/MT.ML
src/HOL/ex/Primrec.ML
src/HOL/ex/cla.ML
src/HOL/ex/meson.ML
src/HOL/ex/set.ML
     1.1 --- a/src/HOL/Auth/Yahalom2.ML	Wed Nov 05 13:14:15 1997 +0100
     1.2 +++ b/src/HOL/Auth/Yahalom2.ML	Wed Nov 05 13:23:46 1997 +0100
     1.3 @@ -400,7 +400,7 @@
     1.4  \        ==> EX X. Says A B {|X, Crypt K (Nonce NB)|} : set evs";
     1.5  by (etac (Says_imp_spies RS parts.Inj RS MPair_parts) 1);
     1.6  by (dtac B_trusts_YM4_shrK 1);
     1.7 -by (safe_tac (claset()));
     1.8 +by Safe_tac;
     1.9  by (rtac lemma 1);
    1.10  by (rtac Spy_not_see_encrypted_key 2);
    1.11  by (REPEAT_FIRST assume_tac);
     2.1 --- a/src/HOL/AxClasses/Lattice/CLattice.ML	Wed Nov 05 13:14:15 1997 +0100
     2.2 +++ b/src/HOL/AxClasses/Lattice/CLattice.ML	Wed Nov 05 13:23:46 1997 +0100
     2.3 @@ -7,46 +7,46 @@
     2.4  (* unique existence *)
     2.5  
     2.6  goalw thy [Inf_def] "is_Inf A (Inf A)";
     2.7 -  br (ex_Inf RS spec RS selectI1) 1;
     2.8 +  by (rtac (ex_Inf RS spec RS selectI1) 1);
     2.9  qed "Inf_is_Inf";
    2.10  
    2.11  goal thy "is_Inf A inf --> Inf A = inf";
    2.12 -  br impI 1;
    2.13 -  br (is_Inf_uniq RS mp) 1;
    2.14 -  br conjI 1;
    2.15 -  br Inf_is_Inf 1;
    2.16 -  ba 1;
    2.17 +  by (rtac impI 1);
    2.18 +  by (rtac (is_Inf_uniq RS mp) 1);
    2.19 +  by (rtac conjI 1);
    2.20 +  by (rtac Inf_is_Inf 1);
    2.21 +  by (assume_tac 1);
    2.22  qed "Inf_uniq";
    2.23  
    2.24  goalw thy [Ex1_def] "ALL A. EX! inf::'a::clattice. is_Inf A inf";
    2.25 -  by (safe_tac (claset()));
    2.26 +  by Safe_tac;
    2.27    by (Step_tac 1);
    2.28    by (Step_tac 1);
    2.29 -  br Inf_is_Inf 1;
    2.30 -  br (Inf_uniq RS mp RS sym) 1;
    2.31 -  ba 1;
    2.32 +  by (rtac Inf_is_Inf 1);
    2.33 +  by (rtac (Inf_uniq RS mp RS sym) 1);
    2.34 +  by (assume_tac 1);
    2.35  qed "ex1_Inf";
    2.36  
    2.37  
    2.38  goalw thy [Sup_def] "is_Sup A (Sup A)";
    2.39 -  br (ex_Sup RS spec RS selectI1) 1;
    2.40 +  by (rtac (ex_Sup RS spec RS selectI1) 1);
    2.41  qed "Sup_is_Sup";
    2.42  
    2.43  goal thy "is_Sup A sup --> Sup A = sup";
    2.44 -  br impI 1;
    2.45 -  br (is_Sup_uniq RS mp) 1;
    2.46 -  br conjI 1;
    2.47 -  br Sup_is_Sup 1;
    2.48 -  ba 1;
    2.49 +  by (rtac impI 1);
    2.50 +  by (rtac (is_Sup_uniq RS mp) 1);
    2.51 +  by (rtac conjI 1);
    2.52 +  by (rtac Sup_is_Sup 1);
    2.53 +  by (assume_tac 1);
    2.54  qed "Sup_uniq";
    2.55  
    2.56  goalw thy [Ex1_def] "ALL A. EX! sup::'a::clattice. is_Sup A sup";
    2.57 -  by (safe_tac (claset()));
    2.58 +  by Safe_tac;
    2.59    by (Step_tac 1);
    2.60    by (Step_tac 1);
    2.61 -  br Sup_is_Sup 1;
    2.62 -  br (Sup_uniq RS mp RS sym) 1;
    2.63 -  ba 1;
    2.64 +  by (rtac Sup_is_Sup 1);
    2.65 +  by (rtac (Sup_uniq RS mp RS sym) 1);
    2.66 +  by (assume_tac 1);
    2.67  qed "ex1_Sup";
    2.68  
    2.69  
    2.70 @@ -54,68 +54,68 @@
    2.71  
    2.72  val prems = goalw thy [Inf_def] "x:A ==> Inf A [= x";
    2.73    by (cut_facts_tac prems 1);
    2.74 -  br selectI2 1;
    2.75 -  br Inf_is_Inf 1;
    2.76 +  by (rtac selectI2 1);
    2.77 +  by (rtac Inf_is_Inf 1);
    2.78    by (rewtac is_Inf_def);
    2.79    by (Fast_tac 1);
    2.80  qed "Inf_lb";
    2.81  
    2.82  val [prem] = goalw thy [Inf_def] "(!!x. x:A ==> z [= x) ==> z [= Inf A";
    2.83 -  br selectI2 1;
    2.84 -  br Inf_is_Inf 1;
    2.85 +  by (rtac selectI2 1);
    2.86 +  by (rtac Inf_is_Inf 1);
    2.87    by (rewtac is_Inf_def);
    2.88    by (Step_tac 1);
    2.89    by (Step_tac 1);
    2.90 -  be mp 1;
    2.91 -  br ballI 1;
    2.92 -  be prem 1;
    2.93 +  by (etac mp 1);
    2.94 +  by (rtac ballI 1);
    2.95 +  by (etac prem 1);
    2.96  qed "Inf_ub_lbs";
    2.97  
    2.98  
    2.99  val prems = goalw thy [Sup_def] "x:A ==> x [= Sup A";
   2.100    by (cut_facts_tac prems 1);
   2.101 -  br selectI2 1;
   2.102 -  br Sup_is_Sup 1;
   2.103 +  by (rtac selectI2 1);
   2.104 +  by (rtac Sup_is_Sup 1);
   2.105    by (rewtac is_Sup_def);
   2.106    by (Fast_tac 1);
   2.107  qed "Sup_ub";
   2.108  
   2.109  val [prem] = goalw thy [Sup_def] "(!!x. x:A ==> x [= z) ==> Sup A [= z";
   2.110 -  br selectI2 1;
   2.111 -  br Sup_is_Sup 1;
   2.112 +  by (rtac selectI2 1);
   2.113 +  by (rtac Sup_is_Sup 1);
   2.114    by (rewtac is_Sup_def);
   2.115    by (Step_tac 1);
   2.116    by (Step_tac 1);
   2.117 -  be mp 1;
   2.118 -  br ballI 1;
   2.119 -  be prem 1;
   2.120 +  by (etac mp 1);
   2.121 +  by (rtac ballI 1);
   2.122 +  by (etac prem 1);
   2.123  qed "Sup_lb_ubs";
   2.124  
   2.125  
   2.126  (** minorized Infs / majorized Sups **)
   2.127  
   2.128  goal thy "(x [= Inf A) = (ALL y:A. x [= y)";
   2.129 -  br iffI 1;
   2.130 +  by (rtac iffI 1);
   2.131    (*==>*)
   2.132 -    br ballI 1;
   2.133 -    br (le_trans RS mp) 1;
   2.134 -    be conjI 1;
   2.135 -    be Inf_lb 1;
   2.136 +    by (rtac ballI 1);
   2.137 +    by (rtac (le_trans RS mp) 1);
   2.138 +    by (etac conjI 1);
   2.139 +    by (etac Inf_lb 1);
   2.140    (*<==*)
   2.141 -    br Inf_ub_lbs 1;
   2.142 +    by (rtac Inf_ub_lbs 1);
   2.143      by (Fast_tac 1);
   2.144  qed "le_Inf_eq";
   2.145  
   2.146  goal thy "(Sup A [= x) = (ALL y:A. y [= x)";
   2.147 -  br iffI 1;
   2.148 +  by (rtac iffI 1);
   2.149    (*==>*)
   2.150 -    br ballI 1;
   2.151 -    br (le_trans RS mp) 1;
   2.152 -    br conjI 1;
   2.153 -    be Sup_ub 1;
   2.154 -    ba 1;
   2.155 +    by (rtac ballI 1);
   2.156 +    by (rtac (le_trans RS mp) 1);
   2.157 +    by (rtac conjI 1);
   2.158 +    by (etac Sup_ub 1);
   2.159 +    by (assume_tac 1);
   2.160    (*<==*)
   2.161 -    br Sup_lb_ubs 1;
   2.162 +    by (rtac Sup_lb_ubs 1);
   2.163      by (Fast_tac 1);
   2.164  qed "ge_Sup_eq";
   2.165  
   2.166 @@ -124,60 +124,60 @@
   2.167  (** Subsets and limits **)
   2.168  
   2.169  goal thy "A <= B --> Inf B [= Inf A";
   2.170 -  br impI 1;
   2.171 +  by (rtac impI 1);
   2.172    by (stac le_Inf_eq 1);
   2.173    by (rewtac Ball_def);
   2.174 -  by (safe_tac (claset()));
   2.175 -  bd subsetD 1;
   2.176 -  ba 1;
   2.177 -  be Inf_lb 1;
   2.178 +  by Safe_tac;
   2.179 +  by (dtac subsetD 1);
   2.180 +  by (assume_tac 1);
   2.181 +  by (etac Inf_lb 1);
   2.182  qed "Inf_subset_antimon";
   2.183  
   2.184  goal thy "A <= B --> Sup A [= Sup B";
   2.185 -  br impI 1;
   2.186 +  by (rtac impI 1);
   2.187    by (stac ge_Sup_eq 1);
   2.188    by (rewtac Ball_def);
   2.189 -  by (safe_tac (claset()));
   2.190 -  bd subsetD 1;
   2.191 -  ba 1;
   2.192 -  be Sup_ub 1;
   2.193 +  by Safe_tac;
   2.194 +  by (dtac subsetD 1);
   2.195 +  by (assume_tac 1);
   2.196 +  by (etac Sup_ub 1);
   2.197  qed "Sup_subset_mon";
   2.198  
   2.199  
   2.200  (** singleton / empty limits **)
   2.201  
   2.202  goal thy "Inf {x} = x";
   2.203 -  br (Inf_uniq RS mp) 1;
   2.204 +  by (rtac (Inf_uniq RS mp) 1);
   2.205    by (rewtac is_Inf_def);
   2.206 -  by (safe_tac (claset()));
   2.207 -  br le_refl 1;
   2.208 +  by Safe_tac;
   2.209 +  by (rtac le_refl 1);
   2.210    by (Fast_tac 1);
   2.211  qed "sing_Inf_eq";
   2.212  
   2.213  goal thy "Sup {x} = x";
   2.214 -  br (Sup_uniq RS mp) 1;
   2.215 +  by (rtac (Sup_uniq RS mp) 1);
   2.216    by (rewtac is_Sup_def);
   2.217 -  by (safe_tac (claset()));
   2.218 -  br le_refl 1;
   2.219 +  by Safe_tac;
   2.220 +  by (rtac le_refl 1);
   2.221    by (Fast_tac 1);
   2.222  qed "sing_Sup_eq";
   2.223  
   2.224  
   2.225  goal thy "Inf {} = Sup {x. True}";
   2.226 -  br (Inf_uniq RS mp) 1;
   2.227 +  by (rtac (Inf_uniq RS mp) 1);
   2.228    by (rewtac is_Inf_def);
   2.229 -  by (safe_tac (claset()));
   2.230 -  br (sing_Sup_eq RS subst) 1;
   2.231 +  by Safe_tac;
   2.232 +  by (rtac (sing_Sup_eq RS subst) 1);
   2.233    back();
   2.234 -  br (Sup_subset_mon RS mp) 1;
   2.235 +  by (rtac (Sup_subset_mon RS mp) 1);
   2.236    by (Fast_tac 1);
   2.237  qed "empty_Inf_eq";
   2.238  
   2.239  goal thy "Sup {} = Inf {x. True}";
   2.240 -  br (Sup_uniq RS mp) 1;
   2.241 +  by (rtac (Sup_uniq RS mp) 1);
   2.242    by (rewtac is_Sup_def);
   2.243 -  by (safe_tac (claset()));
   2.244 -  br (sing_Inf_eq RS subst) 1;
   2.245 -  br (Inf_subset_antimon RS mp) 1;
   2.246 +  by Safe_tac;
   2.247 +  by (rtac (sing_Inf_eq RS subst) 1);
   2.248 +  by (rtac (Inf_subset_antimon RS mp) 1);
   2.249    by (Fast_tac 1);
   2.250  qed "empty_Sup_eq";
     3.1 --- a/src/HOL/AxClasses/Lattice/LatInsts.ML	Wed Nov 05 13:14:15 1997 +0100
     3.2 +++ b/src/HOL/AxClasses/Lattice/LatInsts.ML	Wed Nov 05 13:23:46 1997 +0100
     3.3 @@ -3,15 +3,15 @@
     3.4  
     3.5  
     3.6  goal thy "Inf {x, y} = x && y";
     3.7 -  br (Inf_uniq RS mp) 1;
     3.8 +  by (rtac (Inf_uniq RS mp) 1);
     3.9    by (stac bin_is_Inf_eq 1);
    3.10 -  br inf_is_inf 1;
    3.11 +  by (rtac inf_is_inf 1);
    3.12  qed "bin_Inf_eq";
    3.13  
    3.14  goal thy "Sup {x, y} = x || y";
    3.15 -  br (Sup_uniq RS mp) 1;
    3.16 +  by (rtac (Sup_uniq RS mp) 1);
    3.17    by (stac bin_is_Sup_eq 1);
    3.18 -  br sup_is_sup 1;
    3.19 +  by (rtac sup_is_sup 1);
    3.20  qed "bin_Sup_eq";
    3.21  
    3.22  
    3.23 @@ -19,39 +19,39 @@
    3.24  (* Unions and limits *)
    3.25  
    3.26  goal thy "Inf (A Un B) = Inf A && Inf B";
    3.27 -  br (Inf_uniq RS mp) 1;
    3.28 +  by (rtac (Inf_uniq RS mp) 1);
    3.29    by (rewtac is_Inf_def);
    3.30 -  by (safe_tac (claset()));
    3.31 +  by Safe_tac;
    3.32  
    3.33 -  br (conjI RS (le_trans RS mp)) 1;
    3.34 -  br inf_lb1 1;
    3.35 -  be Inf_lb 1;
    3.36 +  by (rtac (conjI RS (le_trans RS mp)) 1);
    3.37 +  by (rtac inf_lb1 1);
    3.38 +  by (etac Inf_lb 1);
    3.39  
    3.40 -  br (conjI RS (le_trans RS mp)) 1;
    3.41 -  br inf_lb2 1;
    3.42 -  be Inf_lb 1;
    3.43 +  by (rtac (conjI RS (le_trans RS mp)) 1);
    3.44 +  by (rtac inf_lb2 1);
    3.45 +  by (etac Inf_lb 1);
    3.46  
    3.47    by (stac le_inf_eq 1);
    3.48 -  br conjI 1;
    3.49 -  br Inf_ub_lbs 1;
    3.50 +  by (rtac conjI 1);
    3.51 +  by (rtac Inf_ub_lbs 1);
    3.52    by (Fast_tac 1);
    3.53 -  br Inf_ub_lbs 1;
    3.54 +  by (rtac Inf_ub_lbs 1);
    3.55    by (Fast_tac 1);
    3.56  qed "Inf_Un_eq";
    3.57  
    3.58  goal thy "Inf (UN i:A. B i) = Inf {Inf (B i) |i. i:A}";
    3.59 -  br (Inf_uniq RS mp) 1;
    3.60 +  by (rtac (Inf_uniq RS mp) 1);
    3.61    by (rewtac is_Inf_def);
    3.62 -  by (safe_tac (claset()));
    3.63 +  by Safe_tac;
    3.64    (*level 3*)
    3.65 -  br (conjI RS (le_trans RS mp)) 1;
    3.66 -  be Inf_lb 2;
    3.67 -  br (sing_Inf_eq RS subst) 1;
    3.68 -  br (Inf_subset_antimon RS mp) 1;
    3.69 +  by (rtac (conjI RS (le_trans RS mp)) 1);
    3.70 +  by (etac Inf_lb 2);
    3.71 +  by (rtac (sing_Inf_eq RS subst) 1);
    3.72 +  by (rtac (Inf_subset_antimon RS mp) 1);
    3.73    by (Fast_tac 1);
    3.74    (*level 8*)
    3.75    by (stac le_Inf_eq 1);
    3.76 -  by (safe_tac (claset()));
    3.77 +  by Safe_tac;
    3.78    by (stac le_Inf_eq 1);
    3.79    by (Fast_tac 1);
    3.80  qed "Inf_UN_eq";
    3.81 @@ -59,40 +59,40 @@
    3.82  
    3.83  
    3.84  goal thy "Sup (A Un B) = Sup A || Sup B";
    3.85 -  br (Sup_uniq RS mp) 1;
    3.86 +  by (rtac (Sup_uniq RS mp) 1);
    3.87    by (rewtac is_Sup_def);
    3.88 -  by (safe_tac (claset()));
    3.89 +  by Safe_tac;
    3.90  
    3.91 -  br (conjI RS (le_trans RS mp)) 1;
    3.92 -  be Sup_ub 1;
    3.93 -  br sup_ub1 1;
    3.94 +  by (rtac (conjI RS (le_trans RS mp)) 1);
    3.95 +  by (etac Sup_ub 1);
    3.96 +  by (rtac sup_ub1 1);
    3.97  
    3.98 -  br (conjI RS (le_trans RS mp)) 1;
    3.99 -  be Sup_ub 1;
   3.100 -  br sup_ub2 1;
   3.101 +  by (rtac (conjI RS (le_trans RS mp)) 1);
   3.102 +  by (etac Sup_ub 1);
   3.103 +  by (rtac sup_ub2 1);
   3.104  
   3.105    by (stac ge_sup_eq 1);
   3.106 -  br conjI 1;
   3.107 -  br Sup_lb_ubs 1;
   3.108 +  by (rtac conjI 1);
   3.109 +  by (rtac Sup_lb_ubs 1);
   3.110    by (Fast_tac 1);
   3.111 -  br Sup_lb_ubs 1;
   3.112 +  by (rtac Sup_lb_ubs 1);
   3.113    by (Fast_tac 1);
   3.114  qed "Sup_Un_eq";
   3.115  
   3.116  goal thy "Sup (UN i:A. B i) = Sup {Sup (B i) |i. i:A}";
   3.117 -  br (Sup_uniq RS mp) 1;
   3.118 +  by (rtac (Sup_uniq RS mp) 1);
   3.119    by (rewtac is_Sup_def);
   3.120 -  by (safe_tac (claset()));
   3.121 +  by Safe_tac;
   3.122    (*level 3*)
   3.123 -  br (conjI RS (le_trans RS mp)) 1;
   3.124 -  be Sup_ub 1;
   3.125 -  br (sing_Sup_eq RS subst) 1;
   3.126 +  by (rtac (conjI RS (le_trans RS mp)) 1);
   3.127 +  by (etac Sup_ub 1);
   3.128 +  by (rtac (sing_Sup_eq RS subst) 1);
   3.129    back();
   3.130 -  br (Sup_subset_mon RS mp) 1;
   3.131 +  by (rtac (Sup_subset_mon RS mp) 1);
   3.132    by (Fast_tac 1);
   3.133    (*level 8*)
   3.134    by (stac ge_Sup_eq 1);
   3.135 -  by (safe_tac (claset()));
   3.136 +  by Safe_tac;
   3.137    by (stac ge_Sup_eq 1);
   3.138    by (Fast_tac 1);
   3.139  qed "Sup_UN_eq";
     4.1 --- a/src/HOL/AxClasses/Lattice/LatMorph.ML	Wed Nov 05 13:14:15 1997 +0100
     4.2 +++ b/src/HOL/AxClasses/Lattice/LatMorph.ML	Wed Nov 05 13:23:46 1997 +0100
     4.3 @@ -5,49 +5,49 @@
     4.4  (** monotone functions vs. "&&"- / "||"-semi-morphisms **)
     4.5  
     4.6  goalw thy [is_mono_def] "is_mono f = (ALL x y. f (x && y) [= f x && f y)";
     4.7 -  by (safe_tac (claset()));
     4.8 +  by Safe_tac;
     4.9    (*==> (level 1)*)
    4.10      by (stac le_inf_eq 1);
    4.11 -    br conjI 1;
    4.12 +    by (rtac conjI 1);
    4.13      by (Step_tac 1);
    4.14      by (Step_tac 1);
    4.15 -    be mp 1;
    4.16 -    br inf_lb1 1;
    4.17 +    by (etac mp 1);
    4.18 +    by (rtac inf_lb1 1);
    4.19      by (Step_tac 1);
    4.20      by (Step_tac 1);
    4.21 -    be mp 1;
    4.22 -    br inf_lb2 1;
    4.23 +    by (etac mp 1);
    4.24 +    by (rtac inf_lb2 1);
    4.25    (*==> (level 11)*)
    4.26 -    br (conjI RS (le_trans RS mp)) 1;
    4.27 -    br inf_lb2 2;
    4.28 +    by (rtac (conjI RS (le_trans RS mp)) 1);
    4.29 +    by (rtac inf_lb2 2);
    4.30      by (subgoal_tac "x && y = x" 1);
    4.31 -    be subst 1;
    4.32 +    by (etac subst 1);
    4.33      by (Fast_tac 1);
    4.34      by (stac inf_connect 1);
    4.35 -    ba 1;
    4.36 +    by (assume_tac 1);
    4.37  qed "mono_inf_eq";
    4.38  
    4.39  goalw thy [is_mono_def] "is_mono f = (ALL x y. f x || f y [= f (x || y))";
    4.40 -  by (safe_tac (claset()));
    4.41 +  by Safe_tac;
    4.42    (*==> (level 1)*)
    4.43      by (stac ge_sup_eq 1);
    4.44 -    br conjI 1;
    4.45 +    by (rtac conjI 1);
    4.46      by (Step_tac 1);
    4.47      by (Step_tac 1);
    4.48 -    be mp 1;
    4.49 -    br sup_ub1 1;
    4.50 +    by (etac mp 1);
    4.51 +    by (rtac sup_ub1 1);
    4.52      by (Step_tac 1);
    4.53      by (Step_tac 1);
    4.54 -    be mp 1;
    4.55 -    br sup_ub2 1;
    4.56 +    by (etac mp 1);
    4.57 +    by (rtac sup_ub2 1);
    4.58    (*==> (level 11)*)
    4.59 -    br (conjI RS (le_trans RS mp)) 1;
    4.60 -    br sup_ub1 1;
    4.61 +    by (rtac (conjI RS (le_trans RS mp)) 1);
    4.62 +    by (rtac sup_ub1 1);
    4.63      by (subgoal_tac "x || y = y" 1);
    4.64 -    be subst 1;
    4.65 +    by (etac subst 1);
    4.66      by (Fast_tac 1);
    4.67      by (stac sup_connect 1);
    4.68 -    ba 1;
    4.69 +    by (assume_tac 1);
    4.70  qed "mono_sup_eq";
    4.71  
    4.72  
     5.1 --- a/src/HOL/AxClasses/Lattice/LatPreInsts.ML	Wed Nov 05 13:14:15 1997 +0100
     5.2 +++ b/src/HOL/AxClasses/Lattice/LatPreInsts.ML	Wed Nov 05 13:23:46 1997 +0100
     5.3 @@ -5,13 +5,13 @@
     5.4  (** complete lattices **)
     5.5  
     5.6  goal thy "is_inf x y (Inf {x, y})";
     5.7 -  br (bin_is_Inf_eq RS subst) 1;
     5.8 -  br Inf_is_Inf 1;
     5.9 +  by (rtac (bin_is_Inf_eq RS subst) 1);
    5.10 +  by (rtac Inf_is_Inf 1);
    5.11  qed "Inf_is_inf";
    5.12  
    5.13  goal thy "is_sup x y (Sup {x, y})";
    5.14 -  br (bin_is_Sup_eq RS subst) 1;
    5.15 -  br Sup_is_Sup 1;
    5.16 +  by (rtac (bin_is_Sup_eq RS subst) 1);
    5.17 +  by (rtac Sup_is_Sup 1);
    5.18  qed "Sup_is_sup";
    5.19  
    5.20  
    5.21 @@ -22,13 +22,13 @@
    5.22  
    5.23  goalw thy [is_inf_def, le_prod_def] "is_inf p q (fst p && fst q, snd p && snd q)";
    5.24    by (Simp_tac 1);
    5.25 -  by (safe_tac (claset()));
    5.26 +  by Safe_tac;
    5.27    by (REPEAT_FIRST (fn i => resolve_tac [inf_lb1, inf_lb2, inf_ub_lbs] i ORELSE atac i));
    5.28  qed "prod_is_inf";
    5.29  
    5.30  goalw thy [is_sup_def, le_prod_def] "is_sup p q (fst p || fst q, snd p || snd q)";
    5.31    by (Simp_tac 1);
    5.32 -  by (safe_tac (claset()));
    5.33 +  by Safe_tac;
    5.34    by (REPEAT_FIRST (fn i => resolve_tac [sup_ub1, sup_ub2, sup_lb_ubs] i ORELSE atac i));
    5.35  qed "prod_is_sup";
    5.36  
    5.37 @@ -36,18 +36,18 @@
    5.38  (* functions *)
    5.39  
    5.40  goalw thy [is_inf_def, le_fun_def] "is_inf f g (%x. f x && g x)";
    5.41 -  by (safe_tac (claset()));
    5.42 -  br inf_lb1 1;
    5.43 -  br inf_lb2 1;
    5.44 -  br inf_ub_lbs 1;
    5.45 +  by Safe_tac;
    5.46 +  by (rtac inf_lb1 1);
    5.47 +  by (rtac inf_lb2 1);
    5.48 +  by (rtac inf_ub_lbs 1);
    5.49    by (REPEAT_FIRST (Fast_tac));
    5.50  qed "fun_is_inf";
    5.51  
    5.52  goalw thy [is_sup_def, le_fun_def] "is_sup f g (%x. f x || g x)";
    5.53 -  by (safe_tac (claset()));
    5.54 -  br sup_ub1 1;
    5.55 -  br sup_ub2 1;
    5.56 -  br sup_lb_ubs 1;
    5.57 +  by Safe_tac;
    5.58 +  by (rtac sup_ub1 1);
    5.59 +  by (rtac sup_ub2 1);
    5.60 +  by (rtac sup_lb_ubs 1);
    5.61    by (REPEAT_FIRST (Fast_tac));
    5.62  qed "fun_is_sup";
    5.63  
    5.64 @@ -57,20 +57,20 @@
    5.65  
    5.66  goalw thy [is_inf_def, le_dual_def] "is_inf x y (Abs_dual (Rep_dual x || Rep_dual y))";
    5.67    by (stac Abs_dual_inverse' 1);
    5.68 -  by (safe_tac (claset()));
    5.69 -  br sup_ub1 1;
    5.70 -  br sup_ub2 1;
    5.71 -  br sup_lb_ubs 1;
    5.72 -  ba 1;
    5.73 -  ba 1;
    5.74 +  by Safe_tac;
    5.75 +  by (rtac sup_ub1 1);
    5.76 +  by (rtac sup_ub2 1);
    5.77 +  by (rtac sup_lb_ubs 1);
    5.78 +  by (assume_tac 1);
    5.79 +  by (assume_tac 1);
    5.80  qed "dual_is_inf";
    5.81  
    5.82  goalw thy [is_sup_def, le_dual_def] "is_sup x y (Abs_dual (Rep_dual x && Rep_dual y))";
    5.83    by (stac Abs_dual_inverse' 1);
    5.84 -  by (safe_tac (claset()));
    5.85 -  br inf_lb1 1;
    5.86 -  br inf_lb2 1;
    5.87 -  br inf_ub_lbs 1;
    5.88 -  ba 1;
    5.89 -  ba 1;
    5.90 +  by Safe_tac;
    5.91 +  by (rtac inf_lb1 1);
    5.92 +  by (rtac inf_lb2 1);
    5.93 +  by (rtac inf_ub_lbs 1);
    5.94 +  by (assume_tac 1);
    5.95 +  by (assume_tac 1);
    5.96  qed "dual_is_sup";
     6.1 --- a/src/HOL/AxClasses/Lattice/Lattice.ML	Wed Nov 05 13:14:15 1997 +0100
     6.2 +++ b/src/HOL/AxClasses/Lattice/Lattice.ML	Wed Nov 05 13:23:46 1997 +0100
     6.3 @@ -7,46 +7,46 @@
     6.4  (* unique existence *)
     6.5  
     6.6  goalw thy [inf_def] "is_inf x y (x && y)";
     6.7 -  br (ex_inf RS spec RS spec RS selectI1) 1;
     6.8 +  by (rtac (ex_inf RS spec RS spec RS selectI1) 1);
     6.9  qed "inf_is_inf";
    6.10  
    6.11  goal thy "is_inf x y inf --> x && y = inf";
    6.12 -  br impI 1;
    6.13 -  br (is_inf_uniq RS mp) 1;
    6.14 -  br conjI 1;
    6.15 -  br inf_is_inf 1;
    6.16 -  ba 1;
    6.17 +  by (rtac impI 1);
    6.18 +  by (rtac (is_inf_uniq RS mp) 1);
    6.19 +  by (rtac conjI 1);
    6.20 +  by (rtac inf_is_inf 1);
    6.21 +  by (assume_tac 1);
    6.22  qed "inf_uniq";
    6.23  
    6.24  goalw thy [Ex1_def] "ALL x y. EX! inf::'a::lattice. is_inf x y inf";
    6.25 -  by (safe_tac (claset()));
    6.26 +  by Safe_tac;
    6.27    by (Step_tac 1);
    6.28    by (Step_tac 1);
    6.29 -  br inf_is_inf 1;
    6.30 -  br (inf_uniq RS mp RS sym) 1;
    6.31 -  ba 1;
    6.32 +  by (rtac inf_is_inf 1);
    6.33 +  by (rtac (inf_uniq RS mp RS sym) 1);
    6.34 +  by (assume_tac 1);
    6.35  qed "ex1_inf";
    6.36  
    6.37  
    6.38  goalw thy [sup_def] "is_sup x y (x || y)";
    6.39 -  br (ex_sup RS spec RS spec RS selectI1) 1;
    6.40 +  by (rtac (ex_sup RS spec RS spec RS selectI1) 1);
    6.41  qed "sup_is_sup";
    6.42  
    6.43  goal thy "is_sup x y sup --> x || y = sup";
    6.44 -  br impI 1;
    6.45 -  br (is_sup_uniq RS mp) 1;
    6.46 -  br conjI 1;
    6.47 -  br sup_is_sup 1;
    6.48 -  ba 1;
    6.49 +  by (rtac impI 1);
    6.50 +  by (rtac (is_sup_uniq RS mp) 1);
    6.51 +  by (rtac conjI 1);
    6.52 +  by (rtac sup_is_sup 1);
    6.53 +  by (assume_tac 1);
    6.54  qed "sup_uniq";
    6.55  
    6.56  goalw thy [Ex1_def] "ALL x y. EX! sup::'a::lattice. is_sup x y sup";
    6.57 -  by (safe_tac (claset()));
    6.58 +  by Safe_tac;
    6.59    by (Step_tac 1);
    6.60    by (Step_tac 1);
    6.61 -  br sup_is_sup 1;
    6.62 -  br (sup_uniq RS mp RS sym) 1;
    6.63 -  ba 1;
    6.64 +  by (rtac sup_is_sup 1);
    6.65 +  by (rtac (sup_uniq RS mp RS sym) 1);
    6.66 +  by (assume_tac 1);
    6.67  qed "ex1_sup";
    6.68  
    6.69  
    6.70 @@ -96,30 +96,30 @@
    6.71  (* the Connection Theorems: "[=" expressed via "&&" or "||" *)
    6.72  
    6.73  goal thy "(x && y = x) = (x [= y)";
    6.74 -  br iffI 1;
    6.75 +  by (rtac iffI 1);
    6.76    (*==>*)
    6.77 -    be subst 1;
    6.78 -    br inf_lb2 1;
    6.79 +    by (etac subst 1);
    6.80 +    by (rtac inf_lb2 1);
    6.81    (*<==*)
    6.82 -    br (inf_uniq RS mp) 1;
    6.83 +    by (rtac (inf_uniq RS mp) 1);
    6.84      by (rewtac is_inf_def);
    6.85      by (REPEAT_FIRST (rtac conjI));
    6.86 -    br le_refl 1;
    6.87 -    ba 1;
    6.88 +    by (rtac le_refl 1);
    6.89 +    by (assume_tac 1);
    6.90      by (Fast_tac 1);
    6.91  qed "inf_connect";
    6.92  
    6.93  goal thy "(x || y = y) = (x [= y)";
    6.94 -  br iffI 1;
    6.95 +  by (rtac iffI 1);
    6.96    (*==>*)
    6.97 -    be subst 1;
    6.98 -    br sup_ub1 1;
    6.99 +    by (etac subst 1);
   6.100 +    by (rtac sup_ub1 1);
   6.101    (*<==*)
   6.102 -    br (sup_uniq RS mp) 1;
   6.103 +    by (rtac (sup_uniq RS mp) 1);
   6.104      by (rewtac is_sup_def);
   6.105      by (REPEAT_FIRST (rtac conjI));
   6.106 -    ba 1;
   6.107 -    br le_refl 1;
   6.108 +    by (assume_tac 1);
   6.109 +    by (rtac le_refl 1);
   6.110      by (Fast_tac 1);
   6.111  qed "sup_connect";
   6.112  
   6.113 @@ -127,37 +127,37 @@
   6.114  (* minorized infs / majorized sups *)
   6.115  
   6.116  goal thy "(x [= y && z) = (x [= y & x [= z)";
   6.117 -  br iffI 1;
   6.118 +  by (rtac iffI 1);
   6.119    (*==> (level 1)*)
   6.120      by (cut_facts_tac [inf_lb1, inf_lb2] 1);
   6.121 -    br conjI 1;
   6.122 -    br (le_trans RS mp) 1;
   6.123 -    be conjI 1;
   6.124 -    ba 1;
   6.125 -    br (le_trans RS mp) 1;
   6.126 -    be conjI 1;
   6.127 -    ba 1;
   6.128 +    by (rtac conjI 1);
   6.129 +    by (rtac (le_trans RS mp) 1);
   6.130 +    by (etac conjI 1);
   6.131 +    by (assume_tac 1);
   6.132 +    by (rtac (le_trans RS mp) 1);
   6.133 +    by (etac conjI 1);
   6.134 +    by (assume_tac 1);
   6.135    (*<== (level 9)*)
   6.136 -    be conjE 1;
   6.137 -    be inf_ub_lbs 1;
   6.138 -    ba 1;
   6.139 +    by (etac conjE 1);
   6.140 +    by (etac inf_ub_lbs 1);
   6.141 +    by (assume_tac 1);
   6.142  qed "le_inf_eq";
   6.143  
   6.144  goal thy "(x || y [= z) = (x [= z & y [= z)";
   6.145 -  br iffI 1;
   6.146 +  by (rtac iffI 1);
   6.147    (*==> (level 1)*)
   6.148      by (cut_facts_tac [sup_ub1, sup_ub2] 1);
   6.149 -    br conjI 1;
   6.150 -    br (le_trans RS mp) 1;
   6.151 -    be conjI 1;
   6.152 -    ba 1;
   6.153 -    br (le_trans RS mp) 1;
   6.154 -    be conjI 1;
   6.155 -    ba 1;
   6.156 +    by (rtac conjI 1);
   6.157 +    by (rtac (le_trans RS mp) 1);
   6.158 +    by (etac conjI 1);
   6.159 +    by (assume_tac 1);
   6.160 +    by (rtac (le_trans RS mp) 1);
   6.161 +    by (etac conjI 1);
   6.162 +    by (assume_tac 1);
   6.163    (*<== (level 9)*)
   6.164 -    be conjE 1;
   6.165 -    be sup_lb_ubs 1;
   6.166 -    ba 1;
   6.167 +    by (etac conjE 1);
   6.168 +    by (etac sup_lb_ubs 1);
   6.169 +    by (assume_tac 1);
   6.170  qed "ge_sup_eq";
   6.171  
   6.172  
   6.173 @@ -175,8 +175,8 @@
   6.174    back();
   6.175    back();
   6.176    back();
   6.177 -  br refl 2;
   6.178 -  br (is_inf_assoc RS mp) 1;
   6.179 +  by (rtac refl 2);
   6.180 +  by (rtac (is_inf_assoc RS mp) 1);
   6.181    by (REPEAT_FIRST (rtac conjI));
   6.182    by (REPEAT_FIRST (rtac inf_is_inf));
   6.183  qed "inf_assoc";
   6.184 @@ -191,8 +191,8 @@
   6.185    back();
   6.186    back();
   6.187    back();
   6.188 -  br refl 2;
   6.189 -  br (is_sup_assoc RS mp) 1;
   6.190 +  by (rtac refl 2);
   6.191 +  by (rtac (is_sup_assoc RS mp) 1);
   6.192    by (REPEAT_FIRST (rtac conjI));
   6.193    by (REPEAT_FIRST (rtac sup_is_sup));
   6.194  qed "sup_assoc";
   6.195 @@ -202,12 +202,12 @@
   6.196  
   6.197  goalw thy [inf_def] "x && y = y && x";
   6.198    by (stac (is_inf_commut RS ext) 1);
   6.199 -  br refl 1;
   6.200 +  by (rtac refl 1);
   6.201  qed "inf_commut";
   6.202  
   6.203  goalw thy [sup_def] "x || y = y || x";
   6.204    by (stac (is_sup_commut RS ext) 1);
   6.205 -  br refl 1;
   6.206 +  by (rtac refl 1);
   6.207  qed "sup_commut";
   6.208  
   6.209  
   6.210 @@ -215,12 +215,12 @@
   6.211  
   6.212  goal thy "x && x = x";
   6.213    by (stac inf_connect 1);
   6.214 -  br le_refl 1;
   6.215 +  by (rtac le_refl 1);
   6.216  qed "inf_idemp";
   6.217  
   6.218  goal thy "x || x = x";
   6.219    by (stac sup_connect 1);
   6.220 -  br le_refl 1;
   6.221 +  by (rtac le_refl 1);
   6.222  qed "sup_idemp";
   6.223  
   6.224  
   6.225 @@ -229,12 +229,12 @@
   6.226  goal thy "x || (x && y) = x";
   6.227    by (stac sup_commut 1);
   6.228    by (stac sup_connect 1);
   6.229 -  br inf_lb1 1;
   6.230 +  by (rtac inf_lb1 1);
   6.231  qed "sup_inf_absorb";
   6.232  
   6.233  goal thy "x && (x || y) = x";
   6.234    by (stac inf_connect 1);
   6.235 -  br sup_ub1 1;
   6.236 +  by (rtac sup_ub1 1);
   6.237  qed "inf_sup_absorb";
   6.238  
   6.239  
   6.240 @@ -243,27 +243,27 @@
   6.241  val prems = goal thy "[| a [= b; x [= y |] ==> a && x [= b && y";
   6.242    by (cut_facts_tac prems 1);
   6.243    by (stac le_inf_eq 1);
   6.244 -  br conjI 1;
   6.245 -  br (le_trans RS mp) 1;
   6.246 -  br conjI 1;
   6.247 -  br inf_lb1 1;
   6.248 -  ba 1;
   6.249 -  br (le_trans RS mp) 1;
   6.250 -  br conjI 1;
   6.251 -  br inf_lb2 1;
   6.252 -  ba 1;
   6.253 +  by (rtac conjI 1);
   6.254 +  by (rtac (le_trans RS mp) 1);
   6.255 +  by (rtac conjI 1);
   6.256 +  by (rtac inf_lb1 1);
   6.257 +  by (assume_tac 1);
   6.258 +  by (rtac (le_trans RS mp) 1);
   6.259 +  by (rtac conjI 1);
   6.260 +  by (rtac inf_lb2 1);
   6.261 +  by (assume_tac 1);
   6.262  qed "inf_mon";
   6.263  
   6.264  val prems = goal thy "[| a [= b; x [= y |] ==> a || x [= b || y";
   6.265    by (cut_facts_tac prems 1);
   6.266    by (stac ge_sup_eq 1);
   6.267 -  br conjI 1;
   6.268 -  br (le_trans RS mp) 1;
   6.269 -  br conjI 1;
   6.270 -  ba 1;
   6.271 -  br sup_ub1 1;
   6.272 -  br (le_trans RS mp) 1;
   6.273 -  br conjI 1;
   6.274 -  ba 1;
   6.275 -  br sup_ub2 1;
   6.276 +  by (rtac conjI 1);
   6.277 +  by (rtac (le_trans RS mp) 1);
   6.278 +  by (rtac conjI 1);
   6.279 +  by (assume_tac 1);
   6.280 +  by (rtac sup_ub1 1);
   6.281 +  by (rtac (le_trans RS mp) 1);
   6.282 +  by (rtac conjI 1);
   6.283 +  by (assume_tac 1);
   6.284 +  by (rtac sup_ub2 1);
   6.285  qed "sup_mon";
     7.1 --- a/src/HOL/AxClasses/Lattice/OrdDefs.ML	Wed Nov 05 13:14:15 1997 +0100
     7.2 +++ b/src/HOL/AxClasses/Lattice/OrdDefs.ML	Wed Nov 05 13:23:46 1997 +0100
     7.3 @@ -7,47 +7,47 @@
     7.4  (* pairs *)
     7.5  
     7.6  goalw thy [le_prod_def] "x [= (x::'a::quasi_order*'b::quasi_order)";
     7.7 -  br conjI 1;
     7.8 -  br le_refl 1;
     7.9 -  br le_refl 1;
    7.10 +  by (rtac conjI 1);
    7.11 +  by (rtac le_refl 1);
    7.12 +  by (rtac le_refl 1);
    7.13  qed "le_prod_refl";
    7.14  
    7.15  goalw thy [le_prod_def] "x [= y & y [= z --> x [= (z::'a::quasi_order*'b::quasi_order)";
    7.16 -  by (safe_tac (claset()));
    7.17 -  be (conjI RS (le_trans RS mp)) 1;
    7.18 -  ba 1;
    7.19 -  be (conjI RS (le_trans RS mp)) 1;
    7.20 -  ba 1;
    7.21 +  by Safe_tac;
    7.22 +  by (etac (conjI RS (le_trans RS mp)) 1);
    7.23 +  by (assume_tac 1);
    7.24 +  by (etac (conjI RS (le_trans RS mp)) 1);
    7.25 +  by (assume_tac 1);
    7.26  qed "le_prod_trans";
    7.27  
    7.28  goalw thy [le_prod_def] "x [= y & y [= x --> x = (y::'a::partial_order*'b::partial_order)";
    7.29 -  by (safe_tac (claset()));
    7.30 +  by Safe_tac;
    7.31    by (stac Pair_fst_snd_eq 1);
    7.32 -  br conjI 1;
    7.33 -  be (conjI RS (le_antisym RS mp)) 1;
    7.34 -  ba 1;
    7.35 -  be (conjI RS (le_antisym RS mp)) 1;
    7.36 -  ba 1;
    7.37 +  by (rtac conjI 1);
    7.38 +  by (etac (conjI RS (le_antisym RS mp)) 1);
    7.39 +  by (assume_tac 1);
    7.40 +  by (etac (conjI RS (le_antisym RS mp)) 1);
    7.41 +  by (assume_tac 1);
    7.42  qed "le_prod_antisym";
    7.43  
    7.44  
    7.45  (* functions *)
    7.46  
    7.47  goalw thy [le_fun_def] "f [= (f::'a=>'b::quasi_order)";
    7.48 -  br allI 1;
    7.49 -  br le_refl 1;
    7.50 +  by (rtac allI 1);
    7.51 +  by (rtac le_refl 1);
    7.52  qed "le_fun_refl";
    7.53  
    7.54  goalw thy [le_fun_def] "f [= g & g [= h --> f [= (h::'a=>'b::quasi_order)";
    7.55 -  by (safe_tac (claset()));
    7.56 -  br (le_trans RS mp) 1;
    7.57 +  by Safe_tac;
    7.58 +  by (rtac (le_trans RS mp) 1);
    7.59    by (Fast_tac 1);
    7.60  qed "le_fun_trans";
    7.61  
    7.62  goalw thy [le_fun_def] "f [= g & g [= f --> f = (g::'a=>'b::partial_order)";
    7.63 -  by (safe_tac (claset()));
    7.64 -  br ext 1;
    7.65 -  br (le_antisym RS mp) 1;
    7.66 +  by Safe_tac;
    7.67 +  by (rtac ext 1);
    7.68 +  by (rtac (le_antisym RS mp) 1);
    7.69    by (Fast_tac 1);
    7.70  qed "le_fun_antisym";
    7.71  
    7.72 @@ -57,32 +57,32 @@
    7.73  
    7.74  (*"'a dual" is even an isotype*)
    7.75  goal thy "Rep_dual (Abs_dual y) = y";
    7.76 -  br Abs_dual_inverse 1;
    7.77 +  by (rtac Abs_dual_inverse 1);
    7.78    by (rewtac dual_def);
    7.79    by (Fast_tac 1);
    7.80  qed "Abs_dual_inverse'";
    7.81  
    7.82  
    7.83  goalw thy [le_dual_def] "x [= (x::'a::quasi_order dual)";
    7.84 -  br le_refl 1;
    7.85 +  by (rtac le_refl 1);
    7.86  qed "le_dual_refl";
    7.87  
    7.88  goalw thy [le_dual_def] "x [= y & y [= z --> x [= (z::'a::quasi_order dual)";
    7.89    by (stac conj_commut 1);
    7.90 -  br le_trans 1;
    7.91 +  by (rtac le_trans 1);
    7.92  qed "le_dual_trans";
    7.93  
    7.94  goalw thy [le_dual_def] "x [= y & y [= x --> x = (y::'a::partial_order dual)";
    7.95 -  by (safe_tac (claset()));
    7.96 -  br (Rep_dual_inverse RS subst) 1;
    7.97 -  br sym 1;
    7.98 -  br (Rep_dual_inverse RS subst) 1;
    7.99 -  br arg_cong 1;
   7.100 +  by Safe_tac;
   7.101 +  by (rtac (Rep_dual_inverse RS subst) 1);
   7.102 +  by (rtac sym 1);
   7.103 +  by (rtac (Rep_dual_inverse RS subst) 1);
   7.104 +  by (rtac arg_cong 1);
   7.105    back();
   7.106 -  be (conjI RS (le_antisym RS mp)) 1;
   7.107 -  ba 1;
   7.108 +  by (etac (conjI RS (le_antisym RS mp)) 1);
   7.109 +  by (assume_tac 1);
   7.110  qed "le_dual_antisym";
   7.111  
   7.112  goalw thy [le_dual_def] "x [= y | y [= (x::'a::linear_order dual)";
   7.113 -  br le_linear 1;
   7.114 +  by (rtac le_linear 1);
   7.115  qed "le_dual_linear";
     8.1 --- a/src/HOL/AxClasses/Lattice/Order.ML	Wed Nov 05 13:14:15 1997 +0100
     8.2 +++ b/src/HOL/AxClasses/Lattice/Order.ML	Wed Nov 05 13:23:46 1997 +0100
     8.3 @@ -45,70 +45,70 @@
     8.4  (* associativity *)
     8.5  
     8.6  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";
     8.7 -  by (safe_tac (claset()));
     8.8 +  by Safe_tac;
     8.9    (*level 1*)
    8.10 -    br (le_trans RS mp) 1;
    8.11 -    be conjI 1;
    8.12 -    ba 1;
    8.13 +    by (rtac (le_trans RS mp) 1);
    8.14 +    by (etac conjI 1);
    8.15 +    by (assume_tac 1);
    8.16    (*level 4*)
    8.17      by (Step_tac 1);
    8.18      back();
    8.19 -    be mp 1;
    8.20 -    br conjI 1;
    8.21 -    br (le_trans RS mp) 1;
    8.22 -    be conjI 1;
    8.23 -    ba 1;
    8.24 -    ba 1;
    8.25 +    by (etac mp 1);
    8.26 +    by (rtac conjI 1);
    8.27 +    by (rtac (le_trans RS mp) 1);
    8.28 +    by (etac conjI 1);
    8.29 +    by (assume_tac 1);
    8.30 +    by (assume_tac 1);
    8.31    (*level 11*)
    8.32      by (Step_tac 1);
    8.33      back();
    8.34      back();
    8.35 -    be mp 1;
    8.36 -    br conjI 1;
    8.37 +    by (etac mp 1);
    8.38 +    by (rtac conjI 1);
    8.39      by (Step_tac 1);
    8.40 -    be mp 1;
    8.41 -    be conjI 1;
    8.42 -    br (le_trans RS mp) 1;
    8.43 -    be conjI 1;
    8.44 -    ba 1;
    8.45 -    br (le_trans RS mp) 1;
    8.46 -    be conjI 1;
    8.47 +    by (etac mp 1);
    8.48 +    by (etac conjI 1);
    8.49 +    by (rtac (le_trans RS mp) 1);
    8.50 +    by (etac conjI 1);
    8.51 +    by (assume_tac 1);
    8.52 +    by (rtac (le_trans RS mp) 1);
    8.53 +    by (etac conjI 1);
    8.54      back();     (* !! *)
    8.55 -    ba 1;
    8.56 +    by (assume_tac 1);
    8.57  qed "is_inf_assoc";
    8.58  
    8.59  
    8.60  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";
    8.61 -  by (safe_tac (claset()));
    8.62 +  by Safe_tac;
    8.63    (*level 1*)
    8.64 -    br (le_trans RS mp) 1;
    8.65 -    be conjI 1;
    8.66 -    ba 1;
    8.67 +    by (rtac (le_trans RS mp) 1);
    8.68 +    by (etac conjI 1);
    8.69 +    by (assume_tac 1);
    8.70    (*level 4*)
    8.71      by (Step_tac 1);
    8.72      back();
    8.73 -    be mp 1;
    8.74 -    br conjI 1;
    8.75 -    br (le_trans RS mp) 1;
    8.76 -    be conjI 1;
    8.77 -    ba 1;
    8.78 -    ba 1;
    8.79 +    by (etac mp 1);
    8.80 +    by (rtac conjI 1);
    8.81 +    by (rtac (le_trans RS mp) 1);
    8.82 +    by (etac conjI 1);
    8.83 +    by (assume_tac 1);
    8.84 +    by (assume_tac 1);
    8.85    (*level 11*)
    8.86      by (Step_tac 1);
    8.87      back();
    8.88      back();
    8.89 -    be mp 1;
    8.90 -    br conjI 1;
    8.91 +    by (etac mp 1);
    8.92 +    by (rtac conjI 1);
    8.93      by (Step_tac 1);
    8.94 -    be mp 1;
    8.95 -    be conjI 1;
    8.96 -    br (le_trans RS mp) 1;
    8.97 -    be conjI 1;
    8.98 +    by (etac mp 1);
    8.99 +    by (etac conjI 1);
   8.100 +    by (rtac (le_trans RS mp) 1);
   8.101 +    by (etac conjI 1);
   8.102      back();     (* !! *)
   8.103 -    ba 1;
   8.104 -    br (le_trans RS mp) 1;
   8.105 -    be conjI 1;
   8.106 -    ba 1;
   8.107 +    by (assume_tac 1);
   8.108 +    by (rtac (le_trans RS mp) 1);
   8.109 +    by (etac conjI 1);
   8.110 +    by (assume_tac 1);
   8.111  qed "is_sup_assoc";
   8.112  
   8.113  
   8.114 @@ -118,15 +118,15 @@
   8.115    by (stac expand_if 1);
   8.116    by (REPEAT_FIRST (resolve_tac [conjI, impI]));
   8.117    (*case "x [= y"*)
   8.118 -    br le_refl 1;
   8.119 -    ba 1;
   8.120 +    by (rtac le_refl 1);
   8.121 +    by (assume_tac 1);
   8.122      by (Fast_tac 1);
   8.123    (*case "~ x [= y"*)
   8.124 -    br (le_linear RS disjE) 1;
   8.125 -    ba 1;
   8.126 -    be notE 1;
   8.127 -    ba 1;
   8.128 -    br le_refl 1;
   8.129 +    by (rtac (le_linear RS disjE) 1);
   8.130 +    by (assume_tac 1);
   8.131 +    by (etac notE 1);
   8.132 +    by (assume_tac 1);
   8.133 +    by (rtac le_refl 1);
   8.134      by (Fast_tac 1);
   8.135  qed "min_is_inf";
   8.136  
   8.137 @@ -134,15 +134,15 @@
   8.138    by (stac expand_if 1);
   8.139    by (REPEAT_FIRST (resolve_tac [conjI, impI]));
   8.140    (*case "x [= y"*)
   8.141 -    ba 1;
   8.142 -    br le_refl 1;
   8.143 +    by (assume_tac 1);
   8.144 +    by (rtac le_refl 1);
   8.145      by (Fast_tac 1);
   8.146    (*case "~ x [= y"*)
   8.147 -    br le_refl 1;
   8.148 -    br (le_linear RS disjE) 1;
   8.149 -    ba 1;
   8.150 -    be notE 1;
   8.151 -    ba 1;
   8.152 +    by (rtac le_refl 1);
   8.153 +    by (rtac (le_linear RS disjE) 1);
   8.154 +    by (assume_tac 1);
   8.155 +    by (etac notE 1);
   8.156 +    by (assume_tac 1);
   8.157      by (Fast_tac 1);
   8.158  qed "max_is_sup";
   8.159  
   8.160 @@ -151,23 +151,23 @@
   8.161  (** general vs. binary limits **)
   8.162  
   8.163  goalw thy [is_inf_def, is_Inf_def] "is_Inf {x, y} inf = is_inf x y inf";
   8.164 -  br iffI 1;
   8.165 +  by (rtac iffI 1);
   8.166    (*==>*)
   8.167      by (Fast_tac 1);
   8.168    (*<==*)
   8.169 -    by (safe_tac (claset()));
   8.170 +    by Safe_tac;
   8.171      by (Step_tac 1);
   8.172 -    be mp 1;
   8.173 +    by (etac mp 1);
   8.174      by (Fast_tac 1);
   8.175  qed "bin_is_Inf_eq";
   8.176  
   8.177  goalw thy [is_sup_def, is_Sup_def] "is_Sup {x, y} sup = is_sup x y sup";
   8.178 -  br iffI 1;
   8.179 +  by (rtac iffI 1);
   8.180    (*==>*)
   8.181      by (Fast_tac 1);
   8.182    (*<==*)
   8.183 -    by (safe_tac (claset()));
   8.184 +    by Safe_tac;
   8.185      by (Step_tac 1);
   8.186 -    be mp 1;
   8.187 +    by (etac mp 1);
   8.188      by (Fast_tac 1);
   8.189  qed "bin_is_Sup_eq";
     9.1 --- a/src/HOL/Finite.ML	Wed Nov 05 13:14:15 1997 +0100
     9.2 +++ b/src/HOL/Finite.ML	Wed Nov 05 13:23:46 1997 +0100
     9.3 @@ -154,8 +154,8 @@
     9.4  
     9.5  val [prem] = goal Finite.thy
     9.6   "finite A ==> (!a:A. finite(B a)) --> finite(UN a:A. B a)";
     9.7 -br (prem RS finite_induct) 1;
     9.8 -by(ALLGOALS Asm_simp_tac);
     9.9 +by (rtac (prem RS finite_induct) 1);
    9.10 +by (ALLGOALS Asm_simp_tac);
    9.11  bind_thm("finite_UnionI", ballI RSN (2, result() RS mp));
    9.12  Addsimps [finite_UnionI];
    9.13  
    9.14 @@ -163,7 +163,7 @@
    9.15  
    9.16  goalw Finite.thy [Sigma_def]
    9.17   "!!A. [| finite A; !a:A. finite(B a) |] ==> finite(SIGMA a:A. B a)";
    9.18 -by(blast_tac (claset() addSIs [finite_UnionI]) 1);
    9.19 +by (blast_tac (claset() addSIs [finite_UnionI]) 1);
    9.20  bind_thm("finite_SigmaI", ballI RSN (2,result()));
    9.21  Addsimps [finite_SigmaI];
    9.22  
    9.23 @@ -250,15 +250,15 @@
    9.24  by (etac equalityE 1);
    9.25  by (asm_full_simp_tac
    9.26       (simpset() addsimps [subset_insert,Collect_conv_insert, less_Suc_eq]) 1);
    9.27 -by (safe_tac (claset()));
    9.28 +by Safe_tac;
    9.29    by (Asm_full_simp_tac 1);
    9.30    by (res_inst_tac [("x","%i. if f i = f m then a else f i")] exI 1);
    9.31 -  by (SELECT_GOAL(safe_tac (claset()))1);
    9.32 +  by (SELECT_GOAL Safe_tac 1);
    9.33     by (subgoal_tac "x ~= f m" 1);
    9.34      by (Blast_tac 2);
    9.35     by (subgoal_tac "? k. f k = x & k<m" 1);
    9.36      by (Blast_tac 2);
    9.37 -   by (SELECT_GOAL(safe_tac (claset()))1);
    9.38 +   by (SELECT_GOAL Safe_tac 1);
    9.39     by (res_inst_tac [("x","k")] exI 1);
    9.40     by (Asm_simp_tac 1);
    9.41    by (simp_tac (simpset() addsplits [expand_if]) 1);
    9.42 @@ -267,18 +267,18 @@
    9.43   by (rotate_tac ~1 1);
    9.44   by (Asm_full_simp_tac 1);
    9.45   by (res_inst_tac [("x","%i. if f i = f m then a else f i")] exI 1);
    9.46 - by (SELECT_GOAL(safe_tac (claset()))1);
    9.47 + by (SELECT_GOAL Safe_tac 1);
    9.48    by (subgoal_tac "x ~= f m" 1);
    9.49     by (Blast_tac 2);
    9.50    by (subgoal_tac "? k. f k = x & k<m" 1);
    9.51     by (Blast_tac 2);
    9.52 -  by (SELECT_GOAL(safe_tac (claset()))1);
    9.53 +  by (SELECT_GOAL Safe_tac 1);
    9.54    by (res_inst_tac [("x","k")] exI 1);
    9.55    by (Asm_simp_tac 1);
    9.56   by (simp_tac (simpset() addsplits [expand_if]) 1);
    9.57   by (Blast_tac 1);
    9.58  by (res_inst_tac [("x","%j. if f j = f i then f m else f j")] exI 1);
    9.59 -by (SELECT_GOAL(safe_tac (claset()))1);
    9.60 +by (SELECT_GOAL Safe_tac 1);
    9.61   by (subgoal_tac "x ~= f i" 1);
    9.62    by (Blast_tac 2);
    9.63   by (case_tac "x = f m" 1);
    9.64 @@ -286,7 +286,7 @@
    9.65    by (Asm_simp_tac 1);
    9.66   by (subgoal_tac "? k. f k = x & k<m" 1);
    9.67    by (Blast_tac 2);
    9.68 - by (SELECT_GOAL(safe_tac (claset()))1);
    9.69 + by (SELECT_GOAL Safe_tac 1);
    9.70   by (res_inst_tac [("x","k")] exI 1);
    9.71   by (Asm_simp_tac 1);
    9.72  by (simp_tac (simpset() addsplits [expand_if]) 1);
    9.73 @@ -335,7 +335,7 @@
    9.74  by (Clarify_tac 1);
    9.75  by (case_tac "x:B" 1);
    9.76   by (dres_inst_tac [("A","B")] mk_disjoint_insert 1);
    9.77 - by (SELECT_GOAL(safe_tac (claset()))1);
    9.78 + by (SELECT_GOAL Safe_tac 1);
    9.79   by (rotate_tac ~1 1);
    9.80   by (asm_full_simp_tac (simpset() addsimps [subset_insert_iff,finite_subset]) 1);
    9.81  by (rotate_tac ~1 1);
    10.1 --- a/src/HOL/Hoare/Examples.ML	Wed Nov 05 13:14:15 1997 +0100
    10.2 +++ b/src/HOL/Hoare/Examples.ML	Wed Nov 05 13:23:46 1997 +0100
    10.3 @@ -36,7 +36,7 @@
    10.4  
    10.5  by (hoare_tac 1);
    10.6  (*Now prove the verification conditions*)
    10.7 -by (safe_tac (claset()));
    10.8 +by Safe_tac;
    10.9  by (etac less_imp_diff_positive 1);
   10.10  by (asm_simp_tac (simpset() addsimps [less_imp_le, gcd_diff_r]) 1);
   10.11  by (asm_full_simp_tac (simpset() addsimps [not_less_iff_le, gcd_diff_l]) 2);
   10.12 @@ -67,7 +67,7 @@
   10.13  
   10.14  by (simp_tac ((simpset_of Arith.thy) addsimps [pow_0]) 3);
   10.15  
   10.16 -by (safe_tac (claset()));
   10.17 +by Safe_tac;
   10.18  
   10.19  by (subgoal_tac "a*a=a pow 2" 1);
   10.20  by (Asm_simp_tac 1);
   10.21 @@ -103,7 +103,7 @@
   10.22  \ {b = fac A}";
   10.23  
   10.24  by (hoare_tac 1);
   10.25 -by (safe_tac (claset()));
   10.26 +by Safe_tac;
   10.27  by (res_inst_tac [("n","a")] natE 1);
   10.28  by (ALLGOALS
   10.29      (asm_simp_tac
    11.1 --- a/src/HOL/Hoare/List_Examples.ML	Wed Nov 05 13:14:15 1997 +0100
    11.2 +++ b/src/HOL/Hoare/List_Examples.ML	Wed Nov 05 13:23:46 1997 +0100
    11.3 @@ -8,7 +8,7 @@
    11.4  \{y=rev(X)}";
    11.5  by (hoare_tac 1);
    11.6  by (asm_full_simp_tac (simpset() addsimps [neq_Nil_conv]) 1);
    11.7 -by (safe_tac (claset()));
    11.8 +by Safe_tac;
    11.9  by (Asm_full_simp_tac 1);
   11.10  by (Asm_full_simp_tac 1);
   11.11  qed "imperative_reverse";
   11.12 @@ -23,7 +23,7 @@
   11.13  \{y = X@Y}";
   11.14  by (hoare_tac 1);
   11.15  by (asm_full_simp_tac (simpset() addsimps [neq_Nil_conv]) 1);
   11.16 -by (safe_tac (claset()));
   11.17 +by Safe_tac;
   11.18  by (Asm_full_simp_tac 1);
   11.19  by (Asm_full_simp_tac 1);
   11.20  qed "imperative_append";
    12.1 --- a/src/HOL/IMP/Hoare.ML	Wed Nov 05 13:14:15 1997 +0100
    12.2 +++ b/src/HOL/IMP/Hoare.ML	Wed Nov 05 13:23:46 1997 +0100
    12.3 @@ -71,7 +71,7 @@
    12.4  by (rtac iffI 1);
    12.5   by (rtac weak_coinduct 1);
    12.6    by (etac CollectI 1);
    12.7 - by (safe_tac (claset()));
    12.8 + by Safe_tac;
    12.9    by (rotate_tac ~1 1);
   12.10    by (Asm_full_simp_tac 1);
   12.11   by (rotate_tac ~1 1);
    13.1 --- a/src/HOL/IMP/Transition.ML	Wed Nov 05 13:14:15 1997 +0100
    13.2 +++ b/src/HOL/IMP/Transition.ML	Wed Nov 05 13:23:46 1997 +0100
    13.3 @@ -87,7 +87,7 @@
    13.4  
    13.5  (* ASSIGN *)
    13.6  by (fast_tac (claset() addSDs [hlemma]  addSEs [rel_pow_E2]
    13.7 -                      addss simpset()) 1);
    13.8 +                       addss simpset()) 1);
    13.9  
   13.10  (* SEMI *)
   13.11  by (fast_tac (claset() addSDs [lemma2,rel_pow_imp_rtrancl]) 1);
   13.12 @@ -98,8 +98,7 @@
   13.13  by (fast_tac (claset() addSDs [rel_pow_imp_rtrancl]) 1);
   13.14  
   13.15  (* WHILE, induction on the length of the computation *)
   13.16 -by (rotate_tac 1 1);
   13.17 -by (etac rev_mp 1);
   13.18 +by (eres_inst_tac [("P","?X -n-> ?Y")] rev_mp 1);
   13.19  by (res_inst_tac [("x","s")] spec 1);
   13.20  by (res_inst_tac [("n","n")] less_induct 1);
   13.21  by (strip_tac 1);
    14.1 --- a/src/HOL/IOA/IOA.ML	Wed Nov 05 13:14:15 1997 +0100
    14.2 +++ b/src/HOL/IOA/IOA.ML	Wed Nov 05 13:23:46 1997 +0100
    14.3 @@ -55,7 +55,7 @@
    14.4  goalw IOA.thy (reachable_def::exec_rws)
    14.5  "!!A. [| reachable A s; (s,a,t) : trans_of(A) |] ==> reachable A t";
    14.6    by (asm_full_simp_tac (simpset() delsimps bex_simps) 1);
    14.7 -  by (safe_tac (claset()));
    14.8 +  by Safe_tac;
    14.9    by (res_inst_tac [("x","(%i. if i<n then fst ex i                    \
   14.10  \                            else (if i=n then Some a else None),    \
   14.11  \                         %i. if i<Suc n then snd ex i else t)")] bexI 1);
   14.12 @@ -77,13 +77,13 @@
   14.13  \     !!s t a. [|reachable A s; P(s)|] ==> (s,a,t): trans_of(A) --> P(t) |] \
   14.14  \  ==> invariant A P";
   14.15    by (rewrite_goals_tac(reachable_def::Let_def::exec_rws));
   14.16 -  by (safe_tac (claset()));
   14.17 +  by Safe_tac;
   14.18    by (res_inst_tac [("Q","reachable A (snd ex n)")] conjunct1 1);
   14.19    by (nat_ind_tac "n" 1);
   14.20    by (fast_tac (claset() addIs [p1,reachable_0]) 1);
   14.21    by (eres_inst_tac[("x","n")]allE 1);
   14.22    by (exhaust_tac "fst ex n" 1 THEN ALLGOALS Asm_full_simp_tac);
   14.23 -  by (safe_tac (claset()));
   14.24 +  by Safe_tac;
   14.25    by (etac (p2 RS mp) 1);
   14.26    by (ALLGOALS(fast_tac(claset() addDs [reachable_n])));
   14.27  qed "invariantI";
    15.1 --- a/src/HOL/IOA/Solve.ML	Wed Nov 05 13:14:15 1997 +0100
    15.2 +++ b/src/HOL/IOA/Solve.ML	Wed Nov 05 13:23:46 1997 +0100
    15.3 @@ -15,7 +15,7 @@
    15.4  \          is_weak_pmap f C A |] ==> traces(C) <= traces(A)";
    15.5  
    15.6    by (simp_tac(simpset() addsimps [has_trace_def])1);
    15.7 -  by (safe_tac (claset()));
    15.8 +  by Safe_tac;
    15.9  
   15.10    (* choose same trace, therefore same NF *)
   15.11    by (res_inst_tac[("x","mk_trace  C (fst ex)")] exI 1);
   15.12 @@ -32,7 +32,7 @@
   15.13  
   15.14    (* Now show that it's an execution *)
   15.15    by (asm_full_simp_tac(simpset() addsimps [executions_def]) 1);
   15.16 -  by (safe_tac (claset()));
   15.17 +  by Safe_tac;
   15.18  
   15.19    (* Start states map to start states *)
   15.20    by (dtac bspec 1);
   15.21 @@ -40,7 +40,7 @@
   15.22  
   15.23    (* Show that it's an execution fragment *)
   15.24    by (asm_full_simp_tac (simpset() addsimps [is_execution_fragment_def])1);
   15.25 -  by (safe_tac (claset()));
   15.26 +  by Safe_tac;
   15.27  
   15.28    by (eres_inst_tac [("x","snd ex n")] allE 1);
   15.29    by (eres_inst_tac [("x","snd ex (Suc n)")] allE 1);
   15.30 @@ -51,7 +51,7 @@
   15.31  (* Lemmata *)
   15.32  
   15.33  val prems = goal HOL.thy "(P ==> Q-->R) ==> P&Q --> R";
   15.34 -  by(fast_tac (claset() addDs prems) 1);
   15.35 +  by (fast_tac (claset() addDs prems) 1);
   15.36  val imp_conj_lemma = result();
   15.37  
   15.38  
   15.39 @@ -120,7 +120,7 @@
   15.40  by (simp_tac (simpset() addsimps [externals_of_par_extra]) 1);
   15.41  by (simp_tac (simpset() addsimps [par_def]) 1);
   15.42  by (asm_full_simp_tac (simpset() addsimps [trans_of_def]) 1);
   15.43 -by (rtac (expand_if RS ssubst) 1);
   15.44 +by (stac expand_if 1);
   15.45  by (rtac conjI 1);
   15.46  by (rtac impI 1); 
   15.47  by (etac disjE 1);
   15.48 @@ -142,7 +142,7 @@
   15.49  by (Fast_tac 2);
   15.50  by (simp_tac (simpset() addsimps [conj_disj_distribR] addcongs [conj_cong]
   15.51                   addsplits [expand_if]) 1);
   15.52 -by(REPEAT((resolve_tac [conjI,impI] 1 ORELSE etac conjE 1) THEN
   15.53 +by (REPEAT((resolve_tac [conjI,impI] 1 ORELSE etac conjE 1) THEN
   15.54          asm_full_simp_tac(simpset() addsimps[comp1_reachable,
   15.55                                        comp2_reachable])1));
   15.56  qed"fxg_is_weak_pmap_of_product_IOA";
   15.57 @@ -174,8 +174,8 @@
   15.58  by (rtac imp_conj_lemma 1);
   15.59  by (simp_tac (simpset() addsimps [rename_def]) 1);
   15.60  by (asm_full_simp_tac (simpset() addsimps [externals_def,asig_inputs_def,asig_outputs_def,asig_of_def,trans_of_def]) 1);
   15.61 -by (safe_tac (claset()));
   15.62 -by (rtac (expand_if RS ssubst) 1);
   15.63 +by Safe_tac;
   15.64 +by (stac expand_if 1);
   15.65   by (rtac conjI 1);
   15.66   by (rtac impI 1);
   15.67   by (etac disjE 1);
    16.1 --- a/src/HOL/MiniML/Generalize.ML	Wed Nov 05 13:14:15 1997 +0100
    16.2 +++ b/src/HOL/MiniML/Generalize.ML	Wed Nov 05 13:23:46 1997 +0100
    16.3 @@ -95,7 +95,7 @@
    16.4  
    16.5  goalw Generalize.thy [le_type_scheme_def,is_bound_typ_instance]
    16.6    "gen ($ S A) ($ S t) <= $ S (gen A t)";
    16.7 -by (safe_tac (claset()));
    16.8 +by Safe_tac;
    16.9  by (rename_tac "R" 1);
   16.10  by (res_inst_tac [("x", "(%a. bound_typ_inst R (gen ($S A) (S a)))")] exI 1);
   16.11  by (typ.induct_tac "t" 1);
   16.12 @@ -105,7 +105,7 @@
   16.13  
   16.14  goalw Generalize.thy [le_type_scheme_def,is_bound_typ_instance]
   16.15    "!!A B. free_tv B <= free_tv A ==> gen A t <= gen B t";
   16.16 -by (safe_tac (claset()));
   16.17 +by Safe_tac;
   16.18  by (rename_tac "S" 1);
   16.19  by (res_inst_tac [("x","%b. if b:free_tv A then TVar b else S b")] exI 1);
   16.20  by (typ.induct_tac "t" 1);
    17.1 --- a/src/HOL/MiniML/Instance.ML	Wed Nov 05 13:14:15 1997 +0100
    17.2 +++ b/src/HOL/MiniML/Instance.ML	Wed Nov 05 13:23:46 1997 +0100
    17.3 @@ -50,7 +50,7 @@
    17.4  \         (? S. !x:bound_tv sch. B x = mk_scheme (S x))";
    17.5  by (type_scheme.induct_tac "sch" 1);
    17.6  by (Simp_tac 1);
    17.7 -by (safe_tac (claset()));
    17.8 +by Safe_tac;
    17.9  by (rtac exI 1);
   17.10  by (rtac ballI 1);
   17.11  by (rtac sym 1);
   17.12 @@ -62,10 +62,10 @@
   17.13  by (dtac sym 1);
   17.14  by (dtac sym 1);
   17.15  by (REPEAT ((dtac mp 1) THEN (Fast_tac 1)));
   17.16 -by (safe_tac (claset()));
   17.17 +by Safe_tac;
   17.18  by (rename_tac "S1 S2" 1);
   17.19  by (res_inst_tac [("x","%x. if x:bound_tv type_scheme1 then (S1 x) else (S2 x)")] exI 1);
   17.20 -by (safe_tac (claset()));
   17.21 +by Safe_tac;
   17.22  by (asm_simp_tac (simpset() addsplits [expand_if]) 1);
   17.23  by (asm_simp_tac (simpset() addsplits [expand_if]) 1);
   17.24  by (strip_tac 1);
   17.25 @@ -123,7 +123,7 @@
   17.26  by (asm_full_simp_tac (simpset() addsimps [subst_to_scheme_inverse]) 1);
   17.27  by (res_inst_tac [("x","(subst_to_scheme (%k. if n <= k then BVar (k - n) else FVar k)) o S")] exI 1);
   17.28  by (asm_simp_tac (simpset() addsimps [aux2]) 1);
   17.29 -by (safe_tac (claset()));
   17.30 +by Safe_tac;
   17.31  by (res_inst_tac [("x","%n. bound_typ_inst S (B n)")] exI 1);
   17.32  by (type_scheme.induct_tac "sch" 1);
   17.33  by (Simp_tac 1);
   17.34 @@ -162,7 +162,7 @@
   17.35    "(sch # A <= sch' # B) = (sch <= (sch'::type_scheme) & A <= B)";
   17.36  by (Simp_tac 1);
   17.37  by (rtac iffI 1);
   17.38 - by (SELECT_GOAL(safe_tac (claset()))1);
   17.39 + by (SELECT_GOAL Safe_tac 1);
   17.40    by (eres_inst_tac [("x","0")] allE 1);
   17.41    by (Asm_full_simp_tac 1);
   17.42   by (eres_inst_tac [("x","Suc i")] allE 1);
   17.43 @@ -220,7 +220,7 @@
   17.44  by (type_scheme.induct_tac "sch" 1);
   17.45    by (Simp_tac 1);
   17.46   by (Simp_tac 1);
   17.47 - by (SELECT_GOAL(safe_tac(claset()))1);
   17.48 + by (SELECT_GOAL Safe_tac 1);
   17.49   by (eres_inst_tac [("x","TVar n -> TVar n")] allE 1);
   17.50   by (Asm_full_simp_tac 1);
   17.51   by (Fast_tac 1);
    18.1 --- a/src/HOL/MiniML/Type.ML	Wed Nov 05 13:14:15 1997 +0100
    18.2 +++ b/src/HOL/MiniML/Type.ML	Wed Nov 05 13:23:46 1997 +0100
    18.3 @@ -444,7 +444,7 @@
    18.4  (* all greater variables are also new *)
    18.5  goalw thy [new_tv_def] 
    18.6    "!!n m. n<=m ==> new_tv n t ==> new_tv m t";
    18.7 -by (safe_tac (claset()));
    18.8 +by Safe_tac;
    18.9  by (dtac spec 1);
   18.10  by (mp_tac 1);
   18.11  by (trans_tac 1);
   18.12 @@ -547,7 +547,7 @@
   18.13  
   18.14  goalw thy [max_def] "!!n::nat. m < n ==> m < max n n'";
   18.15  by (simp_tac (simpset() addsplits [expand_if]) 1);
   18.16 -by (safe_tac (claset()));
   18.17 +by Safe_tac;
   18.18  by (trans_tac 1);
   18.19  qed "less_maxL";
   18.20  
    19.1 --- a/src/HOL/NatDef.ML	Wed Nov 05 13:14:15 1997 +0100
    19.2 +++ b/src/HOL/NatDef.ML	Wed Nov 05 13:23:46 1997 +0100
    19.3 @@ -628,11 +628,11 @@
    19.4          hyp_subst_tac 1,
    19.5          rewtac Least_nat_def,
    19.6          rtac (select_equality RS arg_cong RS sym) 1,
    19.7 -        safe_tac (claset()),
    19.8 +        Safe_tac,
    19.9          dtac Suc_mono 1,
   19.10          Blast_tac 1,
   19.11          cut_facts_tac [less_linear] 1,
   19.12 -        safe_tac (claset()),
   19.13 +        Safe_tac,
   19.14          atac 2,
   19.15          Blast_tac 2,
   19.16          dtac Suc_mono 1,
    20.1 --- a/src/HOL/Subst/Unify.ML	Wed Nov 05 13:14:15 1997 +0100
    20.2 +++ b/src/HOL/Subst/Unify.ML	Wed Nov 05 13:23:46 1997 +0100
    20.3 @@ -225,7 +225,7 @@
    20.4  by (rotate_tac ~2 1);
    20.5  by (asm_full_simp_tac 
    20.6      (simpset() addsimps [MGUnifier_def, Unifier_def, MoreGeneral_def]) 1);
    20.7 -by (safe_tac (claset()) THEN rename_tac "theta sigma gamma" 1);
    20.8 +by (Safe_tac THEN rename_tac "theta sigma gamma" 1);
    20.9  by (eres_inst_tac [("x","gamma")] allE 1 THEN mp_tac 1);
   20.10  by (etac exE 1 THEN rename_tac "delta" 1);
   20.11  by (eres_inst_tac [("x","delta")] allE 1);
   20.12 @@ -248,7 +248,7 @@
   20.13         (simpset() addsimps [Var_Idem] 
   20.14  	         addsplits [expand_if,split_option_case])));
   20.15  (*Comb-Comb case*)
   20.16 -by (safe_tac (claset()));
   20.17 +by Safe_tac;
   20.18  by (REPEAT (dtac spec 1 THEN mp_tac 1));
   20.19  by (safe_tac (claset() addSDs [rewrite_rule [MGUnifier_def] unify_gives_MGU]));
   20.20  by (rtac Idem_comp 1);
    21.1 --- a/src/HOL/Trancl.ML	Wed Nov 05 13:14:15 1997 +0100
    21.2 +++ b/src/HOL/Trancl.ML	Wed Nov 05 13:23:46 1997 +0100
    21.3 @@ -78,7 +78,7 @@
    21.4  
    21.5  (*transitivity of transitive closure!! -- by induction.*)
    21.6  goalw Trancl.thy [trans_def] "trans(r^*)";
    21.7 -by (safe_tac (claset()));
    21.8 +by Safe_tac;
    21.9  by (eres_inst_tac [("b","z")] rtrancl_induct 1);
   21.10  by (ALLGOALS(blast_tac (claset() addIs [rtrancl_into_rtrancl])));
   21.11  qed "trans_rtrancl";
    22.1 --- a/src/HOL/Univ.ML	Wed Nov 05 13:14:15 1997 +0100
    22.2 +++ b/src/HOL/Univ.ML	Wed Nov 05 13:23:46 1997 +0100
    22.3 @@ -226,7 +226,7 @@
    22.4      "ndepth (Push_Node i n) = Suc(ndepth(n))";
    22.5  by (stac (Rep_Node RS Node_Push_I RS Abs_Node_inverse) 1);
    22.6  by (cut_facts_tac [rewrite_rule [Node_def] Rep_Node] 1);
    22.7 -by (safe_tac (claset()));
    22.8 +by Safe_tac;
    22.9  by (etac ssubst 1);  (*instantiates type variables!*)
   22.10  by (Simp_tac 1);
   22.11  by (rtac Least_equality 1);
   22.12 @@ -546,7 +546,7 @@
   22.13  (*Dependent version*)
   22.14  goal Univ.thy
   22.15      "(Sigma A B <**> Sigma C D) <= Sigma (A<*>C) (Split(%x y. B(x)<*>D(y)))";
   22.16 -by (safe_tac (claset()));
   22.17 +by Safe_tac;
   22.18  by (stac Split 1);
   22.19  by (Blast_tac 1);
   22.20  qed "dprod_subset_Sigma2";
    23.1 --- a/src/HOL/WF.ML	Wed Nov 05 13:14:15 1997 +0100
    23.2 +++ b/src/HOL/WF.ML	Wed Nov 05 13:23:46 1997 +0100
    23.3 @@ -111,7 +111,7 @@
    23.4   by (blast_tac (claset() addEs [wf_trancl RS wf_irrefl] addIs
    23.5        [rtrancl_into_trancl1,wf_subset,impOfSubs rtrancl_mono]) 1);
    23.6  by (asm_full_simp_tac (simpset() addsimps [wf_eq_minimal]) 1);
    23.7 -by (safe_tac (claset()));
    23.8 +by Safe_tac;
    23.9  by (EVERY1[rtac allE, atac, etac impE, Blast_tac]);
   23.10  by (etac bexE 1);
   23.11  by (rename_tac "a" 1);
   23.12 @@ -327,5 +327,5 @@
   23.13  
   23.14  goal WF.thy "!M R f. (f=wfrec R M) --> wf R --> (!x. f x = M (cut f R x) x)";
   23.15  by (Clarify_tac 1);
   23.16 -be wfrec 1;
   23.17 +by (etac wfrec 1);
   23.18  qed "tfl_wfrec";
    24.1 --- a/src/HOL/ex/MT.ML	Wed Nov 05 13:14:15 1997 +0100
    24.2 +++ b/src/HOL/ex/MT.ML	Wed Nov 05 13:23:46 1997 +0100
    24.3 @@ -230,7 +230,7 @@
    24.4  by (rtac eval_fun_mono 1);
    24.5  by (rewtac eval_fun_def);
    24.6  by (dtac CollectD 1);
    24.7 -by (safe_tac (claset()));
    24.8 +by Safe_tac;
    24.9  by (ALLGOALS (resolve_tac prems));
   24.10  by (ALLGOALS (Blast_tac));
   24.11  qed "eval_ind0";
   24.12 @@ -336,7 +336,7 @@
   24.13  by (rtac elab_fun_mono 1);
   24.14  by (rewtac elab_fun_def);
   24.15  by (dtac CollectD 1);
   24.16 -by (safe_tac (claset()));
   24.17 +by Safe_tac;
   24.18  by (ALLGOALS (resolve_tac prems));
   24.19  by (ALLGOALS (Blast_tac));
   24.20  qed "elab_ind0";
   24.21 @@ -387,7 +387,7 @@
   24.22  by (rtac elab_fun_mono 1);
   24.23  by (rewtac elab_fun_def);
   24.24  by (dtac CollectD 1);
   24.25 -by (safe_tac (claset()));
   24.26 +by Safe_tac;
   24.27  by (ALLGOALS (resolve_tac prems));
   24.28  by (ALLGOALS (Blast_tac));
   24.29  qed "elab_elim0";
   24.30 @@ -552,7 +552,7 @@
   24.31  by (rewtac hasty_fun_def);
   24.32  by (dtac CollectD 1);
   24.33  by (fold_goals_tac [hasty_fun_def]);
   24.34 -by (safe_tac (claset()));
   24.35 +by Safe_tac;
   24.36  by (REPEAT (ares_tac prems 1));
   24.37  qed "hasty_rel_elim0";
   24.38  
   24.39 @@ -690,7 +690,7 @@
   24.40  \   |] ==> \
   24.41  \   v_const(c_app c1 c2) hasty t";
   24.42  by (dtac elab_app_elim 1);
   24.43 -by (safe_tac (claset()));
   24.44 +by Safe_tac;
   24.45  by (rtac hasty_const 1);
   24.46  by (rtac isof_app 1);
   24.47  by (rtac hasty_elim_const 1);
   24.48 @@ -711,7 +711,7 @@
   24.49  \   |] ==> \
   24.50  \   v hasty t";
   24.51  by (dtac elab_app_elim 1);
   24.52 -by (safe_tac (claset()));
   24.53 +by Safe_tac;
   24.54  by ((etac allE 1) THEN (etac allE 1) THEN (etac impE 1));
   24.55  by (assume_tac 1);
   24.56  by (etac impE 1);
   24.57 @@ -721,7 +721,7 @@
   24.58  by (etac impE 1);
   24.59  by (assume_tac 1);
   24.60  by (dtac hasty_elim_clos 1);
   24.61 -by (safe_tac (claset()));
   24.62 +by Safe_tac;
   24.63  by (dtac elab_fn_elim 1);
   24.64  by (blast_tac (claset() addIs [hasty_env1] addSDs [t_fun_inj]) 1);
   24.65  qed "consistency_app2";
   24.66 @@ -733,7 +733,7 @@
   24.67  (* Proof by induction on the structure of evaluations *)
   24.68  
   24.69  by (rtac (major RS eval_ind) 1);
   24.70 -by (safe_tac (claset()));
   24.71 +by Safe_tac;
   24.72  by (DEPTH_SOLVE 
   24.73      (ares_tac [consistency_const, consistency_var, consistency_fn,
   24.74                 consistency_fix, consistency_app1, consistency_app2] 1));
   24.75 @@ -746,7 +746,7 @@
   24.76  val prems = goalw MT.thy [isof_env_def,hasty_env_def] 
   24.77    "ve isofenv te ==> ve hastyenv te";
   24.78  by (cut_facts_tac prems 1);
   24.79 -by (safe_tac (claset()));
   24.80 +by Safe_tac;
   24.81  by (etac allE 1);
   24.82  by (etac impE 1);
   24.83  by (assume_tac 1);
    25.1 --- a/src/HOL/ex/Primrec.ML	Wed Nov 05 13:14:15 1997 +0100
    25.2 +++ b/src/HOL/ex/Primrec.ML	Wed Nov 05 13:23:46 1997 +0100
    25.3 @@ -200,7 +200,7 @@
    25.4  \      ==> EX k. ALL l. list_add (map(%f. f l) fs) < ack(k, list_add l)";
    25.5  by (etac lists.induct 1);
    25.6  by (res_inst_tac [("x","0")] exI 1 THEN Asm_simp_tac 1);
    25.7 -by (safe_tac (claset()));
    25.8 +by Safe_tac;
    25.9  by (Asm_simp_tac 1);
   25.10  by (blast_tac (claset() addIs [add_less_mono, ack_add_bound, less_trans]) 1);
   25.11  qed "COMP_map_lemma";
    26.1 --- a/src/HOL/ex/cla.ML	Wed Nov 05 13:14:15 1997 +0100
    26.2 +++ b/src/HOL/ex/cla.ML	Wed Nov 05 13:23:46 1997 +0100
    26.3 @@ -381,7 +381,7 @@
    26.4    the type constraint ensures that x,y,z have the same type as a,b,u. *)
    26.5  goal HOL.thy "(? x y::'a. ! z. z=x | z=y) & P(a) & P(b) & (~a=b) \
    26.6  \               --> (! u::'a. P(u))";
    26.7 -by (Classical.safe_tac (claset()));
    26.8 +by (Classical.Safe_tac);
    26.9  by (res_inst_tac [("x","a")] allE 1);
   26.10  by (assume_tac 1);
   26.11  by (res_inst_tac [("x","b")] allE 1);
    27.1 --- a/src/HOL/ex/meson.ML	Wed Nov 05 13:14:15 1997 +0100
    27.2 +++ b/src/HOL/ex/meson.ML	Wed Nov 05 13:23:46 1997 +0100
    27.3 @@ -430,7 +430,7 @@
    27.4  
    27.5  (*First, breaks the goal into independent units*)
    27.6  val safe_best_meson_tac =
    27.7 -     SELECT_GOAL (TRY (safe_tac (claset())) THEN 
    27.8 +     SELECT_GOAL (TRY Safe_tac THEN 
    27.9                    TRYALL (best_meson_tac size_of_subgoals));
   27.10  
   27.11  (** Depth-first search version **)
   27.12 @@ -464,7 +464,7 @@
   27.13                             (prolog_step_tac' (make_horns cls))));
   27.14  
   27.15  val safe_meson_tac =
   27.16 -     SELECT_GOAL (TRY (safe_tac (claset())) THEN 
   27.17 +     SELECT_GOAL (TRY Safe_tac THEN 
   27.18                    TRYALL (iter_deepen_meson_tac));
   27.19  
   27.20  
    28.1 --- a/src/HOL/ex/set.ML	Wed Nov 05 13:14:15 1997 +0100
    28.2 +++ b/src/HOL/ex/set.ML	Wed Nov 05 13:23:46 1997 +0100
    28.3 @@ -9,15 +9,14 @@
    28.4  
    28.5  writeln"File HOL/ex/set.";
    28.6  
    28.7 -context Set.thy;
    28.8 +context Lfp.thy;
    28.9  
   28.10 -(*Nice demonstration of blast_tac--and its overloading problems*)
   28.11 +(*Nice demonstration of blast_tac--and its limitations*)
   28.12  goal Set.thy "!!S::'a set set. ALL x:S. ALL y:S. x<=y ==> EX z. S <= {z}";
   28.13 -let val insertCI' = read_instantiate [("'a", "?'a set")] insertCI
   28.14 -in    (*Type instantiation is required so that blast_tac can apply equalityI
   28.15 -        to the subgoal arising from insertCI*)
   28.16 -by(blast_tac (claset() addSIs [insertCI']) 1)
   28.17 -end;
   28.18 +(*for some unfathomable reason, UNIV_I increases the search space greatly*)
   28.19 +by (blast_tac (claset() delrules [UNIV_I]) 1);
   28.20 +result();
   28.21 +
   28.22  
   28.23  (*** A unique fixpoint theorem --- fast/best/meson all fail ***)
   28.24