Ran expandshort
authorpaulson
Mon Jun 23 10:42:03 1997 +0200 (1997-06-23)
changeset 3457a8ab7c64817c
parent 3456 fdb1768ebd3e
child 3458 5ff4bfab859c
Ran expandshort
src/HOL/Arith.ML
src/HOL/Divides.ML
src/HOL/Finite.ML
src/HOL/IMP/Denotation.ML
src/HOL/Induct/Com.ML
src/HOL/Integ/Equiv.ML
src/HOL/List.ML
src/HOL/Modelcheck/MCSyn.ML
src/HOL/NatDef.ML
src/HOL/Power.ML
src/HOL/Quot/HQUOT.ML
src/HOL/Quot/NPAIR.ML
src/HOL/Quot/PER.ML
src/HOL/Quot/PER0.ML
src/HOL/Subst/Subst.ML
src/HOL/Subst/Unifier.ML
src/HOL/Trancl.ML
src/HOL/WF.ML
src/HOL/WF_Rel.ML
src/HOL/equalities.ML
src/HOL/ex/Primes.ML
src/HOL/ex/Primrec.ML
src/HOLCF/IMP/Denotational.ML
src/HOLCF/IOA/meta_theory/Automata.ML
src/HOLCF/IOA/meta_theory/CompoExecs.ML
src/HOLCF/IOA/meta_theory/CompoScheds.ML
src/HOLCF/IOA/meta_theory/CompoTraces.ML
src/HOLCF/IOA/meta_theory/Compositionality.ML
src/HOLCF/IOA/meta_theory/Deadlock.ML
src/HOLCF/IOA/meta_theory/RefCorrectness.ML
src/HOLCF/IOA/meta_theory/RefMappings.ML
src/HOLCF/IOA/meta_theory/Seq.ML
src/HOLCF/IOA/meta_theory/Sequence.ML
src/HOLCF/IOA/meta_theory/ShortExecutions.ML
src/HOLCF/IOA/meta_theory/Traces.ML
src/HOLCF/Lift.ML
src/HOLCF/Lift3.ML
     1.1 --- a/src/HOL/Arith.ML	Mon Jun 23 10:35:49 1997 +0200
     1.2 +++ b/src/HOL/Arith.ML	Mon Jun 23 10:42:03 1997 +0200
     1.3 @@ -12,11 +12,11 @@
     1.4  (*** Basic rewrite rules for the arithmetic operators ***)
     1.5  
     1.6  goalw Arith.thy [pred_def] "pred 0 = 0";
     1.7 -by(Simp_tac 1);
     1.8 +by (Simp_tac 1);
     1.9  qed "pred_0";
    1.10  
    1.11  goalw Arith.thy [pred_def] "pred(Suc n) = n";
    1.12 -by(Simp_tac 1);
    1.13 +by (Simp_tac 1);
    1.14  qed "pred_Suc";
    1.15  
    1.16  Addsimps [pred_0,pred_Suc];
    1.17 @@ -175,8 +175,8 @@
    1.18  qed "add_lessD1";
    1.19  
    1.20  goal Arith.thy "!!i::nat. ~ (i+j < i)";
    1.21 -br notI 1;
    1.22 -be (add_lessD1 RS less_irrefl) 1;
    1.23 +by (rtac notI 1);
    1.24 +by (etac (add_lessD1 RS less_irrefl) 1);
    1.25  qed "not_add_less1";
    1.26  
    1.27  goal Arith.thy "!!i::nat. ~ (j+i < i)";
    1.28 @@ -506,7 +506,7 @@
    1.29  qed "mult_less_mono2";
    1.30  
    1.31  goal Arith.thy "!!i::nat. [| i<j; 0<k |] ==> i*k < j*k";
    1.32 -bd mult_less_mono2 1;
    1.33 +by (dtac mult_less_mono2 1);
    1.34  by (ALLGOALS (asm_full_simp_tac (!simpset addsimps [mult_commute])));
    1.35  qed "mult_less_mono1";
    1.36  
    1.37 @@ -531,21 +531,21 @@
    1.38  qed "mult_less_cancel2";
    1.39  
    1.40  goal Arith.thy "!!k. 0<k ==> (k*m < k*n) = (m<n)";
    1.41 -bd mult_less_cancel2 1;
    1.42 +by (dtac mult_less_cancel2 1);
    1.43  by (asm_full_simp_tac (!simpset addsimps [mult_commute]) 1);
    1.44  qed "mult_less_cancel1";
    1.45  Addsimps [mult_less_cancel1, mult_less_cancel2];
    1.46  
    1.47  goal Arith.thy "!!k. 0<k ==> (m*k = n*k) = (m=n)";
    1.48  by (cut_facts_tac [less_linear] 1);
    1.49 -by(Step_tac 1);
    1.50 -ba 2;
    1.51 +by (Step_tac 1);
    1.52 +by (assume_tac 2);
    1.53  by (ALLGOALS (dtac mult_less_mono1 THEN' assume_tac));
    1.54  by (ALLGOALS Asm_full_simp_tac);
    1.55  qed "mult_cancel2";
    1.56  
    1.57  goal Arith.thy "!!k. 0<k ==> (k*m = k*n) = (m=n)";
    1.58 -bd mult_cancel2 1;
    1.59 +by (dtac mult_cancel2 1);
    1.60  by (asm_full_simp_tac (!simpset addsimps [mult_commute]) 1);
    1.61  qed "mult_cancel1";
    1.62  Addsimps [mult_cancel1, mult_cancel2];
    1.63 @@ -574,13 +574,13 @@
    1.64  qed "diff_less_mono";
    1.65  
    1.66  goal Arith.thy "!! a b c::nat. a+b < c ==> a < c-b";
    1.67 -bd diff_less_mono 1;
    1.68 -br le_add2 1;
    1.69 +by (dtac diff_less_mono 1);
    1.70 +by (rtac le_add2 1);
    1.71  by (Asm_full_simp_tac 1);
    1.72  qed "add_less_imp_less_diff";
    1.73  
    1.74  goal Arith.thy "!! n. n <= m ==> Suc m - n = Suc (m - n)";
    1.75 -br Suc_diff_n 1;
    1.76 +by (rtac Suc_diff_n 1);
    1.77  by (asm_full_simp_tac (!simpset addsimps [le_eq_less_Suc]) 1);
    1.78  qed "Suc_diff_le";
    1.79  
    1.80 @@ -597,7 +597,7 @@
    1.81  Addsimps [diff_diff_cancel];
    1.82  
    1.83  goal Arith.thy "!!k::nat. k <= n ==> m <= n + m - k";
    1.84 -be rev_mp 1;
    1.85 +by (etac rev_mp 1);
    1.86  by (res_inst_tac [("m", "k"), ("n", "n")] diff_induct 1);
    1.87  by (Simp_tac 1);
    1.88  by (simp_tac (!simpset addsimps [less_add_Suc2, less_imp_le]) 1);
     2.1 --- a/src/HOL/Divides.ML	Mon Jun 23 10:35:49 1997 +0200
     2.2 +++ b/src/HOL/Divides.ML	Mon Jun 23 10:42:03 1997 +0200
     2.3 @@ -189,7 +189,7 @@
     2.4  
     2.5  goal thy "!!n. 0<n ==> m*n div n = m";
     2.6  by (cut_inst_tac [("m", "m*n")] mod_div_equality 1);
     2.7 -ba 1;
     2.8 +by (assume_tac 1);
     2.9  by (asm_full_simp_tac (!simpset addsimps [mod_mult_self_is_0]) 1);
    2.10  qed "div_mult_self_is_m";
    2.11  Addsimps [div_mult_self_is_m];
    2.12 @@ -264,7 +264,7 @@
    2.13  qed "dvd_diff";
    2.14  
    2.15  goal thy "!!k. [| k dvd (m-n); k dvd n; n<=m |] ==> k dvd m";
    2.16 -be (not_less_iff_le RS iffD2 RS add_diff_inverse RS subst) 1;
    2.17 +by (etac (not_less_iff_le RS iffD2 RS add_diff_inverse RS subst) 1);
    2.18  by (blast_tac (!claset addIs [dvd_add]) 1);
    2.19  qed "dvd_diffD";
    2.20  
    2.21 @@ -316,9 +316,9 @@
    2.22  goalw thy [dvd_def] "!!n. [| k dvd n; 0 < n |] ==> k <= n";
    2.23  by (Step_tac 1);
    2.24  by (ALLGOALS (full_simp_tac (!simpset addsimps [zero_less_mult_iff])));
    2.25 -be conjE 1;
    2.26 -br le_trans 1;
    2.27 -br (le_refl RS mult_le_mono) 2;
    2.28 +by (etac conjE 1);
    2.29 +by (rtac le_trans 1);
    2.30 +by (rtac (le_refl RS mult_le_mono) 2);
    2.31  by (etac Suc_leI 2);
    2.32  by (Simp_tac 1);
    2.33  qed "dvd_imp_le";
     3.1 --- a/src/HOL/Finite.ML	Mon Jun 23 10:35:49 1997 +0200
     3.2 +++ b/src/HOL/Finite.ML	Mon Jun 23 10:42:03 1997 +0200
     3.3 @@ -41,7 +41,7 @@
     3.4  \       !!F a. [| finite F; a:A; a ~: F;  P(F) |] ==> P(insert a F) \
     3.5  \    |] ==> F <= A --> P(F)";
     3.6  by (rtac (major RS finite_induct) 1);
     3.7 -by(ALLGOALS (blast_tac (!claset addIs prems)));
     3.8 +by (ALLGOALS (blast_tac (!claset addIs prems)));
     3.9  val lemma = result();
    3.10  
    3.11  val prems = goal Finite.thy 
    3.12 @@ -49,7 +49,7 @@
    3.13  \       P({}); \
    3.14  \       !!F a. [| finite F; a:A; a ~: F;  P(F) |] ==> P(insert a F) \
    3.15  \    |] ==> P(F)";
    3.16 -by(blast_tac (HOL_cs addIs ((lemma RS mp)::prems)) 1);
    3.17 +by (blast_tac (HOL_cs addIs ((lemma RS mp)::prems)) 1);
    3.18  qed "finite_subset_induct";
    3.19  
    3.20  Addsimps Finites.intrs;
    3.21 @@ -122,7 +122,7 @@
    3.22  
    3.23  goal Finite.thy "finite(A-{a}) = finite(A)";
    3.24  by (case_tac "a:A" 1);
    3.25 -br (finite_insert RS sym RS trans) 1;
    3.26 +by (rtac (finite_insert RS sym RS trans) 1);
    3.27  by (stac insert_Diff 1);
    3.28  by (ALLGOALS Asm_simp_tac);
    3.29  qed "finite_Diff_singleton";
    3.30 @@ -134,21 +134,21 @@
    3.31  by (Step_tac 1);
    3.32  by (subgoal_tac "EX y:A. f y = x & F = f``(A-{y})" 1);
    3.33   by (Step_tac 1);
    3.34 - bw inj_onto_def;
    3.35 + by (rewtac inj_onto_def);
    3.36   by (Blast_tac 1);
    3.37  by (thin_tac "ALL A. ?PP(A)" 1);
    3.38  by (forward_tac [[equalityD2, insertI1] MRS subsetD] 1);
    3.39  by (Step_tac 1);
    3.40  by (res_inst_tac [("x","xa")] bexI 1);
    3.41  by (ALLGOALS Asm_simp_tac);
    3.42 -be equalityE 1;
    3.43 -br equalityI 1;
    3.44 +by (etac equalityE 1);
    3.45 +by (rtac equalityI 1);
    3.46  by (Blast_tac 2);
    3.47  by (Best_tac 1);
    3.48  val lemma = result();
    3.49  
    3.50  goal Finite.thy "!!A. [| finite(f``A);  inj_onto f A |] ==> finite A";
    3.51 -bd lemma 1;
    3.52 +by (dtac lemma 1);
    3.53  by (Blast_tac 1);
    3.54  qed "finite_imageD";
    3.55  
    3.56 @@ -157,15 +157,15 @@
    3.57  
    3.58  goal Finite.thy "!!A. finite(Pow A) ==> finite A";
    3.59  by (subgoal_tac "finite ((%x.{x})``A)" 1);
    3.60 -br finite_subset 2;
    3.61 -ba 3;
    3.62 +by (rtac finite_subset 2);
    3.63 +by (assume_tac 3);
    3.64  by (ALLGOALS
    3.65      (fast_tac (!claset addSDs [rewrite_rule [inj_onto_def] finite_imageD])));
    3.66  val lemma = result();
    3.67  
    3.68  goal Finite.thy "finite(Pow A) = finite A";
    3.69 -br iffI 1;
    3.70 -be lemma 1;
    3.71 +by (rtac iffI 1);
    3.72 +by (etac lemma 1);
    3.73  (*Opposite inclusion: finite A ==> finite (Pow A) *)
    3.74  by (etac finite_induct 1);
    3.75  by (ALLGOALS 
    3.76 @@ -175,19 +175,19 @@
    3.77  AddIffs [finite_Pow_iff];
    3.78  
    3.79  goal Finite.thy "finite(r^-1) = finite r";
    3.80 -by(subgoal_tac "r^-1 = (%(x,y).(y,x))``r" 1);
    3.81 - by(Asm_simp_tac 1);
    3.82 - br iffI 1;
    3.83 -  be (rewrite_rule [inj_onto_def] finite_imageD) 1;
    3.84 -  by(simp_tac (!simpset setloop (split_tac[expand_split])) 1);
    3.85 - be finite_imageI 1;
    3.86 -by(simp_tac (!simpset addsimps [inverse_def,image_def]) 1);
    3.87 -by(Auto_tac());
    3.88 - br bexI 1;
    3.89 - ba 2;
    3.90 - by(Simp_tac 1);
    3.91 -by(split_all_tac 1);
    3.92 -by(Asm_full_simp_tac 1);
    3.93 +by (subgoal_tac "r^-1 = (%(x,y).(y,x))``r" 1);
    3.94 + by (Asm_simp_tac 1);
    3.95 + by (rtac iffI 1);
    3.96 +  by (etac (rewrite_rule [inj_onto_def] finite_imageD) 1);
    3.97 +  by (simp_tac (!simpset setloop (split_tac[expand_split])) 1);
    3.98 + by (etac finite_imageI 1);
    3.99 +by (simp_tac (!simpset addsimps [inverse_def,image_def]) 1);
   3.100 +by (Auto_tac());
   3.101 + by (rtac bexI 1);
   3.102 + by (assume_tac 2);
   3.103 + by (Simp_tac 1);
   3.104 +by (split_all_tac 1);
   3.105 +by (Asm_full_simp_tac 1);
   3.106  qed "finite_inverse";
   3.107  AddIffs [finite_inverse];
   3.108  
   3.109 @@ -249,7 +249,7 @@
   3.110     by (Asm_simp_tac 1);
   3.111    by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
   3.112    by (Blast_tac 1);
   3.113 - bd sym 1;
   3.114 + by (dtac sym 1);
   3.115   by (rotate_tac ~1 1);
   3.116   by (Asm_full_simp_tac 1);
   3.117   by (res_inst_tac [("x","%i. if f i = f m then a else f i")] exI 1);
   3.118 @@ -282,21 +282,21 @@
   3.119  goal Finite.thy "!!A. [| finite A; x ~: A |] ==> \
   3.120  \ (LEAST n. ? f. insert x A = {f i|i.i<n}) = Suc(LEAST n. ? f. A={f i|i.i<n})";
   3.121  by (rtac Least_equality 1);
   3.122 - bd finite_has_card 1;
   3.123 - be exE 1;
   3.124 + by (dtac finite_has_card 1);
   3.125 + by (etac exE 1);
   3.126   by (dres_inst_tac [("P","%n.? f. A={f i|i.i<n}")] LeastI 1);
   3.127 - be exE 1;
   3.128 + by (etac exE 1);
   3.129   by (res_inst_tac
   3.130     [("x","%i. if i<(LEAST n. ? f. A={f i |i. i < n}) then f i else x")] exI 1);
   3.131   by (simp_tac
   3.132      (!simpset addsimps [Collect_conv_insert, less_Suc_eq] 
   3.133                addcongs [rev_conj_cong]) 1);
   3.134 - be subst 1;
   3.135 - br refl 1;
   3.136 + by (etac subst 1);
   3.137 + by (rtac refl 1);
   3.138  by (rtac notI 1);
   3.139  by (etac exE 1);
   3.140  by (dtac lemma 1);
   3.141 - ba 1;
   3.142 + by (assume_tac 1);
   3.143  by (etac exE 1);
   3.144  by (etac conjE 1);
   3.145  by (dres_inst_tac [("P","%x. ? g. A = {g i |i. i < x}")] Least_le 1);
   3.146 @@ -339,9 +339,9 @@
   3.147  goal Finite.thy "!!A. [| finite A; B<=A |] ==> card A - card B = card (A - B)";
   3.148  by (subgoal_tac "(A-B) Un B = A" 1);
   3.149  by (Blast_tac 2);
   3.150 -br (add_right_cancel RS iffD1) 1;
   3.151 -br (card_Un_disjoint RS subst) 1;
   3.152 -be ssubst 4;
   3.153 +by (rtac (add_right_cancel RS iffD1) 1);
   3.154 +by (rtac (card_Un_disjoint RS subst) 1);
   3.155 +by (etac ssubst 4);
   3.156  by (Blast_tac 3);
   3.157  by (ALLGOALS 
   3.158      (asm_simp_tac
   3.159 @@ -382,7 +382,7 @@
   3.160  by (etac finite_induct 1);
   3.161  by (ALLGOALS Asm_simp_tac);
   3.162  by (Step_tac 1);
   3.163 -bw inj_onto_def;
   3.164 +by (rewtac inj_onto_def);
   3.165  by (Blast_tac 1);
   3.166  by (stac card_insert_disjoint 1);
   3.167  by (etac finite_imageI 1);
   3.168 @@ -397,7 +397,7 @@
   3.169  by (EVERY (map (blast_tac (!claset addIs [finite_imageI])) [3,2,1]));
   3.170  by (subgoal_tac "inj_onto (insert x) (Pow F)" 1);
   3.171  by (asm_simp_tac (!simpset addsimps [card_image, Pow_insert]) 1);
   3.172 -bw inj_onto_def;
   3.173 +by (rewtac inj_onto_def);
   3.174  by (blast_tac (!claset addSEs [equalityE]) 1);
   3.175  qed "card_Pow";
   3.176  Addsimps [card_Pow];
     4.1 --- a/src/HOL/IMP/Denotation.ML	Mon Jun 23 10:35:49 1997 +0200
     4.2 +++ b/src/HOL/IMP/Denotation.ML	Mon Jun 23 10:42:03 1997 +0200
     4.3 @@ -29,7 +29,7 @@
     4.4  
     4.5  (* start with rule induction *)
     4.6  by (etac evalc.induct 1);
     4.7 -auto();
     4.8 +by (Auto_tac());
     4.9  (* while *)
    4.10  by (rewtac Gamma_def);
    4.11  by (stac (rewrite_rule [Gamma_def] (Gamma_mono RS lfp_Tarski)) 1);
     5.1 --- a/src/HOL/Induct/Com.ML	Mon Jun 23 10:35:49 1997 +0200
     5.2 +++ b/src/HOL/Induct/Com.ML	Mon Jun 23 10:42:03 1997 +0200
     5.3 @@ -52,7 +52,7 @@
     5.4  qed "assign_different";
     5.5  
     5.6  goalw thy [assign_def] "s[s x/x] = s";
     5.7 -br ext 1;
     5.8 +by (rtac ext 1);
     5.9  by (simp_tac (!simpset setloop split_tac[expand_if]) 1);
    5.10  qed "assign_triv";
    5.11  
     6.1 --- a/src/HOL/Integ/Equiv.ML	Mon Jun 23 10:35:49 1997 +0200
     6.2 +++ b/src/HOL/Integ/Equiv.ML	Mon Jun 23 10:42:03 1997 +0200
     6.3 @@ -263,14 +263,14 @@
     6.4  goal thy "!!A. [| finite A; r <= A Times A |] ==> finite (A/r)";
     6.5  by (rtac finite_subset 1);
     6.6  by (etac (finite_Pow_iff RS iffD2) 2);
     6.7 -by (rewrite_goals_tac [quotient_def]);
     6.8 +by (rewtac quotient_def);
     6.9  by (Blast_tac 1);
    6.10  qed "finite_quotient";
    6.11  
    6.12  goalw thy [quotient_def]
    6.13      "!!A. [| finite A;  r <= A Times A;  X : A/r |] ==> finite X";
    6.14  by (rtac finite_subset 1);
    6.15 -ba 2;
    6.16 +by (assume_tac 2);
    6.17  by (Blast_tac 1);
    6.18  qed "finite_equiv_class";
    6.19  
     7.1 --- a/src/HOL/List.ML	Mon Jun 23 10:35:49 1997 +0200
     7.2 +++ b/src/HOL/List.ML	Mon Jun 23 10:42:03 1997 +0200
     7.3 @@ -38,8 +38,8 @@
     7.4  qed "expand_list_case";
     7.5  
     7.6  val prems = goal thy "[| P([]); !!x xs. P(x#xs) |] ==> P(xs)";
     7.7 -by(induct_tac "xs" 1);
     7.8 -by(REPEAT(resolve_tac prems 1));
     7.9 +by (induct_tac "xs" 1);
    7.10 +by (REPEAT(resolve_tac prems 1));
    7.11  qed "list_cases";
    7.12  
    7.13  goal thy  "(xs=[] --> P([])) & (!y ys. xs=y#ys --> P(y#ys)) --> P(xs)";
    7.14 @@ -73,7 +73,7 @@
    7.15  goal thy "([] = xs@ys) = (xs=[] & ys=[])";
    7.16  by (induct_tac "xs" 1);
    7.17  by (ALLGOALS Asm_simp_tac);
    7.18 -by(Blast_tac 1);
    7.19 +by (Blast_tac 1);
    7.20  qed "Nil_is_append_conv";
    7.21  AddIffs [Nil_is_append_conv];
    7.22  
    7.23 @@ -84,19 +84,19 @@
    7.24  AddIffs [same_append_eq];
    7.25  
    7.26  goal thy "!ys. (xs @ [x] = ys @ [y]) = (xs = ys & x = y)"; 
    7.27 -by(induct_tac "xs" 1);
    7.28 - br allI 1;
    7.29 - by(induct_tac "ys" 1);
    7.30 -  by(ALLGOALS Asm_simp_tac);
    7.31 -br allI 1;
    7.32 -by(induct_tac "ys" 1);
    7.33 - by(ALLGOALS Asm_simp_tac);
    7.34 +by (induct_tac "xs" 1);
    7.35 + by (rtac allI 1);
    7.36 + by (induct_tac "ys" 1);
    7.37 +  by (ALLGOALS Asm_simp_tac);
    7.38 +by (rtac allI 1);
    7.39 +by (induct_tac "ys" 1);
    7.40 + by (ALLGOALS Asm_simp_tac);
    7.41  qed_spec_mp "append1_eq_conv";
    7.42  AddIffs [append1_eq_conv];
    7.43  
    7.44  goal thy "xs ~= [] --> hd xs # tl xs = xs";
    7.45 -by(induct_tac "xs" 1);
    7.46 -by(ALLGOALS Asm_simp_tac);
    7.47 +by (induct_tac "xs" 1);
    7.48 +by (ALLGOALS Asm_simp_tac);
    7.49  qed_spec_mp "hd_Cons_tl";
    7.50  Addsimps [hd_Cons_tl];
    7.51  
    7.52 @@ -106,15 +106,15 @@
    7.53  qed "hd_append";
    7.54  
    7.55  goal thy "tl(xs@ys) = (case xs of [] => tl(ys) | z#zs => zs@ys)";
    7.56 -by(simp_tac (!simpset setloop(split_tac[expand_list_case])) 1);
    7.57 +by (simp_tac (!simpset setloop(split_tac[expand_list_case])) 1);
    7.58  qed "tl_append";
    7.59  
    7.60  (** map **)
    7.61  
    7.62  goal thy
    7.63    "(!x. x : set_of_list xs --> f x = g x) --> map f xs = map g xs";
    7.64 -by(induct_tac "xs" 1);
    7.65 -by(ALLGOALS Asm_simp_tac);
    7.66 +by (induct_tac "xs" 1);
    7.67 +by (ALLGOALS Asm_simp_tac);
    7.68  bind_thm("map_ext", impI RS (allI RS (result() RS mp)));
    7.69  
    7.70  goal thy "map (%x.x) = (%xs.xs)";
    7.71 @@ -190,20 +190,20 @@
    7.72  qed "set_of_list_subset_Cons";
    7.73  
    7.74  goal thy "(set_of_list xs = {}) = (xs = [])";
    7.75 -by(induct_tac "xs" 1);
    7.76 -by(ALLGOALS Asm_simp_tac);
    7.77 +by (induct_tac "xs" 1);
    7.78 +by (ALLGOALS Asm_simp_tac);
    7.79  qed "set_of_list_empty";
    7.80  Addsimps [set_of_list_empty];
    7.81  
    7.82  goal thy "set_of_list(rev xs) = set_of_list(xs)";
    7.83 -by(induct_tac "xs" 1);
    7.84 -by(ALLGOALS Asm_simp_tac);
    7.85 +by (induct_tac "xs" 1);
    7.86 +by (ALLGOALS Asm_simp_tac);
    7.87  qed "set_of_list_rev";
    7.88  Addsimps [set_of_list_rev];
    7.89  
    7.90  goal thy "set_of_list(map f xs) = f``(set_of_list xs)";
    7.91 -by(induct_tac "xs" 1);
    7.92 -by(ALLGOALS Asm_simp_tac);
    7.93 +by (induct_tac "xs" 1);
    7.94 +by (ALLGOALS Asm_simp_tac);
    7.95  qed "set_of_list_map";
    7.96  Addsimps [set_of_list_map];
    7.97  
    7.98 @@ -232,14 +232,14 @@
    7.99  (** filter **)
   7.100  
   7.101  goal thy "filter P (xs@ys) = filter P xs @ filter P ys";
   7.102 -by(induct_tac "xs" 1);
   7.103 - by(ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
   7.104 +by (induct_tac "xs" 1);
   7.105 + by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
   7.106  qed "filter_append";
   7.107  Addsimps [filter_append];
   7.108  
   7.109  goal thy "size (filter P xs) <= size xs";
   7.110 -by(induct_tac "xs" 1);
   7.111 - by(ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
   7.112 +by (induct_tac "xs" 1);
   7.113 + by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
   7.114  qed "filter_size";
   7.115  
   7.116  
   7.117 @@ -277,14 +277,14 @@
   7.118  Addsimps [length_rev];
   7.119  
   7.120  goal thy "(length xs = 0) = (xs = [])";
   7.121 -by(induct_tac "xs" 1);
   7.122 -by(ALLGOALS Asm_simp_tac);
   7.123 +by (induct_tac "xs" 1);
   7.124 +by (ALLGOALS Asm_simp_tac);
   7.125  qed "length_0_conv";
   7.126  AddIffs [length_0_conv];
   7.127  
   7.128  goal thy "(0 < length xs) = (xs ~= [])";
   7.129 -by(induct_tac "xs" 1);
   7.130 -by(ALLGOALS Asm_simp_tac);
   7.131 +by (induct_tac "xs" 1);
   7.132 +by (ALLGOALS Asm_simp_tac);
   7.133  qed "length_greater_0_conv";
   7.134  AddIffs [length_greater_0_conv];
   7.135  
   7.136 @@ -294,14 +294,14 @@
   7.137  goal thy
   7.138    "!xs. nth n (xs@ys) = \
   7.139  \          (if n < length xs then nth n xs else nth (n - length xs) ys)";
   7.140 -by(nat_ind_tac "n" 1);
   7.141 - by(Asm_simp_tac 1);
   7.142 - br allI 1;
   7.143 - by(exhaust_tac "xs" 1);
   7.144 -  by(ALLGOALS Asm_simp_tac);
   7.145 -br allI 1;
   7.146 -by(exhaust_tac "xs" 1);
   7.147 - by(ALLGOALS Asm_simp_tac);
   7.148 +by (nat_ind_tac "n" 1);
   7.149 + by (Asm_simp_tac 1);
   7.150 + by (rtac allI 1);
   7.151 + by (exhaust_tac "xs" 1);
   7.152 +  by (ALLGOALS Asm_simp_tac);
   7.153 +by (rtac allI 1);
   7.154 +by (exhaust_tac "xs" 1);
   7.155 + by (ALLGOALS Asm_simp_tac);
   7.156  qed_spec_mp "nth_append";
   7.157  
   7.158  goal thy "!n. n < length xs --> nth n (map f xs) = f (nth n xs)";
   7.159 @@ -365,118 +365,118 @@
   7.160  Addsimps [take_0,take_Suc_Cons,drop_0,drop_Suc_Cons];
   7.161  
   7.162  goal thy "!xs. length(take n xs) = min (length xs) n";
   7.163 -by(nat_ind_tac "n" 1);
   7.164 - by(ALLGOALS Asm_simp_tac);
   7.165 -br allI 1;
   7.166 -by(exhaust_tac "xs" 1);
   7.167 - by(ALLGOALS Asm_simp_tac);
   7.168 +by (nat_ind_tac "n" 1);
   7.169 + by (ALLGOALS Asm_simp_tac);
   7.170 +by (rtac allI 1);
   7.171 +by (exhaust_tac "xs" 1);
   7.172 + by (ALLGOALS Asm_simp_tac);
   7.173  qed_spec_mp "length_take";
   7.174  Addsimps [length_take];
   7.175  
   7.176  goal thy "!xs. length(drop n xs) = (length xs - n)";
   7.177 -by(nat_ind_tac "n" 1);
   7.178 - by(ALLGOALS Asm_simp_tac);
   7.179 -br allI 1;
   7.180 -by(exhaust_tac "xs" 1);
   7.181 - by(ALLGOALS Asm_simp_tac);
   7.182 +by (nat_ind_tac "n" 1);
   7.183 + by (ALLGOALS Asm_simp_tac);
   7.184 +by (rtac allI 1);
   7.185 +by (exhaust_tac "xs" 1);
   7.186 + by (ALLGOALS Asm_simp_tac);
   7.187  qed_spec_mp "length_drop";
   7.188  Addsimps [length_drop];
   7.189  
   7.190  goal thy "!xs. length xs <= n --> take n xs = xs";
   7.191 -by(nat_ind_tac "n" 1);
   7.192 - by(ALLGOALS Asm_simp_tac);
   7.193 -br allI 1;
   7.194 -by(exhaust_tac "xs" 1);
   7.195 - by(ALLGOALS Asm_simp_tac);
   7.196 +by (nat_ind_tac "n" 1);
   7.197 + by (ALLGOALS Asm_simp_tac);
   7.198 +by (rtac allI 1);
   7.199 +by (exhaust_tac "xs" 1);
   7.200 + by (ALLGOALS Asm_simp_tac);
   7.201  qed_spec_mp "take_all";
   7.202  
   7.203  goal thy "!xs. length xs <= n --> drop n xs = []";
   7.204 -by(nat_ind_tac "n" 1);
   7.205 - by(ALLGOALS Asm_simp_tac);
   7.206 -br allI 1;
   7.207 -by(exhaust_tac "xs" 1);
   7.208 - by(ALLGOALS Asm_simp_tac);
   7.209 +by (nat_ind_tac "n" 1);
   7.210 + by (ALLGOALS Asm_simp_tac);
   7.211 +by (rtac allI 1);
   7.212 +by (exhaust_tac "xs" 1);
   7.213 + by (ALLGOALS Asm_simp_tac);
   7.214  qed_spec_mp "drop_all";
   7.215  
   7.216  goal thy 
   7.217    "!xs. take n (xs @ ys) = (take n xs @ take (n - length xs) ys)";
   7.218 -by(nat_ind_tac "n" 1);
   7.219 - by(ALLGOALS Asm_simp_tac);
   7.220 -br allI 1;
   7.221 -by(exhaust_tac "xs" 1);
   7.222 - by(ALLGOALS Asm_simp_tac);
   7.223 +by (nat_ind_tac "n" 1);
   7.224 + by (ALLGOALS Asm_simp_tac);
   7.225 +by (rtac allI 1);
   7.226 +by (exhaust_tac "xs" 1);
   7.227 + by (ALLGOALS Asm_simp_tac);
   7.228  qed_spec_mp "take_append";
   7.229  Addsimps [take_append];
   7.230  
   7.231  goal thy "!xs. drop n (xs@ys) = drop n xs @ drop (n - length xs) ys"; 
   7.232 -by(nat_ind_tac "n" 1);
   7.233 - by(ALLGOALS Asm_simp_tac);
   7.234 -br allI 1;
   7.235 -by(exhaust_tac "xs" 1);
   7.236 - by(ALLGOALS Asm_simp_tac);
   7.237 +by (nat_ind_tac "n" 1);
   7.238 + by (ALLGOALS Asm_simp_tac);
   7.239 +by (rtac allI 1);
   7.240 +by (exhaust_tac "xs" 1);
   7.241 + by (ALLGOALS Asm_simp_tac);
   7.242  qed_spec_mp "drop_append";
   7.243  Addsimps [drop_append];
   7.244  
   7.245  goal thy "!xs n. take n (take m xs) = take (min n m) xs"; 
   7.246 -by(nat_ind_tac "m" 1);
   7.247 - by(ALLGOALS Asm_simp_tac);
   7.248 -br allI 1;
   7.249 -by(exhaust_tac "xs" 1);
   7.250 - by(ALLGOALS Asm_simp_tac);
   7.251 -br allI 1;
   7.252 -by(exhaust_tac "n" 1);
   7.253 - by(ALLGOALS Asm_simp_tac);
   7.254 +by (nat_ind_tac "m" 1);
   7.255 + by (ALLGOALS Asm_simp_tac);
   7.256 +by (rtac allI 1);
   7.257 +by (exhaust_tac "xs" 1);
   7.258 + by (ALLGOALS Asm_simp_tac);
   7.259 +by (rtac allI 1);
   7.260 +by (exhaust_tac "n" 1);
   7.261 + by (ALLGOALS Asm_simp_tac);
   7.262  qed_spec_mp "take_take";
   7.263  
   7.264  goal thy "!xs. drop n (drop m xs) = drop (n + m) xs"; 
   7.265 -by(nat_ind_tac "m" 1);
   7.266 - by(ALLGOALS Asm_simp_tac);
   7.267 -br allI 1;
   7.268 -by(exhaust_tac "xs" 1);
   7.269 - by(ALLGOALS Asm_simp_tac);
   7.270 +by (nat_ind_tac "m" 1);
   7.271 + by (ALLGOALS Asm_simp_tac);
   7.272 +by (rtac allI 1);
   7.273 +by (exhaust_tac "xs" 1);
   7.274 + by (ALLGOALS Asm_simp_tac);
   7.275  qed_spec_mp "drop_drop";
   7.276  
   7.277  goal thy "!xs n. take n (drop m xs) = drop m (take (n + m) xs)"; 
   7.278 -by(nat_ind_tac "m" 1);
   7.279 - by(ALLGOALS Asm_simp_tac);
   7.280 -br allI 1;
   7.281 -by(exhaust_tac "xs" 1);
   7.282 - by(ALLGOALS Asm_simp_tac);
   7.283 +by (nat_ind_tac "m" 1);
   7.284 + by (ALLGOALS Asm_simp_tac);
   7.285 +by (rtac allI 1);
   7.286 +by (exhaust_tac "xs" 1);
   7.287 + by (ALLGOALS Asm_simp_tac);
   7.288  qed_spec_mp "take_drop";
   7.289  
   7.290  goal thy "!xs. take n (map f xs) = map f (take n xs)"; 
   7.291 -by(nat_ind_tac "n" 1);
   7.292 -by(ALLGOALS Asm_simp_tac);
   7.293 -br allI 1;
   7.294 -by(exhaust_tac "xs" 1);
   7.295 -by(ALLGOALS Asm_simp_tac);
   7.296 +by (nat_ind_tac "n" 1);
   7.297 +by (ALLGOALS Asm_simp_tac);
   7.298 +by (rtac allI 1);
   7.299 +by (exhaust_tac "xs" 1);
   7.300 +by (ALLGOALS Asm_simp_tac);
   7.301  qed_spec_mp "take_map"; 
   7.302  
   7.303  goal thy "!xs. drop n (map f xs) = map f (drop n xs)"; 
   7.304 -by(nat_ind_tac "n" 1);
   7.305 -by(ALLGOALS Asm_simp_tac);
   7.306 -br allI 1;
   7.307 -by(exhaust_tac "xs" 1);
   7.308 -by(ALLGOALS Asm_simp_tac);
   7.309 +by (nat_ind_tac "n" 1);
   7.310 +by (ALLGOALS Asm_simp_tac);
   7.311 +by (rtac allI 1);
   7.312 +by (exhaust_tac "xs" 1);
   7.313 +by (ALLGOALS Asm_simp_tac);
   7.314  qed_spec_mp "drop_map";
   7.315  
   7.316  goal thy "!n i. i < n --> nth i (take n xs) = nth i xs";
   7.317 -by(induct_tac "xs" 1);
   7.318 - by(ALLGOALS Asm_simp_tac);
   7.319 -by(strip_tac 1);
   7.320 -by(exhaust_tac "n" 1);
   7.321 - by(Blast_tac 1);
   7.322 -by(exhaust_tac "i" 1);
   7.323 -by(ALLGOALS Asm_full_simp_tac);
   7.324 +by (induct_tac "xs" 1);
   7.325 + by (ALLGOALS Asm_simp_tac);
   7.326 +by (strip_tac 1);
   7.327 +by (exhaust_tac "n" 1);
   7.328 + by (Blast_tac 1);
   7.329 +by (exhaust_tac "i" 1);
   7.330 +by (ALLGOALS Asm_full_simp_tac);
   7.331  qed_spec_mp "nth_take";
   7.332  Addsimps [nth_take];
   7.333  
   7.334  goal thy  "!xs i. n + i < length xs --> nth i (drop n xs) = nth (n + i) xs";
   7.335 -by(nat_ind_tac "n" 1);
   7.336 - by(ALLGOALS Asm_simp_tac);
   7.337 -br allI 1;
   7.338 -by(exhaust_tac "xs" 1);
   7.339 - by(ALLGOALS Asm_simp_tac);
   7.340 +by (nat_ind_tac "n" 1);
   7.341 + by (ALLGOALS Asm_simp_tac);
   7.342 +by (rtac allI 1);
   7.343 +by (exhaust_tac "xs" 1);
   7.344 + by (ALLGOALS Asm_simp_tac);
   7.345  qed_spec_mp "nth_drop";
   7.346  Addsimps [nth_drop];
   7.347  
   7.348 @@ -484,41 +484,41 @@
   7.349  
   7.350  goal thy
   7.351    "x:set_of_list xs & ~P(x) --> takeWhile P (xs @ ys) = takeWhile P xs";
   7.352 -by(induct_tac "xs" 1);
   7.353 - by(Simp_tac 1);
   7.354 -by(asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1);
   7.355 -by(Blast_tac 1);
   7.356 +by (induct_tac "xs" 1);
   7.357 + by (Simp_tac 1);
   7.358 +by (asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1);
   7.359 +by (Blast_tac 1);
   7.360  bind_thm("takeWhile_append1", conjI RS (result() RS mp));
   7.361  Addsimps [takeWhile_append1];
   7.362  
   7.363  goal thy
   7.364    "(!x:set_of_list xs.P(x)) --> takeWhile P (xs @ ys) = xs @ takeWhile P ys";
   7.365 -by(induct_tac "xs" 1);
   7.366 - by(Simp_tac 1);
   7.367 -by(asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1);
   7.368 +by (induct_tac "xs" 1);
   7.369 + by (Simp_tac 1);
   7.370 +by (asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1);
   7.371  bind_thm("takeWhile_append2", ballI RS (result() RS mp));
   7.372  Addsimps [takeWhile_append2];
   7.373  
   7.374  goal thy
   7.375    "x:set_of_list xs & ~P(x) --> dropWhile P (xs @ ys) = (dropWhile P xs)@ys";
   7.376 -by(induct_tac "xs" 1);
   7.377 - by(Simp_tac 1);
   7.378 -by(asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1);
   7.379 -by(Blast_tac 1);
   7.380 +by (induct_tac "xs" 1);
   7.381 + by (Simp_tac 1);
   7.382 +by (asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1);
   7.383 +by (Blast_tac 1);
   7.384  bind_thm("dropWhile_append1", conjI RS (result() RS mp));
   7.385  Addsimps [dropWhile_append1];
   7.386  
   7.387  goal thy
   7.388    "(!x:set_of_list xs.P(x)) --> dropWhile P (xs @ ys) = dropWhile P ys";
   7.389 -by(induct_tac "xs" 1);
   7.390 - by(Simp_tac 1);
   7.391 -by(asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1);
   7.392 +by (induct_tac "xs" 1);
   7.393 + by (Simp_tac 1);
   7.394 +by (asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1);
   7.395  bind_thm("dropWhile_append2", ballI RS (result() RS mp));
   7.396  Addsimps [dropWhile_append2];
   7.397  
   7.398  goal thy "x:set_of_list(takeWhile P xs) --> x:set_of_list xs & P x";
   7.399 -by(induct_tac "xs" 1);
   7.400 - by(Simp_tac 1);
   7.401 -by(asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1);
   7.402 +by (induct_tac "xs" 1);
   7.403 + by (Simp_tac 1);
   7.404 +by (asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1);
   7.405  qed_spec_mp"set_of_list_take_whileD";
   7.406  
     8.1 --- a/src/HOL/Modelcheck/MCSyn.ML	Mon Jun 23 10:35:49 1997 +0200
     8.2 +++ b/src/HOL/Modelcheck/MCSyn.ML	Mon Jun 23 10:42:03 1997 +0200
     8.3 @@ -19,16 +19,16 @@
     8.4  
     8.5  
     8.6  goal Prod.thy "(? x. P x) = (? a b. P(a,b))";
     8.7 -auto();
     8.8 +by (Auto_tac());
     8.9  by (split_all_tac 1);
    8.10 -auto();
    8.11 +by (Auto_tac());
    8.12  qed "split_paired_Ex";
    8.13  
    8.14  
    8.15  goalw thy [split_def] "(f::'a*'b=>'c) = (%(x, y). f (x, y))";
    8.16 -  br ext 1;
    8.17 +  by (rtac ext 1);
    8.18    by (stac (surjective_pairing RS sym) 1);
    8.19 -  br refl 1;
    8.20 +  by (rtac refl 1);
    8.21  qed "pair_eta_expand";
    8.22  
    8.23  local
     9.1 --- a/src/HOL/NatDef.ML	Mon Jun 23 10:35:49 1997 +0200
     9.2 +++ b/src/HOL/NatDef.ML	Mon Jun 23 10:42:03 1997 +0200
     9.3 @@ -135,7 +135,7 @@
     9.4  bind_thm ("Suc_n_not_n", n_not_Suc_n RS not_sym);
     9.5  
     9.6  goal thy "!!n. n ~= 0 ==> EX m. n = Suc m";
     9.7 -br natE 1;
     9.8 +by (rtac natE 1);
     9.9  by (REPEAT (Blast_tac 1));
    9.10  qed "not0_implies_Suc";
    9.11  
    9.12 @@ -567,15 +567,15 @@
    9.13  (** LEAST -- the least number operator **)
    9.14  
    9.15  goal thy "(! m::nat. P m --> n <= m) = (! m. m < n --> ~ P m)";
    9.16 -by(blast_tac (!claset addIs [leI] addEs [leE]) 1);
    9.17 +by (blast_tac (!claset addIs [leI] addEs [leE]) 1);
    9.18  val lemma = result();
    9.19  
    9.20  (* This is an old def of Least for nat, which is derived for compatibility *)
    9.21  goalw thy [Least_def]
    9.22    "(LEAST n::nat. P n) == (@n. P(n) & (ALL m. m < n --> ~P(m)))";
    9.23 -by(simp_tac (!simpset addsimps [lemma]) 1);
    9.24 -br eq_reflection 1;
    9.25 -br refl 1;
    9.26 +by (simp_tac (!simpset addsimps [lemma]) 1);
    9.27 +by (rtac eq_reflection 1);
    9.28 +by (rtac refl 1);
    9.29  qed "Least_nat_def";
    9.30  
    9.31  val [prem1,prem2] = goalw thy [Least_nat_def]
    10.1 --- a/src/HOL/Power.ML	Mon Jun 23 10:35:49 1997 +0200
    10.2 +++ b/src/HOL/Power.ML	Mon Jun 23 10:42:03 1997 +0200
    10.3 @@ -28,15 +28,15 @@
    10.4  qed "zero_less_power";
    10.5  
    10.6  goalw thy [dvd_def] "!!m::nat. m<=n ==> i^m dvd i^n";
    10.7 -be (not_less_iff_le RS iffD2 RS add_diff_inverse RS subst) 1;
    10.8 +by (etac (not_less_iff_le RS iffD2 RS add_diff_inverse RS subst) 1);
    10.9  by (asm_simp_tac (!simpset addsimps [power_add]) 1);
   10.10  by (Blast_tac 1);
   10.11  qed "le_imp_power_dvd";
   10.12  
   10.13  goal thy "!! i r. [| 0 < i; i^m < i^n |] ==> m<n";
   10.14 -br ccontr 1;
   10.15 -bd (leI RS le_imp_power_dvd RS dvd_imp_le RS leD) 1;
   10.16 -be zero_less_power 1;
   10.17 +by (rtac ccontr 1);
   10.18 +by (dtac (leI RS le_imp_power_dvd RS dvd_imp_le RS leD) 1);
   10.19 +by (etac zero_less_power 1);
   10.20  by (contr_tac 1);
   10.21  qed "power_less_imp_less";
   10.22  
    11.1 --- a/src/HOL/Quot/HQUOT.ML	Mon Jun 23 10:35:49 1997 +0200
    11.2 +++ b/src/HOL/Quot/HQUOT.ML	Mon Jun 23 10:42:03 1997 +0200
    11.3 @@ -14,7 +14,7 @@
    11.4  
    11.5  val prems = goal thy "Rep_quot a = Rep_quot b ==> a=b";
    11.6  by (cut_facts_tac prems 1);
    11.7 -br (Rep_quot_inverse RS subst) 1;
    11.8 +by (rtac (Rep_quot_inverse RS subst) 1);
    11.9  by (res_inst_tac [("t","a")] (Rep_quot_inverse RS subst) 1);
   11.10  by (Asm_simp_tac 1);
   11.11  qed "quot_eq";
   11.12 @@ -22,8 +22,8 @@
   11.13  (* prepare induction and exhaustiveness *)
   11.14  val prems = goal thy "!s.s:quot --> P (Abs_quot s) ==> P x";
   11.15  by (cut_facts_tac prems 1);
   11.16 -br (Abs_quot_inverse RS subst) 1;
   11.17 -br Rep_quot 1;
   11.18 +by (rtac (Abs_quot_inverse RS subst) 1);
   11.19 +by (rtac Rep_quot 1);
   11.20  by (dres_inst_tac [("x","Rep_quot x")] spec 1);
   11.21  by (asm_full_simp_tac (HOL_ss addsimps [Rep_quot,Rep_quot_inverse]) 1);
   11.22  qed "all_q";
   11.23 @@ -39,90 +39,90 @@
   11.24  val prems = goalw thy [peclass_def] "x===y==><[x]>=<[y]>";
   11.25  by (cut_facts_tac prems 1);
   11.26  by (res_inst_tac [("f","Abs_quot")] arg_cong 1);
   11.27 -br Collect_cong 1;
   11.28 -br iffI 1;
   11.29 -be per_trans 1;ba 1;
   11.30 -be per_trans 1;
   11.31 -be per_sym 1;
   11.32 +by (rtac Collect_cong 1);
   11.33 +by (rtac iffI 1);
   11.34 +by (etac per_trans 1);by (assume_tac 1);
   11.35 +by (etac per_trans 1);
   11.36 +by (etac per_sym 1);
   11.37  qed "per_class_eqI";
   11.38  
   11.39  val prems = goalw thy [peclass_def] "<[(x::'a::er)]>=<[y]>==>x===y";
   11.40  by (cut_facts_tac prems 1);
   11.41  by (dres_inst_tac [("f","Rep_quot")] arg_cong 1);
   11.42  by (asm_full_simp_tac(HOL_ss addsimps [Abs_quot_inverse,per_class_rep_quot])1);
   11.43 -by (dres_inst_tac [("c","x")] equalityCE 1);ba 3;
   11.44 +by (dres_inst_tac [("c","x")] equalityCE 1);by (assume_tac 3);
   11.45  by (safe_tac set_cs);
   11.46  by (fast_tac (set_cs addIs [er_refl]) 1);
   11.47  qed "er_class_eqE";
   11.48  
   11.49  val prems = goalw thy [peclass_def] "[|x:D;<[x]>=<[y]>|]==>x===y";
   11.50  by (cut_facts_tac prems 1);
   11.51 -bd DomainD 1;
   11.52 +by (dtac DomainD 1);
   11.53  by (dres_inst_tac [("f","Rep_quot")] arg_cong 1);
   11.54  by (asm_full_simp_tac(HOL_ss addsimps [Abs_quot_inverse,per_class_rep_quot])1);
   11.55 -by (dres_inst_tac [("c","x")] equalityCE 1);ba 3;
   11.56 +by (dres_inst_tac [("c","x")] equalityCE 1);by (assume_tac 3);
   11.57  by (safe_tac set_cs);
   11.58  qed "per_class_eqE";
   11.59  
   11.60  goal thy "<[(x::'a::er)]>=<[y]>=x===y";
   11.61 -br iffI 1;
   11.62 -be er_class_eqE 1;
   11.63 -be per_class_eqI 1;
   11.64 +by (rtac iffI 1);
   11.65 +by (etac er_class_eqE 1);
   11.66 +by (etac per_class_eqI 1);
   11.67  qed "er_class_eq";
   11.68  
   11.69  val prems = goal thy "x:D==><[x]>=<[y]>=x===y";
   11.70  by (cut_facts_tac prems 1);
   11.71 -br iffI 1;
   11.72 -be per_class_eqE 1;ba 1;
   11.73 -be per_class_eqI 1;
   11.74 +by (rtac iffI 1);
   11.75 +by (etac per_class_eqE 1);by (assume_tac 1);
   11.76 +by (etac per_class_eqI 1);
   11.77  qed "per_class_eq";
   11.78  
   11.79  (* inequality *)
   11.80  val prems = goal thy "[|x:D;~x===y|]==><[x]>~=<[y]>";
   11.81  by (cut_facts_tac prems 1);
   11.82 -br notI 1;
   11.83 -bd per_class_eqE 1;
   11.84 -auto();
   11.85 +by (rtac notI 1);
   11.86 +by (dtac per_class_eqE 1);
   11.87 +by (Auto_tac());
   11.88  qed "per_class_neqI";
   11.89  
   11.90  val prems = goal thy "~(x::'a::er)===y==><[x]>~=<[y]>";
   11.91  by (cut_facts_tac prems 1);
   11.92 -br notI 1;
   11.93 -bd er_class_eqE 1;
   11.94 -auto();
   11.95 +by (rtac notI 1);
   11.96 +by (dtac er_class_eqE 1);
   11.97 +by (Auto_tac());
   11.98  qed "er_class_neqI";
   11.99  
  11.100  val prems = goal thy "<[x]>~=<[y]>==>~x===y";
  11.101  by (cut_facts_tac prems 1);
  11.102 -br notI 1;
  11.103 -be notE 1;
  11.104 -be per_class_eqI 1;
  11.105 +by (rtac notI 1);
  11.106 +by (etac notE 1);
  11.107 +by (etac per_class_eqI 1);
  11.108  qed "per_class_neqE";
  11.109  
  11.110  val prems = goal thy "x:D==><[x]>~=<[y]>=(~x===y)";
  11.111  by (cut_facts_tac prems 1);
  11.112 -br iffI 1;
  11.113 -be per_class_neqE 1;
  11.114 -be per_class_neqI 1;ba 1;
  11.115 +by (rtac iffI 1);
  11.116 +by (etac per_class_neqE 1);
  11.117 +by (etac per_class_neqI 1);by (assume_tac 1);
  11.118  qed "per_class_not";
  11.119  
  11.120  goal thy "<[(x::'a::er)]>~=<[y]>=(~x===y)";
  11.121 -br iffI 1;
  11.122 -be per_class_neqE 1;
  11.123 -be er_class_neqI 1;
  11.124 +by (rtac iffI 1);
  11.125 +by (etac per_class_neqE 1);
  11.126 +by (etac er_class_neqI 1);
  11.127  qed "er_class_not";
  11.128  
  11.129  (* exhaustiveness and induction *)
  11.130  goalw thy [peclass_def] "? s.x=<[s]>";
  11.131 -br all_q 1;
  11.132 +by (rtac all_q 1);
  11.133  by (strip_tac 1);
  11.134  by (asm_full_simp_tac (HOL_ss addsimps [mem_Collect_eq,quot_def]) 1);
  11.135 -be exE 1;
  11.136 +by (etac exE 1);
  11.137  by (res_inst_tac [("x","r")] exI 1);
  11.138 -br quot_eq 1;
  11.139 +by (rtac quot_eq 1);
  11.140  by (subgoal_tac "s:quot" 1);
  11.141  by (asm_simp_tac(HOL_ss addsimps [Abs_quot_inverse,per_class_rep_quot])1);
  11.142 -br set_ext 1;
  11.143 +by (rtac set_ext 1);
  11.144  by (fast_tac set_cs 1);
  11.145  by (asm_full_simp_tac (HOL_ss addsimps [mem_Collect_eq,quot_def]) 1);
  11.146  by (fast_tac set_cs 1);
    12.1 --- a/src/HOL/Quot/NPAIR.ML	Mon Jun 23 10:35:49 1997 +0200
    12.2 +++ b/src/HOL/Quot/NPAIR.ML	Mon Jun 23 10:42:03 1997 +0200
    12.3 @@ -7,13 +7,13 @@
    12.4  open NPAIR;
    12.5  
    12.6  goalw thy [rep_NP_def] "rep_NP(abs_NP np) = np";
    12.7 -auto();
    12.8 +by (Auto_tac());
    12.9  qed "rep_abs_NP";
   12.10  
   12.11  Addsimps [rep_abs_NP];
   12.12  
   12.13  val prems = goalw thy [per_NP_def] "eqv (x::NP) y ==> eqv y x";
   12.14  by (cut_facts_tac prems 1);
   12.15 -auto();
   12.16 +by (Auto_tac());
   12.17  qed "per_sym_NP";
   12.18  
    13.1 --- a/src/HOL/Quot/PER.ML	Mon Jun 23 10:35:49 1997 +0200
    13.2 +++ b/src/HOL/Quot/PER.ML	Mon Jun 23 10:42:03 1997 +0200
    13.3 @@ -7,13 +7,13 @@
    13.4  open PER;
    13.5  
    13.6  goalw thy [fun_per_def,per_def] "f===g=(!x y.x:D&y:D&x===y-->f x===g y)";
    13.7 -br refl 1;
    13.8 +by (rtac refl 1);
    13.9  qed "inst_fun_per";
   13.10  
   13.11  (* Witness that quot is not empty *)
   13.12  goal thy "?z:{s.? r.!y.y:s=y===r}";
   13.13  fr CollectI;
   13.14  by (res_inst_tac [("x","x")] exI 1);
   13.15 -br allI 1;
   13.16 -br mem_Collect_eq 1;
   13.17 +by (rtac allI 1);
   13.18 +by (rtac mem_Collect_eq 1);
   13.19  qed "quotNE";
    14.1 --- a/src/HOL/Quot/PER0.ML	Mon Jun 23 10:35:49 1997 +0200
    14.2 +++ b/src/HOL/Quot/PER0.ML	Mon Jun 23 10:42:03 1997 +0200
    14.3 @@ -9,37 +9,37 @@
    14.4  (* derive the characteristic axioms *)
    14.5  val prems = goalw thy [per_def] "x === y ==> y === x";
    14.6  by (cut_facts_tac prems 1);
    14.7 -be ax_per_sym 1;
    14.8 +by (etac ax_per_sym 1);
    14.9  qed "per_sym";
   14.10  
   14.11  val prems = goalw thy [per_def] "[| x === y; y === z |] ==> x === z";
   14.12  by (cut_facts_tac prems 1);
   14.13 -be ax_per_trans 1;
   14.14 -ba 1;
   14.15 +by (etac ax_per_trans 1);
   14.16 +by (assume_tac 1);
   14.17  qed "per_trans";
   14.18  
   14.19  goalw thy [per_def] "(x::'a::er) === x";
   14.20 -br ax_er_refl 1;
   14.21 +by (rtac ax_er_refl 1);
   14.22  qed "er_refl";
   14.23  
   14.24  (* now everything works without axclasses *)
   14.25  
   14.26  goal thy "x===y=y===x";
   14.27 -br iffI 1;
   14.28 -be per_sym 1;
   14.29 -be per_sym 1;
   14.30 +by (rtac iffI 1);
   14.31 +by (etac per_sym 1);
   14.32 +by (etac per_sym 1);
   14.33  qed "per_sym2";
   14.34  
   14.35  val prems = goal  thy "x===y ==> x===x";
   14.36  by (cut_facts_tac prems 1);
   14.37 -br per_trans 1;ba 1;
   14.38 -be per_sym 1;
   14.39 +by (rtac per_trans 1);by (assume_tac 1);
   14.40 +by (etac per_sym 1);
   14.41  qed "sym2refl1";
   14.42  
   14.43  val prems = goal  thy "x===y ==> y===y";
   14.44  by (cut_facts_tac prems 1);
   14.45 -br per_trans 1;ba 2;
   14.46 -be per_sym 1;
   14.47 +by (rtac per_trans 1);by (assume_tac 2);
   14.48 +by (etac per_sym 1);
   14.49  qed "sym2refl2";
   14.50  
   14.51  val prems = goalw thy [Dom] "x:D ==> x === x";
   14.52 @@ -53,44 +53,44 @@
   14.53  qed "DomainI";
   14.54  
   14.55  goal thy "x:D = x===x";
   14.56 -br iffI 1;
   14.57 -be DomainD 1;
   14.58 -be DomainI 1;
   14.59 +by (rtac iffI 1);
   14.60 +by (etac DomainD 1);
   14.61 +by (etac DomainI 1);
   14.62  qed "DomainEq";
   14.63  
   14.64  goal thy "(~ x === y) = (~ y === x)";
   14.65 -br (per_sym2 RS arg_cong) 1;
   14.66 +by (rtac (per_sym2 RS arg_cong) 1);
   14.67  qed "per_not_sym";
   14.68  
   14.69  (* show that PER work only on D *)
   14.70  val prems = goal thy "x===y ==> x:D";
   14.71  by (cut_facts_tac prems 1);
   14.72 -be (sym2refl1 RS DomainI) 1;
   14.73 +by (etac (sym2refl1 RS DomainI) 1);
   14.74  qed "DomainI_left"; 
   14.75  
   14.76  val prems = goal thy "x===y ==> y:D";
   14.77  by (cut_facts_tac prems 1);
   14.78 -be (sym2refl2 RS DomainI) 1;
   14.79 +by (etac (sym2refl2 RS DomainI) 1);
   14.80  qed "DomainI_right"; 
   14.81  
   14.82  val prems = goalw thy [Dom] "x~:D ==> ~x===y";
   14.83  by (cut_facts_tac prems 1);
   14.84 -by (res_inst_tac [("Q","x===y")] (excluded_middle RS disjE) 1);ba 1;
   14.85 -bd sym2refl1 1;
   14.86 +by (res_inst_tac [("Q","x===y")] (excluded_middle RS disjE) 1);by (assume_tac 1);
   14.87 +by (dtac sym2refl1 1);
   14.88  by (fast_tac set_cs 1);
   14.89  qed "notDomainE1"; 
   14.90  
   14.91  val prems = goalw thy [Dom] "x~:D ==> ~y===x";
   14.92  by (cut_facts_tac prems 1);
   14.93 -by (res_inst_tac [("Q","y===x")] (excluded_middle RS disjE) 1);ba 1;
   14.94 -bd sym2refl2 1;
   14.95 +by (res_inst_tac [("Q","y===x")] (excluded_middle RS disjE) 1);by (assume_tac 1);
   14.96 +by (dtac sym2refl2 1);
   14.97  by (fast_tac set_cs 1);
   14.98  qed "notDomainE2"; 
   14.99  
  14.100  (* theorems for equivalence relations *)
  14.101  goal thy "(x::'a::er) : D";
  14.102 -br DomainI 1;
  14.103 -br er_refl 1;
  14.104 +by (rtac DomainI 1);
  14.105 +by (rtac er_refl 1);
  14.106  qed "er_Domain";
  14.107  
  14.108  (* witnesses for "=>" ::(per,per)per  *)
  14.109 @@ -106,9 +106,9 @@
  14.110  by (safe_tac HOL_cs);
  14.111  by (REPEAT (dtac spec 1));
  14.112  by (res_inst_tac [("y","g y")] per_trans 1);
  14.113 -br mp 1;ba 1;
  14.114 +by (rtac mp 1);by (assume_tac 1);
  14.115  by (Asm_simp_tac 1);
  14.116 -br mp 1;ba 1;
  14.117 +by (rtac mp 1);by (assume_tac 1);
  14.118  by (asm_simp_tac (!simpset addsimps [sym2refl2]) 1);
  14.119  qed "per_trans_fun";
  14.120  
    15.1 --- a/src/HOL/Subst/Subst.ML	Mon Jun 23 10:35:49 1997 +0200
    15.2 +++ b/src/HOL/Subst/Subst.ML	Mon Jun 23 10:42:03 1997 +0200
    15.3 @@ -25,7 +25,7 @@
    15.4  
    15.5  goal Subst.thy  "~ (Var(v) <: t) --> t <| (v,t <| s) # s = t <| s";
    15.6  by (case_tac "t = Var(v)" 1);
    15.7 -be rev_mp 2;
    15.8 +by (etac rev_mp 2);
    15.9  by (res_inst_tac [("P",
   15.10      "%x.~x=Var(v) --> ~(Var(v) <: x) --> x <| (v,t<|s)#s=x<|s")]
   15.11      uterm.induct 2);
   15.12 @@ -41,7 +41,7 @@
   15.13  qed "agreement";
   15.14  
   15.15  goal Subst.thy   "~ v: vars_of(t) --> t <| (v,u)#s = t <| s";
   15.16 -by(simp_tac (!simpset addsimps [agreement]
   15.17 +by (simp_tac (!simpset addsimps [agreement]
   15.18                        setloop (split_tac [expand_if])) 1);
   15.19  qed_spec_mp"repl_invariance";
   15.20  
    16.1 --- a/src/HOL/Subst/Unifier.ML	Mon Jun 23 10:35:49 1997 +0200
    16.2 +++ b/src/HOL/Subst/Unifier.ML	Mon Jun 23 10:42:03 1997 +0200
    16.3 @@ -56,7 +56,7 @@
    16.4  by (simp_tac(!simpset addsimps [MGU_iff, Unifier_def, MoreGeneral_def]
    16.5  	              delsimps [subst_Var]) 1);
    16.6  by (Step_tac 1);
    16.7 -br exI 1;
    16.8 +by (rtac exI 1);
    16.9  by (etac subst 1 THEN rtac (Cons_trivial RS subst_sym) 1);
   16.10  by (etac ssubst_subst2 1);
   16.11  by (asm_simp_tac (!simpset addsimps [Var_not_occs]) 1);
    17.1 --- a/src/HOL/Trancl.ML	Mon Jun 23 10:35:49 1997 +0200
    17.2 +++ b/src/HOL/Trancl.ML	Mon Jun 23 10:42:03 1997 +0200
    17.3 @@ -195,16 +195,16 @@
    17.4  qed "rtranclE2";
    17.5  
    17.6  goal Trancl.thy "r O r^* = r^* O r";
    17.7 -by(Step_tac 1);
    17.8 - by(blast_tac (!claset addEs [rtranclE2] addIs [rtrancl_into_rtrancl]) 1);
    17.9 -by(blast_tac (!claset addEs [rtranclE] addIs [rtrancl_into_rtrancl2]) 1);
   17.10 +by (Step_tac 1);
   17.11 + by (blast_tac (!claset addEs [rtranclE2] addIs [rtrancl_into_rtrancl]) 1);
   17.12 +by (blast_tac (!claset addEs [rtranclE] addIs [rtrancl_into_rtrancl2]) 1);
   17.13  qed "r_comp_rtrancl_eq";
   17.14  
   17.15  
   17.16  (**** The relation trancl ****)
   17.17  
   17.18  goalw Trancl.thy [trancl_def] "!!p.[| p:r^+; r <= s |] ==> p:s^+";
   17.19 -by(blast_tac (!claset addIs [rtrancl_mono RS subsetD]) 1);
   17.20 +by (blast_tac (!claset addIs [rtrancl_mono RS subsetD]) 1);
   17.21  qed "trancl_mono";
   17.22  
   17.23  (** Conversions between trancl and rtrancl **)
   17.24 @@ -279,7 +279,7 @@
   17.25  
   17.26  goalw Trancl.thy [trancl_def]
   17.27    "!!r. [| (x,y):r^*; (y,z):r^+ |] ==> (x,z):r^+";
   17.28 -by(blast_tac (!claset addIs [rtrancl_trans,r_into_rtrancl]) 1);
   17.29 +by (blast_tac (!claset addIs [rtrancl_trans,r_into_rtrancl]) 1);
   17.30  qed "rtrancl_trancl_trancl";
   17.31  
   17.32  val prems = goal Trancl.thy
   17.33 @@ -291,22 +291,22 @@
   17.34  
   17.35  (* primitive recursion for trancl over finite relations: *)
   17.36  goal Trancl.thy "(insert (y,x) r)^+ = r^+ Un {(a,b). (a,y):r^* & (x,b):r^*}";
   17.37 -br equalityI 1;
   17.38 - br subsetI 1;
   17.39 - by(split_all_tac 1);
   17.40 - be trancl_induct 1;
   17.41 -  by(blast_tac (!claset addIs [r_into_trancl]) 1);
   17.42 - by(blast_tac (!claset addIs
   17.43 +by (rtac equalityI 1);
   17.44 + by (rtac subsetI 1);
   17.45 + by (split_all_tac 1);
   17.46 + by (etac trancl_induct 1);
   17.47 +  by (blast_tac (!claset addIs [r_into_trancl]) 1);
   17.48 + by (blast_tac (!claset addIs
   17.49       [rtrancl_into_trancl1,trancl_into_rtrancl,r_into_trancl,trancl_trans]) 1);
   17.50 -br subsetI 1;
   17.51 -by(blast_tac (!claset addIs
   17.52 +by (rtac subsetI 1);
   17.53 +by (blast_tac (!claset addIs
   17.54       [rtrancl_into_trancl2, rtrancl_trancl_trancl,
   17.55        impOfSubs rtrancl_mono, trancl_mono]) 1);
   17.56  qed "trancl_insert";
   17.57  
   17.58  goalw Trancl.thy [trancl_def] "(r^-1)^+ = (r^+)^-1";
   17.59 -by(simp_tac (!simpset addsimps [rtrancl_inverse,inverse_comp]) 1);
   17.60 -by(simp_tac (!simpset addsimps [rtrancl_inverse RS sym,r_comp_rtrancl_eq]) 1);
   17.61 +by (simp_tac (!simpset addsimps [rtrancl_inverse,inverse_comp]) 1);
   17.62 +by (simp_tac (!simpset addsimps [rtrancl_inverse RS sym,r_comp_rtrancl_eq]) 1);
   17.63  qed "trancl_inverse";
   17.64  
   17.65  
    18.1 --- a/src/HOL/WF.ML	Mon Jun 23 10:35:49 1997 +0200
    18.2 +++ b/src/HOL/WF.ML	Mon Jun 23 10:42:03 1997 +0200
    18.3 @@ -107,23 +107,23 @@
    18.4   *---------------------------------------------------------------------------*)
    18.5  
    18.6  goal WF.thy "wf(insert (y,x) r) = (wf(r) & (x,y) ~: r^*)";
    18.7 -br iffI 1;
    18.8 - by(blast_tac (!claset addEs [wf_trancl RS wf_irrefl] addIs
    18.9 +by (rtac iffI 1);
   18.10 + by (blast_tac (!claset addEs [wf_trancl RS wf_irrefl] addIs
   18.11        [rtrancl_into_trancl1,wf_subset,impOfSubs rtrancl_mono]) 1);
   18.12 -by(asm_full_simp_tac (!simpset addsimps [wf_eq_minimal]) 1);
   18.13 -by(safe_tac (!claset));
   18.14 -by(EVERY1[rtac allE, atac, etac impE, Blast_tac]);
   18.15 -be bexE 1;
   18.16 -by(rename_tac "a" 1);
   18.17 -by(case_tac "a = x" 1);
   18.18 - by(res_inst_tac [("x","a")]bexI 2);
   18.19 -  ba 3;
   18.20 - by(Blast_tac 2);
   18.21 -by(case_tac "y:Q" 1);
   18.22 - by(Blast_tac 2);
   18.23 -by(res_inst_tac [("x","{z. z:Q & (z,y) : r^*}")]allE 1);
   18.24 - ba 1;
   18.25 -by(fast_tac (!claset addIs [rtrancl_into_rtrancl2]) 1);
   18.26 +by (asm_full_simp_tac (!simpset addsimps [wf_eq_minimal]) 1);
   18.27 +by (safe_tac (!claset));
   18.28 +by (EVERY1[rtac allE, atac, etac impE, Blast_tac]);
   18.29 +by (etac bexE 1);
   18.30 +by (rename_tac "a" 1);
   18.31 +by (case_tac "a = x" 1);
   18.32 + by (res_inst_tac [("x","a")]bexI 2);
   18.33 +  by (assume_tac 3);
   18.34 + by (Blast_tac 2);
   18.35 +by (case_tac "y:Q" 1);
   18.36 + by (Blast_tac 2);
   18.37 +by (res_inst_tac [("x","{z. z:Q & (z,y) : r^*}")]allE 1);
   18.38 + by (assume_tac 1);
   18.39 +by (fast_tac (!claset addIs [rtrancl_into_rtrancl2]) 1);
   18.40  qed "wf_insert";
   18.41  AddIffs [wf_insert];
   18.42  
   18.43 @@ -131,18 +131,18 @@
   18.44  
   18.45  goalw WF.thy [acyclic_def]
   18.46   "!!r. wf r ==> acyclic r";
   18.47 -by(blast_tac (!claset addEs [wf_trancl RS wf_irrefl]) 1);
   18.48 +by (blast_tac (!claset addEs [wf_trancl RS wf_irrefl]) 1);
   18.49  qed "wf_acyclic";
   18.50  
   18.51  goalw WF.thy [acyclic_def]
   18.52    "acyclic(insert (y,x) r) = (acyclic r & (x,y) ~: r^*)";
   18.53 -by(simp_tac (!simpset addsimps [trancl_insert]) 1);
   18.54 -by(blast_tac (!claset addEs [make_elim rtrancl_trans]) 1);
   18.55 +by (simp_tac (!simpset addsimps [trancl_insert]) 1);
   18.56 +by (blast_tac (!claset addEs [make_elim rtrancl_trans]) 1);
   18.57  qed "acyclic_insert";
   18.58  AddIffs [acyclic_insert];
   18.59  
   18.60  goalw WF.thy [acyclic_def] "acyclic(r^-1) = acyclic r";
   18.61 -by(simp_tac (!simpset addsimps [trancl_inverse]) 1);
   18.62 +by (simp_tac (!simpset addsimps [trancl_inverse]) 1);
   18.63  qed "acyclic_inverse";
   18.64  
   18.65  (** cut **)
    19.1 --- a/src/HOL/WF_Rel.ML	Mon Jun 23 10:35:49 1997 +0200
    19.2 +++ b/src/HOL/WF_Rel.ML	Mon Jun 23 10:42:03 1997 +0200
    19.3 @@ -106,14 +106,14 @@
    19.4   *---------------------------------------------------------------------------*)
    19.5  
    19.6  goal thy "!!r. finite r ==> acyclic r --> wf r";
    19.7 -be finite_induct 1;
    19.8 - by(Blast_tac 1);
    19.9 -by(split_all_tac 1);
   19.10 -by(Asm_full_simp_tac 1);
   19.11 +by (etac finite_induct 1);
   19.12 + by (Blast_tac 1);
   19.13 +by (split_all_tac 1);
   19.14 +by (Asm_full_simp_tac 1);
   19.15  qed_spec_mp "finite_acyclic_wf";
   19.16  
   19.17  goal thy "!!r. finite r ==> wf r = acyclic r";
   19.18 -by(blast_tac (!claset addIs [finite_acyclic_wf,wf_acyclic]) 1);
   19.19 +by (blast_tac (!claset addIs [finite_acyclic_wf,wf_acyclic]) 1);
   19.20  qed "wf_iff_acyclic_if_finite";
   19.21  
   19.22  
   19.23 @@ -123,26 +123,26 @@
   19.24  
   19.25  goalw thy [wf_eq_minimal RS eq_reflection]
   19.26    "wf r = (~(? f. !i. (f(Suc i),f i) : r))";
   19.27 -br iffI 1;
   19.28 - br notI 1;
   19.29 - be exE 1;
   19.30 - by(eres_inst_tac [("x","{w. ? i. w=f i}")] allE 1);
   19.31 - by(Blast_tac 1);
   19.32 -be swap 1;
   19.33 +by (rtac iffI 1);
   19.34 + by (rtac notI 1);
   19.35 + by (etac exE 1);
   19.36 + by (eres_inst_tac [("x","{w. ? i. w=f i}")] allE 1);
   19.37 + by (Blast_tac 1);
   19.38 +by (etac swap 1);
   19.39  by (Asm_full_simp_tac 1);
   19.40  by (Step_tac 1);
   19.41 -by(subgoal_tac "!n. nat_rec x (%i y. @z. z:Q & (z,y):r) n : Q" 1);
   19.42 +by (subgoal_tac "!n. nat_rec x (%i y. @z. z:Q & (z,y):r) n : Q" 1);
   19.43   by (res_inst_tac[("x","nat_rec x (%i y. @z. z:Q & (z,y):r)")]exI 1);
   19.44 - br allI 1;
   19.45 - by(Simp_tac 1);
   19.46 - br selectI2EX 1;
   19.47 -  by(Blast_tac 1);
   19.48 - by(Blast_tac 1);
   19.49 -br allI 1;
   19.50 -by(induct_tac "n" 1);
   19.51 - by(Asm_simp_tac 1);
   19.52 -by(Simp_tac 1);
   19.53 -br selectI2EX 1;
   19.54 - by(Blast_tac 1);
   19.55 -by(Blast_tac 1);
   19.56 + by (rtac allI 1);
   19.57 + by (Simp_tac 1);
   19.58 + by (rtac selectI2EX 1);
   19.59 +  by (Blast_tac 1);
   19.60 + by (Blast_tac 1);
   19.61 +by (rtac allI 1);
   19.62 +by (induct_tac "n" 1);
   19.63 + by (Asm_simp_tac 1);
   19.64 +by (Simp_tac 1);
   19.65 +by (rtac selectI2EX 1);
   19.66 + by (Blast_tac 1);
   19.67 +by (Blast_tac 1);
   19.68  qed "wf_iff_no_infinite_down_chain";
    20.1 --- a/src/HOL/equalities.ML	Mon Jun 23 10:35:49 1997 +0200
    20.2 +++ b/src/HOL/equalities.ML	Mon Jun 23 10:42:03 1997 +0200
    20.3 @@ -100,7 +100,7 @@
    20.4  qed "image_id";
    20.5  
    20.6  goal Set.thy "f``(range g) = range (%x. f (g x))";
    20.7 -by(Blast_tac 1);
    20.8 +by (Blast_tac 1);
    20.9  qed "image_range";
   20.10  
   20.11  qed_goal "ball_image" Set.thy "(!y:F``S. P y) = (!x:S. P (F x))"
   20.12 @@ -379,7 +379,7 @@
   20.13  Addsimps[UN_empty];
   20.14  
   20.15  goal Set.thy "(UN x:A. {}) = {}";
   20.16 -by(Blast_tac 1);
   20.17 +by (Blast_tac 1);
   20.18  qed "UN_empty2";
   20.19  Addsimps[UN_empty2];
   20.20  
   20.21 @@ -635,7 +635,7 @@
   20.22  
   20.23  goal Set.thy "Pow (insert a A) = Pow A Un (insert a `` Pow A)";
   20.24  by (Step_tac 1);
   20.25 -be swap 1;
   20.26 +by (etac swap 1);
   20.27  by (res_inst_tac [("x", "x-{a}")] image_eqI 1);
   20.28  by (ALLGOALS Blast_tac);
   20.29  qed "Pow_insert";
    21.1 --- a/src/HOL/ex/Primes.ML	Mon Jun 23 10:35:49 1997 +0200
    21.2 +++ b/src/HOL/ex/Primes.ML	Mon Jun 23 10:42:03 1997 +0200
    21.3 @@ -89,8 +89,8 @@
    21.4  goalw thy [prime_def] "!!p. [| p: prime; p dvd (m*n) |] ==> p dvd m | p dvd n";
    21.5  by (Step_tac 1);
    21.6  by (subgoal_tac "m = gcd(m*p, m*n)" 1);
    21.7 -be ssubst 1;
    21.8 -br gcd_greatest 1;
    21.9 +by (etac ssubst 1);
   21.10 +by (rtac gcd_greatest 1);
   21.11  by (ALLGOALS (asm_simp_tac (!simpset addsimps [gcd_mult_distrib2 RS sym])));
   21.12  (*Now deduce  gcd(p,n)=1  to finish the proof*)
   21.13  by (cut_inst_tac [("m","p"),("n","n")] gcd_divides_both 1);
    22.1 --- a/src/HOL/ex/Primrec.ML	Mon Jun 23 10:35:49 1997 +0200
    22.2 +++ b/src/HOL/ex/Primrec.ML	Mon Jun 23 10:42:03 1997 +0200
    22.3 @@ -128,7 +128,7 @@
    22.4  val lemma = result();
    22.5  
    22.6  goal thy "!!i j k. i<j ==> ack(i,k) < ack(j,k)";
    22.7 -be less_natE 1;
    22.8 +by (etac less_natE 1);
    22.9  by (blast_tac (!claset addSIs [lemma]) 1);
   22.10  qed "ack_less_mono1";
   22.11  
   22.12 @@ -248,8 +248,8 @@
   22.13   "!!f g. [| ALL l. f l < ack(kf, list_add l);        \
   22.14  \           ALL l. g l < ack(kg, list_add l)         \
   22.15  \        |] ==> EX k. ALL l. PREC f g l< ack(k, list_add l)";
   22.16 -br exI 1;
   22.17 -br allI 1;
   22.18 +by (rtac exI 1);
   22.19 +by (rtac allI 1);
   22.20  by (rtac ([le_add1, PREC_case_lemma] MRS le_less_trans) 1);
   22.21  by (REPEAT (blast_tac (!claset addIs [ack_add_bound2]) 1));
   22.22  qed "PREC_case";
    23.1 --- a/src/HOLCF/IMP/Denotational.ML	Mon Jun 23 10:35:49 1997 +0200
    23.2 +++ b/src/HOLCF/IMP/Denotational.ML	Mon Jun 23 10:42:03 1997 +0200
    23.3 @@ -7,25 +7,25 @@
    23.4  *)
    23.5  
    23.6  goalw thy [dlift_def] "dlift f`(Def x) = f`(Discr x)";
    23.7 -by(Simp_tac 1);
    23.8 +by (Simp_tac 1);
    23.9  qed "dlift_Def";
   23.10  Addsimps [dlift_Def];
   23.11  
   23.12  goalw thy [dlift_def] "cont(%f. dlift f)";
   23.13 -by(Simp_tac 1);
   23.14 +by (Simp_tac 1);
   23.15  qed "cont_dlift";
   23.16  AddIffs [cont_dlift];
   23.17  
   23.18  goalw thy [dlift_def]
   23.19   "(dlift f`l = Def y) = (? x. l = Def x & f`(Discr x) = Def y)";
   23.20 -by(simp_tac (!simpset setloop (split_tac[expand_lift_case])) 1);
   23.21 +by (simp_tac (!simpset setloop (split_tac[expand_lift_case])) 1);
   23.22  qed "dlift_is_Def";
   23.23  Addsimps [dlift_is_Def];
   23.24  
   23.25  goal thy "!!c. <c,s> -c-> t ==> D c`(Discr s) = (Def t)";
   23.26 -be evalc.induct 1;
   23.27 +by (etac evalc.induct 1);
   23.28        by (ALLGOALS Asm_simp_tac);
   23.29 - by (ALLGOALS (rtac (fix_eq RS ssubst) THEN' Asm_full_simp_tac));
   23.30 + by (ALLGOALS (stac fix_eq THEN' Asm_full_simp_tac));
   23.31  qed_spec_mp "eval_implies_D";
   23.32  
   23.33  goal thy "!s t. D c`(Discr s) = (Def t) --> <c,s> -c-> t";
   23.34 @@ -36,8 +36,8 @@
   23.35   by (simp_tac (!simpset setloop (split_tac[expand_if])) 1);
   23.36   by (fast_tac ((HOL_cs addIs evalc.intrs) addss !simpset) 1);
   23.37  by (Simp_tac 1);
   23.38 -br fix_ind 1;
   23.39 -  by(fast_tac (HOL_cs addSIs (adm_lemmas@[adm_chfindom,ax_flat_lift])) 1);
   23.40 +by (rtac fix_ind 1);
   23.41 +  by (fast_tac (HOL_cs addSIs (adm_lemmas@[adm_chfindom,ax_flat_lift])) 1);
   23.42   by (Simp_tac 1);
   23.43  by (simp_tac (!simpset setloop (split_tac[expand_if])) 1);
   23.44  by (safe_tac HOL_cs);
    24.1 --- a/src/HOLCF/IOA/meta_theory/Automata.ML	Mon Jun 23 10:35:49 1997 +0200
    24.2 +++ b/src/HOLCF/IOA/meta_theory/Automata.ML	Mon Jun 23 10:42:03 1997 +0200
    24.3 @@ -32,7 +32,7 @@
    24.4  
    24.5  goal thy
    24.6  "starts_of(A || B) = {p. fst(p):starts_of(A) & snd(p):starts_of(B)}";
    24.7 -  by(simp_tac (!simpset addsimps (par_def::ioa_projections)) 1);
    24.8 +  by (simp_tac (!simpset addsimps (par_def::ioa_projections)) 1);
    24.9  qed "starts_of_par";
   24.10  
   24.11  
   24.12 @@ -43,14 +43,14 @@
   24.13  
   24.14  goal thy 
   24.15  "actions(asig_comp a b) = actions(a) Un actions(b)";
   24.16 -  by(simp_tac (!simpset addsimps
   24.17 +  by (simp_tac (!simpset addsimps
   24.18                 ([actions_def,asig_comp_def]@asig_projections)) 1);
   24.19    by (fast_tac (set_cs addSIs [equalityI]) 1);
   24.20  qed "actions_asig_comp";
   24.21  
   24.22  
   24.23  goal thy "asig_of(A || B) = asig_comp (asig_of A) (asig_of B)";
   24.24 -  by(simp_tac (!simpset addsimps (par_def::ioa_projections)) 1);
   24.25 +  by (simp_tac (!simpset addsimps (par_def::ioa_projections)) 1);
   24.26  qed "asig_of_par";
   24.27  
   24.28  
   24.29 @@ -90,7 +90,7 @@
   24.30  
   24.31  goal thy"compatible A B = compatible B A";
   24.32  by (asm_full_simp_tac (!simpset addsimps [compatible_def,Int_commute]) 1);
   24.33 -auto();
   24.34 +by (Auto_tac());
   24.35  qed"compat_commute";
   24.36  
   24.37  goalw thy [externals_def,actions_def,compatible_def]
   24.38 @@ -167,21 +167,21 @@
   24.39  
   24.40  goal thy "starts_of(restrict ioa acts) = starts_of(ioa) &     \
   24.41  \             trans_of(restrict ioa acts) = trans_of(ioa)";
   24.42 -by(simp_tac (!simpset addsimps ([restrict_def]@ioa_projections)) 1);
   24.43 +by (simp_tac (!simpset addsimps ([restrict_def]@ioa_projections)) 1);
   24.44  qed "cancel_restrict_a";
   24.45  
   24.46  goal thy "reachable (restrict ioa acts) s = reachable ioa s";
   24.47  by (rtac iffI 1);
   24.48 -be reachable.induct 1;
   24.49 -by(asm_full_simp_tac (!simpset addsimps [cancel_restrict_a,reachable_0]) 1);
   24.50 +by (etac reachable.induct 1);
   24.51 +by (asm_full_simp_tac (!simpset addsimps [cancel_restrict_a,reachable_0]) 1);
   24.52  by (etac reachable_n 1);
   24.53 -by(asm_full_simp_tac (!simpset addsimps [cancel_restrict_a]) 1);
   24.54 +by (asm_full_simp_tac (!simpset addsimps [cancel_restrict_a]) 1);
   24.55  (* <--  *)
   24.56 -be reachable.induct 1;
   24.57 +by (etac reachable.induct 1);
   24.58  by (rtac reachable_0 1);
   24.59 -by(asm_full_simp_tac (!simpset addsimps [cancel_restrict_a]) 1);
   24.60 +by (asm_full_simp_tac (!simpset addsimps [cancel_restrict_a]) 1);
   24.61  by (etac reachable_n 1);
   24.62 -by(asm_full_simp_tac (!simpset addsimps [cancel_restrict_a]) 1);
   24.63 +by (asm_full_simp_tac (!simpset addsimps [cancel_restrict_a]) 1);
   24.64  qed "cancel_restrict_b";
   24.65  
   24.66  goal thy "starts_of(restrict ioa acts) = starts_of(ioa) &     \
   24.67 @@ -202,14 +202,14 @@
   24.68  
   24.69  
   24.70  goal thy "!!s.[| reachable (rename C g) s |] ==> reachable C s";
   24.71 -be reachable.induct 1;
   24.72 -br reachable_0 1;
   24.73 -by(asm_full_simp_tac (!simpset addsimps [rename_def]@ioa_projections) 1);
   24.74 -bd trans_rename 1;
   24.75 -be exE 1;
   24.76 -be conjE 1;
   24.77 -be reachable_n 1;
   24.78 -ba 1;
   24.79 +by (etac reachable.induct 1);
   24.80 +by (rtac reachable_0 1);
   24.81 +by (asm_full_simp_tac (!simpset addsimps [rename_def]@ioa_projections) 1);
   24.82 +by (dtac trans_rename 1);
   24.83 +by (etac exE 1);
   24.84 +by (etac conjE 1);
   24.85 +by (etac reachable_n 1);
   24.86 +by (assume_tac 1);
   24.87  qed"reachable_rename";
   24.88  
   24.89  
   24.90 @@ -282,7 +282,7 @@
   24.91  \     (snd(snd(snd(s))),a,snd(snd(snd(t)))):trans_of(D)                      \
   24.92  \   else snd(snd(snd(t)))=snd(snd(snd(s)))))";
   24.93  
   24.94 -  by(simp_tac (!simpset addsimps ([par_def,actions_asig_comp,Pair_fst_snd_eq,Let_def]@
   24.95 +  by (simp_tac (!simpset addsimps ([par_def,actions_asig_comp,Pair_fst_snd_eq,Let_def]@
   24.96                              ioa_projections)
   24.97                    setloop (split_tac [expand_if])) 1);
   24.98  qed "trans_of_par4";
    25.1 --- a/src/HOLCF/IOA/meta_theory/CompoExecs.ML	Mon Jun 23 10:35:49 1997 +0200
    25.2 +++ b/src/HOLCF/IOA/meta_theory/CompoExecs.ML	Mon Jun 23 10:42:03 1997 +0200
    25.3 @@ -89,9 +89,9 @@
    25.4  \             `x) \
    25.5  \           ))";
    25.6  by (rtac trans 1);
    25.7 -br fix_eq2 1;
    25.8 -br stutter2_def 1;
    25.9 -br beta_cfun 1;
   25.10 +by (rtac fix_eq2 1);
   25.11 +by (rtac stutter2_def 1);
   25.12 +by (rtac beta_cfun 1);
   25.13  by (simp_tac (!simpset addsimps [flift1_def]) 1);
   25.14  qed"stutter2_unfold";
   25.15  
   25.16 @@ -108,7 +108,7 @@
   25.17  goal thy "(stutter2 A`(at>>xs)) s = \
   25.18  \              ((if (fst at)~:act A then Def (s=snd at) else TT) \
   25.19  \                andalso (stutter2 A`xs) (snd at))"; 
   25.20 -br trans 1;
   25.21 +by (rtac trans 1);
   25.22  by (stac stutter2_unfold 1);
   25.23  by (asm_full_simp_tac (!simpset addsimps [Cons_def,flift1_def,If_and_if]) 1);
   25.24  by (Simp_tac 1);
    26.1 --- a/src/HOLCF/IOA/meta_theory/CompoScheds.ML	Mon Jun 23 10:35:49 1997 +0200
    26.2 +++ b/src/HOLCF/IOA/meta_theory/CompoScheds.ML	Mon Jun 23 10:42:03 1997 +0200
    26.3 @@ -69,7 +69,7 @@
    26.4  goal thy "!!x.[| x:act A; x~:act B; HD`exA=Def a|] \
    26.5  \   ==> (mkex2 A B`(x>>sch)`exA`exB) s t =   \
    26.6  \       (x,snd a,t) >> (mkex2 A B`sch`(TL`exA)`exB) (snd a) t";
    26.7 -br trans 1;
    26.8 +by (rtac trans 1);
    26.9  by (stac mkex2_unfold 1);
   26.10  by (asm_full_simp_tac (!simpset addsimps [Cons_def,If_and_if]) 1);
   26.11  by (asm_full_simp_tac (!simpset addsimps [Cons_def]) 1);
   26.12 @@ -78,7 +78,7 @@
   26.13  goal thy "!!x.[| x~:act A; x:act B; HD`exB=Def b|] \
   26.14  \   ==> (mkex2 A B`(x>>sch)`exA`exB) s t = \
   26.15  \       (x,s,snd b) >> (mkex2 A B`sch`exA`(TL`exB)) s (snd b)";
   26.16 -br trans 1;
   26.17 +by (rtac trans 1);
   26.18  by (stac mkex2_unfold 1);
   26.19  by (asm_full_simp_tac (!simpset addsimps [Cons_def,If_and_if]) 1);
   26.20  by (asm_full_simp_tac (!simpset addsimps [Cons_def]) 1);
   26.21 @@ -88,7 +88,7 @@
   26.22  \   ==> (mkex2 A B`(x>>sch)`exA`exB) s t =  \
   26.23  \        (x,snd a,snd b) >> \
   26.24  \           (mkex2 A B`sch`(TL`exA)`(TL`exB)) (snd a) (snd b)";
   26.25 -br trans 1;
   26.26 +by (rtac trans 1);
   26.27  by (stac mkex2_unfold 1);
   26.28  by (asm_full_simp_tac (!simpset addsimps [Cons_def,If_and_if]) 1);
   26.29  by (asm_full_simp_tac (!simpset addsimps [Cons_def]) 1);
   26.30 @@ -115,7 +115,7 @@
   26.31  by (simp_tac (!simpset addsimps [mkex_def] 
   26.32                         setloop (split_tac [expand_if]) ) 1);
   26.33  by (cut_inst_tac [("exA","a>>exA")] mkex2_cons_1 1);
   26.34 -auto();
   26.35 +by (Auto_tac());
   26.36  qed"mkex_cons_1";
   26.37  
   26.38  goal thy "!!x.[| x~:act A; x:act B |] \
   26.39 @@ -124,7 +124,7 @@
   26.40  by (simp_tac (!simpset addsimps [mkex_def] 
   26.41                         setloop (split_tac [expand_if]) ) 1);
   26.42  by (cut_inst_tac [("exB","b>>exB")] mkex2_cons_2 1);
   26.43 -auto();
   26.44 +by (Auto_tac());
   26.45  qed"mkex_cons_2";
   26.46  
   26.47  goal thy "!!x.[| x:act A; x:act B |]  \
   26.48 @@ -133,7 +133,7 @@
   26.49  by (simp_tac (!simpset addsimps [mkex_def] 
   26.50                         setloop (split_tac [expand_if]) ) 1);
   26.51  by (cut_inst_tac [("exB","b>>exB"),("exA","a>>exA")] mkex2_cons_3 1);
   26.52 -auto();
   26.53 +by (Auto_tac());
   26.54  qed"mkex_cons_3";
   26.55  
   26.56  Delsimps [mkex2_UU,mkex2_nil,mkex2_cons_1,mkex2_cons_2,mkex2_cons_3];
   26.57 @@ -289,8 +289,8 @@
   26.58  by (cut_facts_tac [stutterA_mkex] 1);
   26.59  by (asm_full_simp_tac (!simpset addsimps [stutter_def,ProjA_def,mkex_def]) 1);
   26.60  by (REPEAT (etac allE 1));
   26.61 -bd mp 1;
   26.62 -ba 2;
   26.63 +by (dtac mp 1);
   26.64 +by (assume_tac 2);
   26.65  by (Asm_full_simp_tac 1);
   26.66  qed"stutter_mkex_on_A";
   26.67  
   26.68 @@ -320,8 +320,8 @@
   26.69  by (cut_facts_tac [stutterB_mkex] 1);
   26.70  by (asm_full_simp_tac (!simpset addsimps [stutter_def,ProjB_def,mkex_def]) 1);
   26.71  by (REPEAT (etac allE 1));
   26.72 -bd mp 1;
   26.73 -ba 2;
   26.74 +by (dtac mp 1);
   26.75 +by (assume_tac 2);
   26.76  by (Asm_full_simp_tac 1);
   26.77  qed"stutter_mkex_on_B";
   26.78  
   26.79 @@ -380,11 +380,11 @@
   26.80  by (asm_full_simp_tac (!simpset addsimps [ProjA_def,Filter_ex_def]) 1);
   26.81  by (pair_tac "exA" 1);
   26.82  by (pair_tac "exB" 1);
   26.83 -br conjI 1;
   26.84 +by (rtac conjI 1);
   26.85  by (simp_tac (!simpset addsimps [mkex_def]) 1);
   26.86  by (stac trick_against_eq_in_ass 1);
   26.87  back();
   26.88 -ba 1;
   26.89 +by (assume_tac 1);
   26.90  by (asm_full_simp_tac (!simpset addsimps [filter_mkex_is_exA_tmp]) 1);
   26.91  qed"filter_mkex_is_exA";
   26.92   
   26.93 @@ -424,11 +424,11 @@
   26.94  by (asm_full_simp_tac (!simpset addsimps [ProjB_def,Filter_ex_def]) 1);
   26.95  by (pair_tac "exA" 1);
   26.96  by (pair_tac "exB" 1);
   26.97 -br conjI 1;
   26.98 +by (rtac conjI 1);
   26.99  by (simp_tac (!simpset addsimps [mkex_def]) 1);
  26.100  by (stac trick_against_eq_in_ass 1);
  26.101  back();
  26.102 -ba 1;
  26.103 +by (assume_tac 1);
  26.104  by (asm_full_simp_tac (!simpset addsimps [filter_mkex_is_exB_tmp]) 1);
  26.105  qed"filter_mkex_is_exB";
  26.106  
  26.107 @@ -473,7 +473,7 @@
  26.108                                   lemma_2_1a,lemma_2_1b]) 1);
  26.109  by (asm_full_simp_tac (!simpset addsimps [executions_def]) 1);
  26.110  by (pair_tac "ex" 1);
  26.111 -be conjE 1;
  26.112 +by (etac conjE 1);
  26.113  by (asm_full_simp_tac (!simpset addsimps [sch_actions_in_AorB]) 1);
  26.114  
  26.115  (* <== *)
    27.1 --- a/src/HOLCF/IOA/meta_theory/CompoTraces.ML	Mon Jun 23 10:35:49 1997 +0200
    27.2 +++ b/src/HOLCF/IOA/meta_theory/CompoTraces.ML	Mon Jun 23 10:42:03 1997 +0200
    27.3 @@ -65,7 +65,7 @@
    27.4  \         (Takewhile (%a.a:int A)`schA) \
    27.5  \         @@ (x>>(mksch A B`tr`(TL`(Dropwhile (%a.a:int A)`schA)) \
    27.6  \                             `schB))";
    27.7 -br trans 1;
    27.8 +by (rtac trans 1);
    27.9  by (stac mksch_unfold 1);
   27.10  by (asm_full_simp_tac (!simpset addsimps [Cons_def,If_and_if]) 1);
   27.11  by (simp_tac (!simpset addsimps [Cons_def]) 1);
   27.12 @@ -76,7 +76,7 @@
   27.13  \        (Takewhile (%a.a:int B)`schB)  \
   27.14  \         @@ (x>>(mksch A B`tr`schA`(TL`(Dropwhile (%a.a:int B)`schB))  \
   27.15  \                            ))";
   27.16 -br trans 1;
   27.17 +by (rtac trans 1);
   27.18  by (stac mksch_unfold 1);
   27.19  by (asm_full_simp_tac (!simpset addsimps [Cons_def,If_and_if]) 1);
   27.20  by (simp_tac (!simpset addsimps [Cons_def]) 1);
   27.21 @@ -89,7 +89,7 @@
   27.22  \         @@ (x>>(mksch A B`tr`(TL`(Dropwhile (%a.a:int A)`schA)) \
   27.23  \                            `(TL`(Dropwhile (%a.a:int B)`schB))))  \
   27.24  \             )";
   27.25 -br trans 1;
   27.26 +by (rtac trans 1);
   27.27  by (stac mksch_unfold 1);
   27.28  by (asm_full_simp_tac (!simpset addsimps [Cons_def,If_and_if]) 1);
   27.29  by (simp_tac (!simpset addsimps [Cons_def]) 1);
   27.30 @@ -136,13 +136,13 @@
   27.31  (* Lemma for substitution of looping assumption in another specific assumption *) 
   27.32  val [p1,p2] = goal thy "[| f << (g x) ; x=(h x) |] ==> f << g (h x)";
   27.33  by (cut_facts_tac [p1] 1);
   27.34 -be (p2 RS subst) 1;
   27.35 +by (etac (p2 RS subst) 1);
   27.36  qed"subst_lemma1";
   27.37  
   27.38  (* Lemma for substitution of looping assumption in another specific assumption *) 
   27.39  val [p1,p2] = goal thy "[| (f x) = y >> g; x=(h x) |] ==> (f (h x)) = y >> g";
   27.40  by (cut_facts_tac [p1] 1);
   27.41 -be (p2 RS subst) 1;
   27.42 +by (etac (p2 RS subst) 1);
   27.43  qed"subst_lemma2";
   27.44  
   27.45  
   27.46 @@ -156,21 +156,21 @@
   27.47  by (case_tac "a:act B" 1);
   27.48  (* a:A, a:B *)
   27.49  by (Asm_full_simp_tac 1);
   27.50 -br (Forall_Conc_impl RS mp) 1;
   27.51 +by (rtac (Forall_Conc_impl RS mp) 1);
   27.52  by (asm_full_simp_tac (!simpset addsimps [ForallPTakewhileQ,intA_is_not_actB,int_is_act]) 1);
   27.53 -br (Forall_Conc_impl RS mp) 1;
   27.54 +by (rtac (Forall_Conc_impl RS mp) 1);
   27.55  by (asm_full_simp_tac (!simpset addsimps [ForallPTakewhileQ,intA_is_not_actB,int_is_act]) 1);
   27.56  (* a:A,a~:B *)
   27.57  by (Asm_full_simp_tac 1);
   27.58 -br (Forall_Conc_impl RS mp) 1;
   27.59 +by (rtac (Forall_Conc_impl RS mp) 1);
   27.60  by (asm_full_simp_tac (!simpset addsimps [ForallPTakewhileQ,intA_is_not_actB,int_is_act]) 1);
   27.61  by (case_tac "a:act B" 1);
   27.62  (* a~:A, a:B *)
   27.63  by (Asm_full_simp_tac 1);
   27.64 -br (Forall_Conc_impl RS mp) 1;
   27.65 +by (rtac (Forall_Conc_impl RS mp) 1);
   27.66  by (asm_full_simp_tac (!simpset addsimps [ForallPTakewhileQ,intA_is_not_actB,int_is_act]) 1);
   27.67  (* a~:A,a~:B *)
   27.68 -auto();
   27.69 +by (Auto_tac());
   27.70  qed"ForallAorB_mksch1";
   27.71  
   27.72  bind_thm ("ForallAorB_mksch",ForallAorB_mksch1 RS spec RS spec RS mp);
   27.73 @@ -181,7 +181,7 @@
   27.74  
   27.75  by (Seq_induct_tac "tr" [Forall_def,sforall_def,mksch_def] 1);
   27.76  by (safe_tac set_cs);
   27.77 -br (Forall_Conc_impl RS mp) 1;
   27.78 +by (rtac (Forall_Conc_impl RS mp) 1);
   27.79  by (asm_full_simp_tac (!simpset addsimps [ForallPTakewhileQ,
   27.80                              intA_is_not_actB,int_is_act]) 1);
   27.81  qed"ForallBnA_mksch";
   27.82 @@ -196,7 +196,7 @@
   27.83  by (Seq_induct_tac "tr" [Forall_def,sforall_def,mksch_def] 1);
   27.84  by (safe_tac set_cs);
   27.85  by (Asm_full_simp_tac 1);
   27.86 -br (Forall_Conc_impl RS mp) 1;
   27.87 +by (rtac (Forall_Conc_impl RS mp) 1);
   27.88  by (asm_full_simp_tac (!simpset addsimps [ForallPTakewhileQ,
   27.89                         intA_is_not_actB,int_is_act]) 1);
   27.90  qed"ForallAnB_mksch";
   27.91 @@ -214,7 +214,7 @@
   27.92  \          Forall (%x. x:ext (A||B)) tr \
   27.93  \          --> Finite (mksch A B`tr`x`y)";
   27.94  
   27.95 -be Seq_Finite_ind  1;
   27.96 +by (etac Seq_Finite_ind  1);
   27.97  by (Asm_full_simp_tac 1);
   27.98  (* main case *)
   27.99  by (asm_full_simp_tac (!simpset setloop split_tac [expand_if]) 1);
  27.100 @@ -231,10 +231,10 @@
  27.101  (* now for conclusion IH applicable, but assumptions have to be transformed *)
  27.102  by (dres_inst_tac [("x","x"),
  27.103                     ("g","Filter (%a. a:act A)`s")] subst_lemma2 1);
  27.104 -ba 1;
  27.105 +by (assume_tac 1);
  27.106  by (dres_inst_tac [("x","y"),
  27.107                     ("g","Filter (%a. a:act B)`s")] subst_lemma2 1);
  27.108 -ba 1;
  27.109 +by (assume_tac 1);
  27.110  (* IH *)
  27.111  by (asm_full_simp_tac (!simpset addsimps [not_ext_is_int_or_not_act,
  27.112                     FilterPTakewhileQnil,ForallTL,ForallDropwhile]) 1);
  27.113 @@ -249,7 +249,7 @@
  27.114  (* now for conclusion IH applicable, but assumptions have to be transformed *)
  27.115  by (dres_inst_tac [("x","y"),
  27.116                     ("g","Filter (%a. a:act B)`s")] subst_lemma2 1);
  27.117 -ba 1;
  27.118 +by (assume_tac 1);
  27.119  (* IH *)
  27.120  by (asm_full_simp_tac (!simpset addsimps [not_ext_is_int_or_not_act,
  27.121                     FilterPTakewhileQnil,ForallTL,ForallDropwhile]) 1);
  27.122 @@ -264,7 +264,7 @@
  27.123  (* now for conclusion IH applicable, but assumptions have to be transformed *)
  27.124  by (dres_inst_tac [("x","x"),
  27.125                     ("g","Filter (%a. a:act A)`s")] subst_lemma2 1);
  27.126 -ba 1;
  27.127 +by (assume_tac 1);
  27.128  (* IH *)
  27.129  by (asm_full_simp_tac (!simpset addsimps [not_ext_is_int_or_not_act,
  27.130                     FilterPTakewhileQnil,ForallTL,ForallDropwhile]) 1);
  27.131 @@ -290,7 +290,7 @@
  27.132  \                   Finite y1 & y = (y1 @@ y2) & \
  27.133  \                   Filter (%a. a:ext B)`y1 = bs)";
  27.134  by (forw_inst_tac [("A2","A")] (compat_commute RS iffD1) 1);
  27.135 -be Seq_Finite_ind  1;
  27.136 +by (etac Seq_Finite_ind  1);
  27.137  by (REPEAT (rtac allI 1));
  27.138  by (rtac impI 1);
  27.139  by (res_inst_tac [("x","nil")] exI 1);
  27.140 @@ -308,7 +308,7 @@
  27.141  (* transform assumption f eB y = f B (s@z) *)
  27.142  by (dres_inst_tac [("x","y"),
  27.143                     ("g","Filter (%a. a:act B)`(s@@z)")] subst_lemma2 1);
  27.144 -ba 1;
  27.145 +by (assume_tac 1);
  27.146  Addsimps [FilterConc]; 
  27.147  by (asm_full_simp_tac (!simpset addsimps [FilterPTakewhileQnil,not_ext_is_int_or_not_act]) 1);
  27.148  (* apply IH *)
  27.149 @@ -345,7 +345,7 @@
  27.150  \                   Finite x1 & x = (x1 @@ x2) & \
  27.151  \                   Filter (%a. a:ext A)`x1 = as)";
  27.152  by (forw_inst_tac [("A2","A")] (compat_commute RS iffD1) 1);
  27.153 -be Seq_Finite_ind  1;
  27.154 +by (etac Seq_Finite_ind  1);
  27.155  by (REPEAT (rtac allI 1));
  27.156  by (rtac impI 1);
  27.157  by (res_inst_tac [("x","nil")] exI 1);
  27.158 @@ -363,7 +363,7 @@
  27.159  (* transform assumption f eA x = f A (s@z) *)
  27.160  by (dres_inst_tac [("x","x"),
  27.161                     ("g","Filter (%a. a:act A)`(s@@z)")] subst_lemma2 1);
  27.162 -ba 1;
  27.163 +by (assume_tac 1);
  27.164  Addsimps [FilterConc]; 
  27.165  by (asm_full_simp_tac (!simpset addsimps [FilterPTakewhileQnil,not_ext_is_int_or_not_act]) 1);
  27.166  (* apply IH *)
  27.167 @@ -394,13 +394,13 @@
  27.168  goal thy "!! y.Finite y ==> ! z tr. Forall (%a.a:ext (A||B)) tr & \
  27.169  \                             y = z @@ mksch A B`tr`a`b\
  27.170  \                             --> Finite tr";
  27.171 -be Seq_Finite_ind  1;
  27.172 -auto();
  27.173 +by (etac Seq_Finite_ind  1);
  27.174 +by (Auto_tac());
  27.175  by (Seq_case_simp_tac "tr" 1);
  27.176  (* tr = UU *)
  27.177  by (asm_full_simp_tac (!simpset addsimps [nil_is_Conc]) 1);
  27.178  (* tr = nil *)
  27.179 -auto();
  27.180 +by (Auto_tac());
  27.181  (* tr = Conc *)
  27.182  ren "s ss" 1;
  27.183  
  27.184 @@ -419,7 +419,7 @@
  27.185  by (Seq_case_simp_tac "tr" 1);
  27.186  (* tr = UU *)
  27.187  by (asm_full_simp_tac (!simpset addsimps [Conc_Conc_eq]) 1);
  27.188 -auto();
  27.189 +by (Auto_tac());
  27.190  (* tr = nil ok *)
  27.191  (* tr = Conc *)
  27.192  by (Seq_case_simp_tac "z" 1);
  27.193 @@ -452,19 +452,19 @@
  27.194  
  27.195  goal thy "(x>>xs = y @@ z) = ((y=nil & x>>xs=z) | (? ys. y=x>>ys & xs=ys@@z))";
  27.196  by (Seq_case_simp_tac "y" 1);
  27.197 -auto();
  27.198 +by (Auto_tac());
  27.199  qed"Conc_Conc_eq";
  27.200  
  27.201  goal thy "!! (y::'a Seq).Finite y ==> ~ y= x@@UU";
  27.202 -be Seq_Finite_ind 1;
  27.203 +by (etac Seq_Finite_ind 1);
  27.204  by (Seq_case_simp_tac "x" 1);
  27.205  by (Seq_case_simp_tac "x" 1);
  27.206 -auto();
  27.207 +by (Auto_tac());
  27.208  qed"FiniteConcUU1";
  27.209  
  27.210  goal thy "~ Finite ((x::'a Seq)@@UU)";
  27.211 -br (FiniteConcUU1 COMP rev_contrapos) 1;
  27.212 -auto();
  27.213 +by (rtac (FiniteConcUU1 COMP rev_contrapos) 1);
  27.214 +by (Auto_tac());
  27.215  qed"FiniteConcUU";
  27.216  
  27.217  finiteR_mksch
  27.218 @@ -505,9 +505,9 @@
  27.219             externals_of_par, intA_is_not_extB,int_is_not_ext]) 1);
  27.220  (* conclusion of IH ok, but assumptions of IH have to be transformed *)
  27.221  by (dres_inst_tac [("x","schA")] subst_lemma1 1);
  27.222 -ba 1;
  27.223 +by (assume_tac 1);
  27.224  by (dres_inst_tac [("x","schB")] subst_lemma1 1);
  27.225 -ba 1;
  27.226 +by (assume_tac 1);
  27.227  (* IH *)
  27.228  by (asm_full_simp_tac (!simpset addsimps [not_ext_is_int_or_not_act,
  27.229                     FilterPTakewhileQnil,ForallTL,ForallDropwhile]) 1);
  27.230 @@ -521,7 +521,7 @@
  27.231             externals_of_par, intA_is_not_extB,int_is_not_ext]) 1);
  27.232  by (dres_inst_tac [("x","schB")] subst_lemma1 1);
  27.233  back();
  27.234 -ba 1;
  27.235 +by (assume_tac 1);
  27.236  by (asm_full_simp_tac (!simpset addsimps [not_ext_is_int_or_not_act,
  27.237                      FilterPTakewhileQnil,ForallTL,ForallDropwhile]) 1);
  27.238  (* Case a:A, a~:B *)
  27.239 @@ -533,7 +533,7 @@
  27.240            [FilterPTakewhileQnil,not_ext_is_int_or_not_act,
  27.241             externals_of_par, intA_is_not_extB,int_is_not_ext]) 1);
  27.242  by (dres_inst_tac [("x","schA")] subst_lemma1 1);
  27.243 -ba 1;
  27.244 +by (assume_tac 1);
  27.245  by (asm_full_simp_tac (!simpset addsimps [not_ext_is_int_or_not_act,
  27.246                      FilterPTakewhileQnil,ForallTL,ForallDropwhile]) 1);
  27.247  (* Case a~:A, a~:B *)
  27.248 @@ -614,8 +614,8 @@
  27.249  (* eliminate the B-only prefix *)
  27.250  
  27.251  by (subgoal_tac "(Filter (%a.a :act A)`y1) = nil" 1);
  27.252 -be ForallQFilterPnil 2;
  27.253 -ba 2;
  27.254 +by (etac ForallQFilterPnil 2);
  27.255 +by (assume_tac 2);
  27.256  by (Fast_tac 2);
  27.257  
  27.258  (* Now real recursive step follows (in y) *)
  27.259 @@ -630,8 +630,8 @@
  27.260  by (rotate_tac ~1 1);
  27.261  by (Asm_full_simp_tac  1);
  27.262  (* eliminate introduced subgoal 2 *)
  27.263 -be ForallQFilterPnil 2;
  27.264 -ba 2;
  27.265 +by (etac ForallQFilterPnil 2);
  27.266 +by (assume_tac 2);
  27.267  by (Fast_tac 2);
  27.268   
  27.269  (* bring in divide Seq for s *)
  27.270 @@ -643,15 +643,15 @@
  27.271  back();
  27.272  back();
  27.273  back();
  27.274 -ba 1;
  27.275 +by (assume_tac 1);
  27.276  
  27.277  (* reduce trace_takes from n to strictly smaller k *)
  27.278 -br take_reduction 1;
  27.279 +by (rtac take_reduction 1);
  27.280  
  27.281  (* f A (tw iA) = tw ~eA *)
  27.282  by (asm_full_simp_tac (!simpset addsimps [FilterPTakewhileQid,int_is_act,
  27.283                                not_ext_is_int_or_not_act]) 1);
  27.284 -br refl 1;
  27.285 +by (rtac refl 1);
  27.286  
  27.287  (* now conclusion fulfills induction hypothesis, but assumptions are not ready *)
  27.288  (*
  27.289 @@ -665,12 +665,12 @@
  27.290  (* assumption schA *)
  27.291  by (dres_inst_tac [("x","schA"),
  27.292                     ("g","Filter (%a. a:act A)`s2")] subst_lemma2 1);
  27.293 -ba 1;
  27.294 +by (assume_tac 1);
  27.295  by (asm_full_simp_tac (!simpset addsimps [FilterPTakewhileQnil]) 1);
  27.296  (* assumptions concerning LastActExtsch, cannot be rewritten, as LastActExtsmalli are looping  *)
  27.297  by (dres_inst_tac [("sch","schA"),("P","%a. a:int A")] LastActExtsmall1 1);
  27.298  by (dres_inst_tac [("sch1.0","y1")]  LastActExtsmall2 1);
  27.299 -ba 1;
  27.300 +by (assume_tac 1);
  27.301  
  27.302  FIX: problem: schA and schB are not quantified in the new take lemma version !!!
  27.303  
  27.304 @@ -699,15 +699,15 @@
  27.305  \ --> Filter (%a.a:act A)`(mksch A B`tr`schA`schB) = schA";
  27.306  
  27.307  by (strip_tac 1);
  27.308 -br seq.take_lemma 1;
  27.309 -br mp 1;
  27.310 -ba 2;
  27.311 +by (rtac seq.take_lemma 1);
  27.312 +by (rtac mp 1);
  27.313 +by (assume_tac 2);
  27.314  back();back();back();back();
  27.315  by (res_inst_tac [("x","schA")] spec 1);
  27.316  by (res_inst_tac [("x","schB")] spec 1);
  27.317  by (res_inst_tac [("x","tr")] spec 1);
  27.318  by (thin_tac' 5 1);
  27.319 -br less_induct 1;
  27.320 +by (rtac less_induct 1);
  27.321  by (REPEAT (rtac allI 1));
  27.322  ren "tr schB schA" 1;
  27.323  by (strip_tac 1);
  27.324 @@ -715,7 +715,7 @@
  27.325  
  27.326  by (case_tac "Forall (%x. x:act B & x~:act A) tr" 1);
  27.327  
  27.328 -br (seq_take_lemma RS iffD2 RS spec) 1;
  27.329 +by (rtac (seq_take_lemma RS iffD2 RS spec) 1);
  27.330  by (thin_tac' 5 1);
  27.331  
  27.332  
  27.333 @@ -731,7 +731,7 @@
  27.334  by (eres_inst_tac [("A","A")] LastActExtimplnil 1);
  27.335  by (Asm_simp_tac 1);
  27.336  by (eres_inst_tac [("Q","%x.x:act B & x~:act A")] ForallQFilterPnil 1);
  27.337 -ba 1;
  27.338 +by (assume_tac 1);
  27.339  by (Fast_tac 1);
  27.340  
  27.341  (* case ~ Finite s *)
  27.342 @@ -748,12 +748,12 @@
  27.343  by (eres_inst_tac [("A","A")] LastActExtimplUU 1);
  27.344  by (Asm_simp_tac 1);
  27.345  by (eres_inst_tac [("Q","%x.x:act B & x~:act A")] ForallQFilterPUU 1);
  27.346 -ba 1;
  27.347 +by (assume_tac 1);
  27.348  by (Fast_tac 1);
  27.349  
  27.350  (* case" ~ Forall (%x.x:act B & x~:act A) s" *)
  27.351  
  27.352 -bd divide_Seq3 1;
  27.353 +by (dtac divide_Seq3 1);
  27.354  
  27.355  by (REPEAT (etac exE 1));
  27.356  by (REPEAT (etac conjE 1));
  27.357 @@ -772,8 +772,8 @@
  27.358  (* eliminate the B-only prefix *)
  27.359  
  27.360  by (subgoal_tac "(Filter (%a.a :act A)`y1) = nil" 1);
  27.361 -be ForallQFilterPnil 2;
  27.362 -ba 2;
  27.363 +by (etac ForallQFilterPnil 2);
  27.364 +by (assume_tac 2);
  27.365  by (Fast_tac 2);
  27.366  
  27.367  (* Now real recursive step follows (in y) *)
  27.368 @@ -788,8 +788,8 @@
  27.369  by (rotate_tac ~1 1);
  27.370  by (Asm_full_simp_tac  1);
  27.371  (* eliminate introduced subgoal 2 *)
  27.372 -be ForallQFilterPnil 2;
  27.373 -ba 2;
  27.374 +by (etac ForallQFilterPnil 2);
  27.375 +by (assume_tac 2);
  27.376  by (Fast_tac 2);
  27.377   
  27.378  (* bring in divide Seq for s *)
  27.379 @@ -801,15 +801,15 @@
  27.380  back();
  27.381  back();
  27.382  back();
  27.383 -ba 1;
  27.384 +by (assume_tac 1);
  27.385  
  27.386  (* reduce trace_takes from n to strictly smaller k *)
  27.387 -br take_reduction 1;
  27.388 +by (rtac take_reduction 1);
  27.389  
  27.390  (* f A (tw iA) = tw ~eA *)
  27.391  by (asm_full_simp_tac (!simpset addsimps [FilterPTakewhileQid,int_is_act,
  27.392                                not_ext_is_int_or_not_act]) 1);
  27.393 -br refl 1;
  27.394 +by (rtac refl 1);
  27.395  by (asm_full_simp_tac (!simpset addsimps [int_is_act,
  27.396                                not_ext_is_int_or_not_act]) 1);
  27.397  by (rotate_tac ~11 1);
  27.398 @@ -824,17 +824,17 @@
  27.399  (* assumption schA *)
  27.400  by (dres_inst_tac [("x","schA"),
  27.401                     ("g","Filter (%a. a:act A)`rs")] subst_lemma2 1);
  27.402 -ba 1;
  27.403 +by (assume_tac 1);
  27.404  by (asm_full_simp_tac (!simpset addsimps [FilterPTakewhileQnil,int_is_not_ext]) 1);
  27.405  (* assumptions concerning LastActExtsch, cannot be rewritten, as LastActExtsmalli are looping  *)
  27.406  by (dres_inst_tac [("sch","schA"),("P","%a. a:int A")] LastActExtsmall1 1);
  27.407  by (forw_inst_tac [("sch1.0","y1")]  LastActExtsmall2 1);
  27.408 -ba 1;
  27.409 +by (assume_tac 1);
  27.410  
  27.411  (* assumption Forall schA *)
  27.412  by (dres_inst_tac [("s","schA"),
  27.413                     ("P","Forall (%x.x:act A)")] subst 1);
  27.414 -ba 1;
  27.415 +by (assume_tac 1);
  27.416  by (asm_full_simp_tac (!simpset addsimps [ForallPTakewhileQ, int_is_act]) 1);
  27.417  
  27.418  (* case x:actions(asig_of A) & x: actions(asig_of B) *)
  27.419 @@ -847,8 +847,8 @@
  27.420  by (rotate_tac ~1 1);
  27.421  by (Asm_full_simp_tac  1);
  27.422  (* eliminate introduced subgoal 2 *)
  27.423 -be ForallQFilterPnil 2;
  27.424 -ba 2;
  27.425 +by (etac ForallQFilterPnil 2);
  27.426 +by (assume_tac 2);
  27.427  by (Fast_tac 2);
  27.428   
  27.429  (* bring in divide Seq for s *)
  27.430 @@ -860,7 +860,7 @@
  27.431  back();
  27.432  back();
  27.433  back();
  27.434 -ba 1;
  27.435 +by (assume_tac 1);
  27.436  
  27.437  (* f A (tw iA) = tw ~eA *)
  27.438  by (asm_full_simp_tac (!simpset addsimps [FilterPTakewhileQid,int_is_act,
  27.439 @@ -876,7 +876,7 @@
  27.440  (* assumption schA *)
  27.441  by (dres_inst_tac [("x","schA"),
  27.442                     ("g","Filter (%a. a:act A)`rs")] subst_lemma2 1);
  27.443 -ba 1;
  27.444 +by (assume_tac 1);
  27.445  by (asm_full_simp_tac (!simpset addsimps [FilterPTakewhileQnil,int_is_not_ext]) 1);
  27.446  
  27.447  (* f A (tw iB schB2) = nil *) 
  27.448 @@ -885,22 +885,22 @@
  27.449  
  27.450  
  27.451  (* reduce trace_takes from n to strictly smaller k *)
  27.452 -br take_reduction 1;
  27.453 -br refl 1;
  27.454 -br refl 1;
  27.455 +by (rtac take_reduction 1);
  27.456 +by (rtac refl 1);
  27.457 +by (rtac refl 1);
  27.458  
  27.459  (* now conclusion fulfills induction hypothesis, but assumptions are not all ready *)
  27.460  
  27.461  (* assumption schB *)
  27.462  by (dres_inst_tac [("x","y2"),
  27.463                     ("g","Filter (%a. a:act B)`rs")] subst_lemma2 1);
  27.464 -ba 1;
  27.465 +by (assume_tac 1);
  27.466  by (asm_full_simp_tac (!simpset addsimps [FilterPTakewhileQnil,intA_is_not_actB,int_is_not_ext]) 1);
  27.467  
  27.468  (* conclusions concerning LastActExtsch, cannot be rewritten, as LastActExtsmalli are looping  *)
  27.469  by (dres_inst_tac [("sch","schA"),("P","%a. a:int A")] LastActExtsmall1 1);
  27.470  by (forw_inst_tac [("sch1.0","y1")]  LastActExtsmall2 1);
  27.471 -ba 1;
  27.472 +by (assume_tac 1);
  27.473  by (dres_inst_tac [("sch","y2"),("P","%a. a:int B")] LastActExtsmall1 1);
  27.474  
  27.475  (* assumption Forall schA, and Forall schA are performed by ForallTL,ForallDropwhile *)
  27.476 @@ -941,15 +941,15 @@
  27.477  \ --> Filter (%a.a:act B)`(mksch A B`tr`schA`schB) = schB";
  27.478  
  27.479  by (strip_tac 1);
  27.480 -br seq.take_lemma 1;
  27.481 -br mp 1;
  27.482 -ba 2;
  27.483 +by (rtac seq.take_lemma 1);
  27.484 +by (rtac mp 1);
  27.485 +by (assume_tac 2);
  27.486  back();back();back();back();
  27.487  by (res_inst_tac [("x","schA")] spec 1);
  27.488  by (res_inst_tac [("x","schB")] spec 1);
  27.489  by (res_inst_tac [("x","tr")] spec 1);
  27.490  by (thin_tac' 5 1);
  27.491 -br less_induct 1;
  27.492 +by (rtac less_induct 1);
  27.493  by (REPEAT (rtac allI 1));
  27.494  ren "tr schB schA" 1;
  27.495  by (strip_tac 1);
  27.496 @@ -957,7 +957,7 @@
  27.497  
  27.498  by (case_tac "Forall (%x. x:act A & x~:act B) tr" 1);
  27.499  
  27.500 -br (seq_take_lemma RS iffD2 RS spec) 1;
  27.501 +by (rtac (seq_take_lemma RS iffD2 RS spec) 1);
  27.502  by (thin_tac' 5 1);
  27.503  
  27.504  
  27.505 @@ -973,7 +973,7 @@
  27.506  by (eres_inst_tac [("A","B")] LastActExtimplnil 1);
  27.507  by (Asm_simp_tac 1);
  27.508  by (eres_inst_tac [("Q","%x.x:act A & x~:act B")] ForallQFilterPnil 1);
  27.509 -ba 1;
  27.510 +by (assume_tac 1);
  27.511  by (Fast_tac 1);
  27.512  
  27.513  (* case ~ Finite tr *)
  27.514 @@ -990,12 +990,12 @@
  27.515  by (eres_inst_tac [("A","B")] LastActExtimplUU 1);
  27.516  by (Asm_simp_tac 1);
  27.517  by (eres_inst_tac [("Q","%x.x:act A & x~:act B")] ForallQFilterPUU 1);
  27.518 -ba 1;
  27.519 +by (assume_tac 1);
  27.520  by (Fast_tac 1);
  27.521  
  27.522  (* case" ~ Forall (%x.x:act B & x~:act A) s" *)
  27.523  
  27.524 -bd divide_Seq3 1;
  27.525 +by (dtac divide_Seq3 1);
  27.526  
  27.527  by (REPEAT (etac exE 1));
  27.528  by (REPEAT (etac conjE 1));
  27.529 @@ -1014,8 +1014,8 @@
  27.530  (* eliminate the A-only prefix *)
  27.531  
  27.532  by (subgoal_tac "(Filter (%a.a :act B)`x1) = nil" 1);
  27.533 -be ForallQFilterPnil 2;
  27.534 -ba 2;
  27.535 +by (etac ForallQFilterPnil 2);
  27.536 +by (assume_tac 2);
  27.537  by (Fast_tac 2);
  27.538  
  27.539  (* Now real recursive step follows (in x) *)
  27.540 @@ -1030,8 +1030,8 @@
  27.541  by (rotate_tac ~1 1);
  27.542  by (Asm_full_simp_tac  1);
  27.543  (* eliminate introduced subgoal 2 *)
  27.544 -be ForallQFilterPnil 2;
  27.545 -ba 2;
  27.546 +by (etac ForallQFilterPnil 2);
  27.547 +by (assume_tac 2);
  27.548  by (Fast_tac 2);
  27.549   
  27.550  (* bring in divide Seq for s *)
  27.551 @@ -1043,15 +1043,15 @@
  27.552  back();
  27.553  back();
  27.554  back();
  27.555 -ba 1;
  27.556 +by (assume_tac 1);
  27.557  
  27.558  (* reduce trace_takes from n to strictly smaller k *)
  27.559 -br take_reduction 1;
  27.560 +by (rtac take_reduction 1);
  27.561  
  27.562  (* f B (tw iB) = tw ~eB *)
  27.563  by (asm_full_simp_tac (!simpset addsimps [FilterPTakewhileQid,int_is_act,
  27.564                                not_ext_is_int_or_not_act]) 1);
  27.565 -br refl 1;
  27.566 +by (rtac refl 1);
  27.567  by (asm_full_simp_tac (!simpset addsimps [int_is_act,
  27.568                                not_ext_is_int_or_not_act]) 1);
  27.569  by (rotate_tac ~11 1);
  27.570 @@ -1066,17 +1066,17 @@
  27.571  (* assumption schB *)
  27.572  by (dres_inst_tac [("x","schB"),
  27.573                     ("g","Filter (%a. a:act B)`rs")] subst_lemma2 1);
  27.574 -ba 1;
  27.575 +by (assume_tac 1);
  27.576  by (asm_full_simp_tac (!simpset addsimps [FilterPTakewhileQnil,int_is_not_ext]) 1);
  27.577  (* assumptions concerning LastActExtsch, cannot be rewritten, as LastActExtsmalli are looping  *)
  27.578  by (dres_inst_tac [("sch","schB"),("P","%a. a:int B")] LastActExtsmall1 1);
  27.579  by (forw_inst_tac [("sch1.0","x1")]  LastActExtsmall2 1);
  27.580 -ba 1;
  27.581 +by (assume_tac 1);
  27.582  
  27.583  (* assumption Forall schB *)
  27.584  by (dres_inst_tac [("s","schB"),
  27.585                     ("P","Forall (%x.x:act B)")] subst 1);
  27.586 -ba 1;
  27.587 +by (assume_tac 1);
  27.588  by (asm_full_simp_tac (!simpset addsimps [ForallPTakewhileQ, int_is_act]) 1);
  27.589  
  27.590  (* case x:actions(asig_of A) & x: actions(asig_of B) *)
  27.591 @@ -1089,8 +1089,8 @@
  27.592  by (rotate_tac ~1 1);
  27.593  by (Asm_full_simp_tac  1);
  27.594  (* eliminate introduced subgoal 2 *)
  27.595 -be ForallQFilterPnil 2;
  27.596 -ba 2;
  27.597 +by (etac ForallQFilterPnil 2);
  27.598 +by (assume_tac 2);
  27.599  by (Fast_tac 2);
  27.600   
  27.601  (* bring in divide Seq for s *)
  27.602 @@ -1102,7 +1102,7 @@
  27.603  back();
  27.604  back();
  27.605  back();
  27.606 -ba 1;
  27.607 +by (assume_tac 1);
  27.608  
  27.609  (* f B (tw iB) = tw ~eB *)
  27.610  by (asm_full_simp_tac (!simpset addsimps [FilterPTakewhileQid,int_is_act,
  27.611 @@ -1118,7 +1118,7 @@
  27.612  (* assumption schA *)
  27.613  by (dres_inst_tac [("x","schB"),
  27.614                     ("g","Filter (%a. a:act B)`rs")] subst_lemma2 1);
  27.615 -ba 1;
  27.616 +by (assume_tac 1);
  27.617  by (asm_full_simp_tac (!simpset addsimps [FilterPTakewhileQnil,int_is_not_ext]) 1);
  27.618  
  27.619  (* f B (tw iA schA2) = nil *) 
  27.620 @@ -1127,22 +1127,22 @@
  27.621  
  27.622  
  27.623  (* reduce trace_takes from n to strictly smaller k *)
  27.624 -br take_reduction 1;
  27.625 -br refl 1;
  27.626 -br refl 1;
  27.627 +by (rtac take_reduction 1);
  27.628 +by (rtac refl 1);
  27.629 +by (rtac refl 1);
  27.630  
  27.631  (* now conclusion fulfills induction hypothesis, but assumptions are not all ready *)
  27.632  
  27.633  (* assumption schA *)
  27.634  by (dres_inst_tac [("x","x2"),
  27.635                     ("g","Filter (%a. a:act A)`rs")] subst_lemma2 1);
  27.636 -ba 1;
  27.637 +by (assume_tac 1);
  27.638  by (asm_full_simp_tac (!simpset addsimps [FilterPTakewhileQnil,intA_is_not_actB,int_is_not_ext]) 1);
  27.639  
  27.640  (* conclusions concerning LastActExtsch, cannot be rewritten, as LastActExtsmalli are looping  *)
  27.641  by (dres_inst_tac [("sch","schB"),("P","%a. a:int B")] LastActExtsmall1 1);
  27.642  by (forw_inst_tac [("sch1.0","x1")]  LastActExtsmall2 1);
  27.643 -ba 1;
  27.644 +by (assume_tac 1);
  27.645  by (dres_inst_tac [("sch","x2"),("P","%a. a:int A")] LastActExtsmall1 1);
  27.646  
  27.647  (* assumption Forall schA, and Forall schA are performed by ForallTL,ForallDropwhile *)
  27.648 @@ -1192,22 +1192,22 @@
  27.649  by (asm_full_simp_tac (!simpset addsimps [compatibility_consequence2,
  27.650                    externals_of_par,ext1_ext2_is_not_act2]) 1);
  27.651  (* Traces of A||B have only external actions from A or B *)  
  27.652 -br ForallPFilterP 1;
  27.653 +by (rtac ForallPFilterP 1);
  27.654  
  27.655  (* <== *)
  27.656  
  27.657  (* replace schA and schB by Cut(schA) and Cut(schB) *)
  27.658  by (dtac exists_LastActExtsch 1);
  27.659 -ba 1;
  27.660 +by (assume_tac 1);
  27.661  by (dtac exists_LastActExtsch 1);
  27.662 -ba 1;
  27.663 +by (assume_tac 1);
  27.664  by (REPEAT (etac exE 1));
  27.665  by (REPEAT (etac conjE 1));
  27.666  (* Schedules of A(B) have only actions of A(B) *)
  27.667 -bd scheds_in_sig 1;
  27.668 -ba 1;
  27.669 -bd scheds_in_sig 1;
  27.670 -ba 1;
  27.671 +by (dtac scheds_in_sig 1);
  27.672 +by (assume_tac 1);
  27.673 +by (dtac scheds_in_sig 1);
  27.674 +by (assume_tac 1);
  27.675  
  27.676  ren "h1 h2 schA schB" 1;
  27.677  (* mksch is exactly the construction of trA||B out of schA, schB, and the oracle tr,
  27.678 @@ -1220,9 +1220,9 @@
  27.679  (* mksch is a schedule -- use compositionality on sch-level *)
  27.680  by (asm_full_simp_tac (!simpset addsimps [compositionality_sch]) 1);
  27.681  by (asm_full_simp_tac (!simpset addsimps [FilterAmksch_is_schA,FilterBmksch_is_schB]) 1);
  27.682 -be ForallAorB_mksch 1;
  27.683 -be ForallPForallQ 1;
  27.684 -be ext_is_act 1;
  27.685 +by (etac ForallAorB_mksch 1);
  27.686 +by (etac ForallPForallQ 1);
  27.687 +by (etac ext_is_act 1);
  27.688  qed"compositionality_tr";
  27.689  
  27.690  
    28.1 --- a/src/HOLCF/IOA/meta_theory/Compositionality.ML	Mon Jun 23 10:35:49 1997 +0200
    28.2 +++ b/src/HOLCF/IOA/meta_theory/Compositionality.ML	Mon Jun 23 10:42:03 1997 +0200
    28.3 @@ -9,16 +9,16 @@
    28.4  
    28.5  
    28.6  goal thy "!! A. [|eA --> A ; eB & ~eA --> ~A|] ==> (eA | eB) --> A=eA";
    28.7 -auto();
    28.8 +by (Auto_tac());
    28.9  qed"compatibility_consequence3";
   28.10  
   28.11  
   28.12  goal thy 
   28.13  "!! A B. [| compatible A B; Forall (%a. a: ext A | a: ext B) tr |] ==> \
   28.14  \           Filter (%a. a: act A)`tr= Filter (%a. a: ext A)`tr";
   28.15 -br ForallPFilterQR 1;
   28.16 -ba 2;
   28.17 -br compatibility_consequence3 1;
   28.18 +by (rtac ForallPFilterQR 1);
   28.19 +by (assume_tac 2);
   28.20 +by (rtac compatibility_consequence3 1);
   28.21  by (REPEAT (asm_full_simp_tac (!simpset 
   28.22                    addsimps [ext_is_act,ext1_ext2_is_not_act1]) 1));
   28.23  qed"Filter_actAisFilter_extA";
   28.24 @@ -28,15 +28,15 @@
   28.25      or even better A||B= B||A, FIX *)
   28.26  
   28.27  goal thy "!! A. [|eA --> A ; eB & ~eA --> ~A|] ==> (eB | eA) --> A=eA";
   28.28 -auto();
   28.29 +by (Auto_tac());
   28.30  qed"compatibility_consequence4";
   28.31  
   28.32  goal thy 
   28.33  "!! A B. [| compatible A B; Forall (%a. a: ext B | a: ext A) tr |] ==> \
   28.34  \           Filter (%a. a: act A)`tr= Filter (%a. a: ext A)`tr";
   28.35 -br ForallPFilterQR 1;
   28.36 -ba 2;
   28.37 -br compatibility_consequence4 1;
   28.38 +by (rtac ForallPFilterQR 1);
   28.39 +by (assume_tac 2);
   28.40 +by (rtac compatibility_consequence4 1);
   28.41  by (REPEAT (asm_full_simp_tac (!simpset 
   28.42                    addsimps [ext_is_act,ext1_ext2_is_not_act1]) 1));
   28.43  qed"Filter_actAisFilter_extA2";
   28.44 @@ -73,11 +73,11 @@
   28.45  (* 2 goals, the 3rd has been solved automatically *)
   28.46  (* 1: Filter A2 x : traces A2 *)
   28.47  by (dres_inst_tac [("A","traces A1")] subsetD 1);
   28.48 -ba 1;
   28.49 +by (assume_tac 1);
   28.50  by (asm_full_simp_tac (!simpset addsimps [Filter_actAisFilter_extA]) 1);
   28.51  (* 2: Filter B2 x : traces B2 *)
   28.52  by (dres_inst_tac [("A","traces B1")] subsetD 1);
   28.53 -ba 1;
   28.54 +by (assume_tac 1);
   28.55  by (asm_full_simp_tac (!simpset addsimps [Filter_actAisFilter_extA2]) 1);
   28.56  qed"compositionality";
   28.57  
    29.1 --- a/src/HOLCF/IOA/meta_theory/Deadlock.ML	Mon Jun 23 10:35:49 1997 +0200
    29.2 +++ b/src/HOLCF/IOA/meta_theory/Deadlock.ML	Mon Jun 23 10:42:03 1997 +0200
    29.3 @@ -20,28 +20,28 @@
    29.4  ren "sch s ex" 1;
    29.5  by (subgoal_tac "Finite ex" 1);
    29.6  by (asm_full_simp_tac (!simpset addsimps [filter_act_def]) 2);
    29.7 -br (Map2Finite RS iffD1) 2;
    29.8 +by (rtac (Map2Finite RS iffD1) 2);
    29.9  by (res_inst_tac [("t","Map fst`ex")] subst 2);
   29.10 -ba 2;
   29.11 -be FiniteFilter 2;
   29.12 +by (assume_tac 2);
   29.13 +by (etac FiniteFilter 2);
   29.14  (* subgoal 1 *)
   29.15  by (forward_tac [exists_laststate] 1);
   29.16 -be allE 1;
   29.17 -be exE 1;
   29.18 +by (etac allE 1);
   29.19 +by (etac exE 1);
   29.20  (* using input-enabledness *)
   29.21  by (asm_full_simp_tac (!simpset addsimps [ioa_def,input_enabled_def]) 1);
   29.22  by (REPEAT (etac conjE 1));
   29.23  by (eres_inst_tac [("x","a")] allE 1);
   29.24  by (Asm_full_simp_tac 1);
   29.25  by (eres_inst_tac [("x","u")] allE 1);
   29.26 -be exE 1;
   29.27 +by (etac exE 1);
   29.28  (* instantiate execution *)
   29.29  by (res_inst_tac [("x","(s,ex @@ (a,s2)>>nil)")] exI 1);
   29.30  by (asm_full_simp_tac (!simpset addsimps [filter_act_def,MapConc]) 1);
   29.31  by (eres_inst_tac [("t","u")] lemma_2_1 1);
   29.32  by (Asm_full_simp_tac 1);
   29.33 -br sym 1;
   29.34 -ba 1;
   29.35 +by (rtac sym 1);
   29.36 +by (assume_tac 1);
   29.37  qed"scheds_input_enabled";
   29.38  
   29.39  (********************************************************************************
   29.40 @@ -56,18 +56,18 @@
   29.41  \          ==> (sch @@ a>>nil) : schedules (A||B)";
   29.42  
   29.43  by (asm_full_simp_tac (!simpset addsimps [compositionality_sch,locals_def]) 1);
   29.44 -br conjI 1;
   29.45 +by (rtac conjI 1);
   29.46  (* a : act (A||B) *)
   29.47  by (asm_full_simp_tac (!simpset addsimps [actions_of_par]) 2);
   29.48 -br disjI1 2;
   29.49 -be disjE 2;
   29.50 -be int_is_act 2;
   29.51 -be out_is_act 2;
   29.52 +by (rtac disjI1 2);
   29.53 +by (etac disjE 2);
   29.54 +by (etac int_is_act 2);
   29.55 +by (etac out_is_act 2);
   29.56  (* Filter B (sch@@[a]) : schedules B *)
   29.57  
   29.58  by (case_tac "a:int A" 1);
   29.59 -bd intA_is_not_actB 1;
   29.60 -ba 1;  (* --> a~:act B *)
   29.61 +by (dtac intA_is_not_actB 1);
   29.62 +by (assume_tac 1);  (* --> a~:act B *)
   29.63  by (Asm_full_simp_tac 1);
   29.64  
   29.65  (* case a~:int A , i.e. a:out A *)
   29.66 @@ -77,10 +77,10 @@
   29.67  by (Asm_full_simp_tac 1);
   29.68  by (subgoal_tac "a:out A" 1);
   29.69  by (Fast_tac 2);
   29.70 -bd  outAactB_is_inpB 1;
   29.71 -ba 1;
   29.72 -ba 1;
   29.73 -br scheds_input_enabled 1;
   29.74 +by (dtac outAactB_is_inpB 1);
   29.75 +by (assume_tac 1);
   29.76 +by (assume_tac 1);
   29.77 +by (rtac scheds_input_enabled 1);
   29.78  by (Asm_full_simp_tac 1);
   29.79  by (REPEAT (atac 1));
   29.80  qed"IOA_deadlock_free";
    30.1 --- a/src/HOLCF/IOA/meta_theory/RefCorrectness.ML	Mon Jun 23 10:35:49 1997 +0200
    30.2 +++ b/src/HOLCF/IOA/meta_theory/RefCorrectness.ML	Mon Jun 23 10:42:03 1997 +0200
    30.3 @@ -24,9 +24,9 @@
    30.4  \                              @@ ((corresp_exC A f `xs) (snd pr)))   \
    30.5  \                        `x) ))";
    30.6  by (rtac trans 1);
    30.7 -br fix_eq2 1;
    30.8 -br corresp_exC_def 1;
    30.9 -br beta_cfun 1;
   30.10 +by (rtac fix_eq2 1);
   30.11 +by (rtac corresp_exC_def 1);
   30.12 +by (rtac beta_cfun 1);
   30.13  by (simp_tac (!simpset addsimps [flift1_def]) 1);
   30.14  qed"corresp_exC_unfold";
   30.15  
   30.16 @@ -43,7 +43,7 @@
   30.17  goal thy "(corresp_exC A f`(at>>xs)) s = \
   30.18  \          (@cex. move A cex (f s) (fst at) (f (snd at)))  \
   30.19  \          @@ ((corresp_exC A f`xs) (snd at))";
   30.20 -br trans 1;
   30.21 +by (rtac trans 1);
   30.22  by (stac corresp_exC_unfold 1);
   30.23  by (asm_full_simp_tac (!simpset addsimps [Cons_def,flift1_def]) 1);
   30.24  by (Simp_tac 1);
   30.25 @@ -140,7 +140,7 @@
   30.26  by (safe_tac set_cs);
   30.27  by (asm_full_simp_tac (!simpset addsimps [mk_traceConc]) 1);
   30.28  by (forward_tac [reachable.reachable_n] 1);
   30.29 -ba 1;
   30.30 +by (assume_tac 1);
   30.31  by (eres_inst_tac [("x","y")] allE 1);
   30.32  by (Asm_full_simp_tac 1);
   30.33  by (asm_full_simp_tac (!simpset addsimps [move_subprop4] 
   30.34 @@ -165,7 +165,7 @@
   30.35  \     t = laststate (s,xs) \
   30.36  \ --> is_exec_frag A (s,xs @@ ys))";
   30.37  
   30.38 -br impI 1;
   30.39 +by (rtac impI 1);
   30.40  by (Seq_Finite_induct_tac 1);
   30.41  (* base_case *)
   30.42  by (fast_tac HOL_cs 1);
   30.43 @@ -193,12 +193,12 @@
   30.44  by (res_inst_tac [("t","f y")]  lemma_2_1 1);
   30.45  
   30.46  (* Finite *)
   30.47 -be move_subprop2 1;
   30.48 +by (etac move_subprop2 1);
   30.49  by (REPEAT (atac 1));
   30.50  by (rtac conjI 1);
   30.51  
   30.52  (* is_exec_frag *)
   30.53 -be  move_subprop1 1;
   30.54 +by (etac move_subprop1 1);
   30.55  by (REPEAT (atac 1));
   30.56  by (rtac conjI 1);
   30.57  
   30.58 @@ -207,10 +207,10 @@
   30.59  by (eres_inst_tac [("x","y")] allE 1);
   30.60  by (Asm_full_simp_tac 1);
   30.61  by (forward_tac [reachable.reachable_n] 1);
   30.62 -ba 1;
   30.63 +by (assume_tac 1);
   30.64  by (Asm_full_simp_tac 1);
   30.65  (* laststate *)
   30.66 -be (move_subprop3 RS sym) 1;
   30.67 +by (etac (move_subprop3 RS sym) 1);
   30.68  by (REPEAT (atac 1));
   30.69  qed"lemma_2";
   30.70  
    31.1 --- a/src/HOLCF/IOA/meta_theory/RefMappings.ML	Mon Jun 23 10:35:49 1997 +0200
    31.2 +++ b/src/HOLCF/IOA/meta_theory/RefMappings.ML	Mon Jun 23 10:42:03 1997 +0200
    31.3 @@ -25,8 +25,8 @@
    31.4  by (case_tac "ex=nil" 1);
    31.5  by (Asm_simp_tac 1);
    31.6  by (Asm_simp_tac 1);
    31.7 -bd (Finite_Last1 RS mp) 1;
    31.8 -ba 1;
    31.9 +by (dtac (Finite_Last1 RS mp) 1);
   31.10 +by (assume_tac 1);
   31.11  by (def_tac 1);
   31.12  qed"laststate_cons";
   31.13  
   31.14 @@ -92,7 +92,7 @@
   31.15  
   31.16  
   31.17  val prems = goal HOL.thy "(P ==> Q-->R) ==> P&Q --> R";
   31.18 -  by(fast_tac (!claset addDs prems) 1);
   31.19 +  by (fast_tac (!claset addDs prems) 1);
   31.20  qed "imp_conj_lemma";
   31.21  
   31.22  goal thy "!!f.[| is_weak_ref_map f C A |]\
   31.23 @@ -108,7 +108,7 @@
   31.24  by (asm_full_simp_tac (!simpset addsimps [externals_def,asig_inputs_def,
   31.25  asig_outputs_def,asig_of_def,trans_of_def]) 1);
   31.26  by (safe_tac (!claset));
   31.27 -by (rtac (expand_if RS ssubst) 1);
   31.28 +by (stac expand_if 1);
   31.29   by (rtac conjI 1);
   31.30   by (rtac impI 1);
   31.31   by (etac disjE 1);
    32.1 --- a/src/HOLCF/IOA/meta_theory/Seq.ML	Mon Jun 23 10:35:49 1997 +0200
    32.2 +++ b/src/HOLCF/IOA/meta_theory/Seq.ML	Mon Jun 23 10:42:03 1997 +0200
    32.3 @@ -48,10 +48,10 @@
    32.4  
    32.5  goal thy 
    32.6  "!!x.[|x~=UU|] ==> smap`f`(x##xs)= (f`x)##smap`f`xs"; 
    32.7 -br trans 1;
    32.8 +by (rtac trans 1);
    32.9  by (stac smap_unfold 1);
   32.10  by (Asm_full_simp_tac 1);
   32.11 -br refl 1;
   32.12 +by (rtac refl 1);
   32.13  qed"smap_cons";
   32.14  
   32.15  (* ----------------------------------------------------------- *)
   32.16 @@ -76,10 +76,10 @@
   32.17  goal thy 
   32.18  "!!x.x~=UU ==> sfilter`P`(x##xs)=   \
   32.19  \             (If P`x then x##(sfilter`P`xs) else sfilter`P`xs fi)";
   32.20 -br trans 1;
   32.21 +by (rtac trans 1);
   32.22  by (stac sfilter_unfold 1);
   32.23  by (Asm_full_simp_tac 1);
   32.24 -br refl 1;
   32.25 +by (rtac refl 1);
   32.26  qed"sfilter_cons";
   32.27  
   32.28  (* ----------------------------------------------------------- *)
   32.29 @@ -103,10 +103,10 @@
   32.30  
   32.31  goal thy 
   32.32  "!!x.x~=UU ==> sforall2`P`(x##xs)= ((P`x) andalso sforall2`P`xs)";
   32.33 -br trans 1;
   32.34 +by (rtac trans 1);
   32.35  by (stac sforall2_unfold 1);
   32.36  by (Asm_full_simp_tac 1);
   32.37 -br refl 1;
   32.38 +by (rtac refl 1);
   32.39  qed"sforall2_cons";
   32.40  
   32.41  
   32.42 @@ -133,10 +133,10 @@
   32.43  goal thy 
   32.44  "!!x.x~=UU ==> stakewhile`P`(x##xs) =   \
   32.45  \             (If P`x then x##(stakewhile`P`xs) else nil fi)";
   32.46 -br trans 1;
   32.47 +by (rtac trans 1);
   32.48  by (stac stakewhile_unfold 1);
   32.49  by (Asm_full_simp_tac 1);
   32.50 -br refl 1;
   32.51 +by (rtac refl 1);
   32.52  qed"stakewhile_cons";
   32.53  
   32.54  (* ----------------------------------------------------------- *)
   32.55 @@ -162,10 +162,10 @@
   32.56  goal thy 
   32.57  "!!x.x~=UU ==> sdropwhile`P`(x##xs) =   \
   32.58  \             (If P`x then sdropwhile`P`xs else x##xs fi)";
   32.59 -br trans 1;
   32.60 +by (rtac trans 1);
   32.61  by (stac sdropwhile_unfold 1);
   32.62  by (Asm_full_simp_tac 1);
   32.63 -br refl 1;
   32.64 +by (rtac refl 1);
   32.65  qed"sdropwhile_cons";
   32.66  
   32.67  
   32.68 @@ -192,10 +192,10 @@
   32.69  
   32.70  goal thy 
   32.71  "!!x.x~=UU ==> slast`(x##xs)= (If is_nil`xs then x else slast`xs fi)";
   32.72 -br trans 1;
   32.73 +by (rtac trans 1);
   32.74  by (stac slast_unfold 1);
   32.75  by (Asm_full_simp_tac 1);
   32.76 -br refl 1;
   32.77 +by (rtac refl 1);
   32.78  qed"slast_cons";
   32.79  
   32.80  
   32.81 @@ -220,7 +220,7 @@
   32.82  qed"sconc_UU";
   32.83  
   32.84  goal thy "(x##xs) @@ y=x##(xs @@ y)";
   32.85 -br trans 1;
   32.86 +by (rtac trans 1);
   32.87  by (stac sconc_unfold 1);
   32.88  by (Asm_full_simp_tac 1);
   32.89  by (case_tac "x=UU" 1);
   32.90 @@ -250,7 +250,7 @@
   32.91  qed"sflat_UU";
   32.92  
   32.93  goal thy "sflat`(x##xs)= x@@(sflat`xs)"; 
   32.94 -br trans 1;
   32.95 +by (rtac trans 1);
   32.96  by (stac sflat_unfold 1);
   32.97  by (Asm_full_simp_tac 1);
   32.98  by (case_tac "x=UU" 1);
   32.99 @@ -289,13 +289,13 @@
  32.100  qed"szip_UU2";
  32.101  
  32.102  goal thy "!!x.x~=UU ==> szip`(x##xs)`nil=UU";
  32.103 -br trans 1;
  32.104 +by (rtac trans 1);
  32.105  by (stac szip_unfold 1);
  32.106  by (REPEAT (Asm_full_simp_tac 1));
  32.107  qed"szip_cons_nil";
  32.108  
  32.109  goal thy "!!x.[| x~=UU; y~=UU|] ==> szip`(x##xs)`(y##ys) = <x,y>##szip`xs`ys";
  32.110 -br trans 1;
  32.111 +by (rtac trans 1);
  32.112  by (stac szip_unfold 1);
  32.113  by (REPEAT (Asm_full_simp_tac 1));
  32.114  qed"szip_cons";
  32.115 @@ -320,7 +320,7 @@
  32.116   "!!x. [|x~=UU;y~=UU|]==> (x##xs=y##ys) = (x=y & xs=ys)";
  32.117  by (rtac iffI 1);
  32.118  by (etac (hd seq.injects) 1);
  32.119 -auto();
  32.120 +by (Auto_tac());
  32.121  qed"scons_inject_eq";
  32.122  
  32.123  goal thy "!!x. nil<<x ==> nil=x";
  32.124 @@ -399,8 +399,8 @@
  32.125  (* ----------------------------------------------------  *)
  32.126  
  32.127  goal thy "Finite x --> x~=UU";
  32.128 -br impI 1;
  32.129 -be sfinite.induct 1;
  32.130 +by (rtac impI 1);
  32.131 +by (etac sfinite.induct 1);
  32.132   by (Asm_full_simp_tac 1);
  32.133  by (Asm_full_simp_tac 1);
  32.134  qed"Finite_UU_a";
  32.135 @@ -412,7 +412,7 @@
  32.136  
  32.137  goal thy "Finite x --> a~=UU --> x=a##xs --> Finite xs";
  32.138  by (strip_tac 1);
  32.139 -be sfinite.elim 1;
  32.140 +by (etac sfinite.elim 1);
  32.141  by (fast_tac (HOL_cs addss !simpset) 1);
  32.142  by (fast_tac (HOL_cs addSDs seq.injects) 1);
  32.143  qed"Finite_cons_a";
  32.144 @@ -454,8 +454,8 @@
  32.145  \  !! x s1.[|x~=UU;P(s1)|] ==> P(x##s1)\
  32.146  \  |] ==> seq_finite(s) --> P(s)";
  32.147  by (rtac seq_finite_ind_lemma 1);
  32.148 -be seq.finite_ind 1;
  32.149 - ba 1;
  32.150 +by (etac seq.finite_ind 1);
  32.151 + by (assume_tac 1);
  32.152  by (Asm_full_simp_tac 1);
  32.153  qed"seq_finite_ind";
  32.154  
    33.1 --- a/src/HOLCF/IOA/meta_theory/Sequence.ML	Mon Jun 23 10:35:49 1997 +0200
    33.2 +++ b/src/HOLCF/IOA/meta_theory/Sequence.ML	Mon Jun 23 10:42:03 1997 +0200
    33.3 @@ -13,8 +13,8 @@
    33.4  \           ==> adm (%x. P x = Q x)";
    33.5  by (res_inst_tac [("P2","(%x.(P x --> Q x) & (Q x --> P x))")] (adm_cong RS iffD1) 1);
    33.6  by (Fast_tac 1);
    33.7 -be adm_conj 1;
    33.8 -ba 1;
    33.9 +by (etac adm_conj 1);
   33.10 +by (assume_tac 1);
   33.11  qed"adm_iff";
   33.12  
   33.13  Addsimps [adm_iff];
   33.14 @@ -169,9 +169,9 @@
   33.15  \                                                  Undef => UU \
   33.16  \                                                | Def b => Def (a,b)##(Zip`xs`ys)))))";
   33.17  by (rtac trans 1);
   33.18 -br fix_eq2 1;
   33.19 -br Zip_def 1;
   33.20 -br beta_cfun 1;
   33.21 +by (rtac fix_eq2 1);
   33.22 +by (rtac Zip_def 1);
   33.23 +by (rtac beta_cfun 1);
   33.24  by (Simp_tac 1);
   33.25  qed"Zip_unfold";
   33.26  
   33.27 @@ -198,7 +198,7 @@
   33.28  qed"Zip_cons_nil";
   33.29  
   33.30  goal thy "Zip`(x>>xs)`(y>>ys)= (x,y) >> Zip`xs`ys"; 
   33.31 -br trans 1;
   33.32 +by (rtac trans 1);
   33.33  by (stac Zip_unfold 1);
   33.34  by (Simp_tac 1);
   33.35  (* FIX: Why Simp_tac 2 times. Does continuity in simpflication make job sometimes not 
   33.36 @@ -236,9 +236,9 @@
   33.37   \       | x##xs => (case x of Undef => UU | Def y => \
   33.38  \                   (if P y then y>>(Filter2 P`xs) else Filter2 P`xs)))";
   33.39  by (rtac trans 1);
   33.40 -br fix_eq2 1;
   33.41 -br Filter2_def 1;
   33.42 -br beta_cfun 1;
   33.43 +by (rtac fix_eq2 1);
   33.44 +by (rtac Filter2_def 1);
   33.45 +by (rtac beta_cfun 1);
   33.46  by (Simp_tac 1);
   33.47  
   33.48  is also possible, if then else has to be proven continuous and it would be nice if a case for 
   33.49 @@ -265,9 +265,9 @@
   33.50  
   33.51  goal thy "!!P. [| x = UU ==> P; x = nil ==> P; !!a s. x = a >> s  ==> P |] ==> P";
   33.52  by (cut_inst_tac [("x","x")] Seq_exhaust 1);
   33.53 -be disjE 1;
   33.54 +by (etac disjE 1);
   33.55  by (Asm_full_simp_tac 1);
   33.56 -be disjE 1;
   33.57 +by (etac disjE 1);
   33.58  by (Asm_full_simp_tac 1);
   33.59  by (REPEAT (etac exE 1));
   33.60  by (Asm_full_simp_tac 1);
   33.61 @@ -284,7 +284,7 @@
   33.62  goal thy "a>>s ~= UU";
   33.63  by (stac Cons_def2 1);
   33.64  by (resolve_tac seq.con_rews 1);
   33.65 -br Def_not_UU 1;
   33.66 +by (rtac Def_not_UU 1);
   33.67  qed"Cons_not_UU";
   33.68  
   33.69  
   33.70 @@ -298,7 +298,7 @@
   33.71  goal thy "~a>>s << nil";
   33.72  by (stac Cons_def2 1);
   33.73  by (resolve_tac seq.rews 1);
   33.74 -br Def_not_UU 1;
   33.75 +by (rtac Def_not_UU 1);
   33.76  qed"Cons_not_less_nil";
   33.77  
   33.78  goal thy "a>>s ~= nil";
   33.79 @@ -353,7 +353,7 @@
   33.80  section "induction";
   33.81  
   33.82  goal thy "!! P. [| adm P; P UU; P nil; !! a s. P s ==> P (a>>s)|] ==> P x";
   33.83 -be seq.ind 1;
   33.84 +by (etac seq.ind 1);
   33.85  by (REPEAT (atac 1));
   33.86  by (def_tac 1);
   33.87  by (asm_full_simp_tac (!simpset addsimps [Cons_def]) 1);
   33.88 @@ -361,15 +361,15 @@
   33.89  
   33.90  goal thy "!! P.[|P UU;P nil; !! a s. P s ==> P(a>>s) |]  \
   33.91  \               ==> seq_finite x --> P x";
   33.92 -be seq_finite_ind 1;
   33.93 +by (etac seq_finite_ind 1);
   33.94  by (REPEAT (atac 1));
   33.95  by (def_tac 1);
   33.96  by (asm_full_simp_tac (!simpset addsimps [Cons_def]) 1);
   33.97  qed"Seq_FinitePartial_ind";
   33.98  
   33.99  goal thy "!! P.[| Finite x; P nil; !! a s. [| Finite s; P s|] ==> P (a>>s) |] ==> P x";
  33.100 -be sfinite.induct 1;
  33.101 -ba 1;
  33.102 +by (etac sfinite.induct 1);
  33.103 +by (assume_tac 1);
  33.104  by (def_tac 1);
  33.105  by (asm_full_simp_tac (!simpset addsimps [Cons_def]) 1);
  33.106  qed"Seq_Finite_ind"; 
  33.107 @@ -442,10 +442,10 @@
  33.108  
  33.109  goal thy "Finite(x@@y) = (Finite (x::'a Seq) & Finite y)";
  33.110  by (rtac iffI 1);
  33.111 -be (FiniteConc_2 RS spec RS spec RS mp) 1;
  33.112 -br refl 1;
  33.113 -br (FiniteConc_1 RS mp) 1;
  33.114 -auto();
  33.115 +by (etac (FiniteConc_2 RS spec RS spec RS mp) 1);
  33.116 +by (rtac refl 1);
  33.117 +by (rtac (FiniteConc_1 RS mp) 1);
  33.118 +by (Auto_tac());
  33.119  qed"FiniteConc";
  33.120  
  33.121  Addsimps [FiniteConc];
  33.122 @@ -461,16 +461,16 @@
  33.123  by (Seq_case_simp_tac "t" 1);
  33.124  by (Asm_full_simp_tac 1);
  33.125  (* main case *)
  33.126 -auto();
  33.127 +by (Auto_tac());
  33.128  by (Seq_case_simp_tac "t" 1);
  33.129  by (Asm_full_simp_tac 1);
  33.130  qed"FiniteMap2";
  33.131  
  33.132  goal thy "Finite (Map f`s) = Finite s";
  33.133 -auto();
  33.134 -be (FiniteMap2 RS spec RS mp) 1;
  33.135 -br refl 1;
  33.136 -be FiniteMap1 1;
  33.137 +by (Auto_tac());
  33.138 +by (etac (FiniteMap2 RS spec RS mp) 1);
  33.139 +by (rtac refl 1);
  33.140 +by (etac FiniteMap1 1);
  33.141  qed"Map2Finite";
  33.142  
  33.143  
  33.144 @@ -492,27 +492,27 @@
  33.145  goal thy "!! (x:: 'a Seq). Finite x ==> !y. Finite (y:: 'a Seq) & x<<y --> x=y";
  33.146  by (Seq_Finite_induct_tac 1);
  33.147  by (strip_tac 1);
  33.148 -be conjE 1;
  33.149 -be nil_less_is_nil 1;
  33.150 +by (etac conjE 1);
  33.151 +by (etac nil_less_is_nil 1);
  33.152  (* main case *)
  33.153 -auto();
  33.154 +by (Auto_tac());
  33.155  by (Seq_case_simp_tac "y" 1);
  33.156 -auto();
  33.157 +by (Auto_tac());
  33.158  qed_spec_mp"Finite_flat";
  33.159  
  33.160  
  33.161  goal thy "adm(%(x:: 'a Seq).Finite x)";
  33.162 -br admI 1;
  33.163 +by (rtac admI 1);
  33.164  by (eres_inst_tac [("x","0")] allE 1);
  33.165  back();
  33.166 -be exE 1;
  33.167 +by (etac exE 1);
  33.168  by (REPEAT (etac conjE 1));
  33.169  by (res_inst_tac [("x","0")] allE 1);
  33.170 -ba 1;
  33.171 +by (assume_tac 1);
  33.172  by (eres_inst_tac [("x","j")] allE 1);
  33.173  by (cut_inst_tac [("x","Y 0"),("y","Y j")] Finite_flat 1);
  33.174  (* Generates a contradiction in subgoal 3 *)
  33.175 -auto();
  33.176 +by (Auto_tac());
  33.177  qed"adm_Finite";
  33.178  
  33.179  Addsimps [adm_Finite];
  33.180 @@ -543,12 +543,12 @@
  33.181  (* FIX: should be same as nil_is_Conc2 when all nils are turned to right side !! *)
  33.182  goal thy "(nil = x @@ y) = ((x::'a Seq)= nil & y = nil)";
  33.183  by (Seq_case_simp_tac "x" 1);
  33.184 -auto();
  33.185 +by (Auto_tac());
  33.186  qed"nil_is_Conc";
  33.187  
  33.188  goal thy "(x @@ y = nil) = ((x::'a Seq)= nil & y = nil)";
  33.189  by (Seq_case_simp_tac "x" 1);
  33.190 -auto();
  33.191 +by (Auto_tac());
  33.192  qed"nil_is_Conc2";
  33.193  
  33.194  
  33.195 @@ -655,14 +655,14 @@
  33.196  by (strip_tac 1); 
  33.197  by (Seq_case_simp_tac "sa" 1);
  33.198  by (Asm_full_simp_tac 1);
  33.199 -auto();
  33.200 +by (Auto_tac());
  33.201  qed"Forall_prefix";
  33.202   
  33.203  bind_thm ("Forall_prefixclosed",Forall_prefix RS spec RS mp RS mp);
  33.204  
  33.205  
  33.206  goal thy "!! h. [| Finite h; Forall P s; s= h @@ t |] ==> Forall P t";
  33.207 -auto();
  33.208 +by (Auto_tac());
  33.209  qed"Forall_postfixclosed";
  33.210  
  33.211  
  33.212 @@ -715,7 +715,7 @@
  33.213  by (res_inst_tac[("x","ys")] Seq_induct 1);
  33.214  (* adm *)
  33.215  (* FIX: not admissible, search other proof!! *)
  33.216 -br adm_all 1;
  33.217 +by (rtac adm_all 1);
  33.218  (* base cases *)
  33.219  by (Simp_tac 1);
  33.220  by (Simp_tac 1);
  33.221 @@ -741,23 +741,23 @@
  33.222  \                (Forall (%x. ~P x) ys  & ~Finite ys)";
  33.223  by (rtac conjI 1);
  33.224  by (cut_inst_tac [] (FilterUU_nFinite_lemma2 RS mp COMP rev_contrapos) 1);
  33.225 -auto();
  33.226 +by (Auto_tac());
  33.227  by (blast_tac (!claset addSDs [FilterUU_nFinite_lemma1]) 1);
  33.228  qed"FilternPUUForallP";
  33.229  
  33.230  
  33.231  goal thy  "!! Q P.[| Forall Q ys; Finite ys; !!x. Q x ==> ~P x|] \
  33.232  \   ==> Filter P`ys = nil";
  33.233 -be ForallnPFilterPnil 1;
  33.234 -be ForallPForallQ 1;
  33.235 -auto();
  33.236 +by (etac ForallnPFilterPnil 1);
  33.237 +by (etac ForallPForallQ 1);
  33.238 +by (Auto_tac());
  33.239  qed"ForallQFilterPnil";
  33.240  
  33.241  goal thy "!! Q P. [| ~Finite ys; Forall Q ys;  !!x. Q x ==> ~P x|] \
  33.242  \   ==> Filter P`ys = UU ";
  33.243 -be ForallnPFilterPUU 1;
  33.244 -be ForallPForallQ 1;
  33.245 -auto();
  33.246 +by (etac ForallnPFilterPUU 1);
  33.247 +by (etac ForallPForallQ 1);
  33.248 +by (Auto_tac());
  33.249  qed"ForallQFilterPUU";
  33.250  
  33.251  
  33.252 @@ -773,26 +773,26 @@
  33.253  
  33.254  
  33.255  goal thy"!! P. [| !!x. Q x==> P x |] ==> Forall P (Takewhile Q`x)";
  33.256 -br ForallPForallQ 1;
  33.257 -br ForallPTakewhileP 1;
  33.258 -auto();
  33.259 +by (rtac ForallPForallQ 1);
  33.260 +by (rtac ForallPTakewhileP 1);
  33.261 +by (Auto_tac());
  33.262  qed"ForallPTakewhileQ";
  33.263  
  33.264  
  33.265  goal thy  "!! Q P.[| Finite (Takewhile Q`ys); !!x. Q x ==> ~P x |] \
  33.266  \   ==> Filter P`(Takewhile Q`ys) = nil";
  33.267 -be ForallnPFilterPnil 1;
  33.268 -br ForallPForallQ 1;
  33.269 -br ForallPTakewhileP 1;
  33.270 -auto();
  33.271 +by (etac ForallnPFilterPnil 1);
  33.272 +by (rtac ForallPForallQ 1);
  33.273 +by (rtac ForallPTakewhileP 1);
  33.274 +by (Auto_tac());
  33.275  qed"FilterPTakewhileQnil";
  33.276  
  33.277  goal thy "!! Q P. [| !!x. Q x ==> P x |] ==> \
  33.278  \            Filter P`(Takewhile Q`ys) = (Takewhile Q`ys)";
  33.279 -br ForallPFilterPid 1;
  33.280 -br ForallPForallQ 1;
  33.281 -br ForallPTakewhileP 1;
  33.282 -auto();
  33.283 +by (rtac ForallPFilterPid 1);
  33.284 +by (rtac ForallPForallQ 1);
  33.285 +by (rtac ForallPTakewhileP 1);
  33.286 +by (Auto_tac());
  33.287  qed"FilterPTakewhileQid";
  33.288  
  33.289  Addsimps [ForallPTakewhileP,ForallPTakewhileQ,
  33.290 @@ -840,26 +840,26 @@
  33.291  (* FIX: pay attention: is only admissible with chain-finite package to be added to 
  33.292          adm test *)
  33.293  by (Seq_induct_tac "y" [] 1);
  33.294 -br adm_all 1;
  33.295 +by (rtac adm_all 1);
  33.296  by (Asm_full_simp_tac 1); 
  33.297  by (case_tac "P a" 1);
  33.298  by (Asm_full_simp_tac 1); 
  33.299 -br impI 1;
  33.300 +by (rtac impI 1);
  33.301  by (hyp_subst_tac 1);
  33.302  by (Asm_full_simp_tac 1); 
  33.303  (* ~ P a *)
  33.304  by (Asm_full_simp_tac 1); 
  33.305 -br impI 1;
  33.306 +by (rtac impI 1);
  33.307  by (rotate_tac ~1 1);
  33.308  by (Asm_full_simp_tac 1); 
  33.309  by (REPEAT (etac conjE 1));
  33.310 -ba 1;
  33.311 +by (assume_tac 1);
  33.312  qed"divide_Seq_lemma";
  33.313  
  33.314  goal thy "!! x. (x>>xs) << Filter P`y  \
  33.315  \   ==> y = ((Takewhile (%a. ~ P a)`y) @@ (x >> TL`(Dropwhile (%a.~P a)`y))) \
  33.316  \      & Finite (Takewhile (%a. ~ P a)`y)  & P x";
  33.317 -br (divide_Seq_lemma RS mp) 1;
  33.318 +by (rtac (divide_Seq_lemma RS mp) 1);
  33.319  by (dres_inst_tac [("fo","HD"),("xa","x>>xs")]  monofun_cfun_arg 1);
  33.320  by (Asm_full_simp_tac 1); 
  33.321  qed"divide_Seq";
  33.322 @@ -869,7 +869,7 @@
  33.323  (* FIX: pay attention: is only admissible with chain-finite package to be added to 
  33.324          adm test *)
  33.325  by (Seq_induct_tac "y" [] 1);
  33.326 -br adm_all 1;
  33.327 +by (rtac adm_all 1);
  33.328  by (case_tac "P a" 1);
  33.329  by (Asm_full_simp_tac 1); 
  33.330  by (Asm_full_simp_tac 1); 
  33.331 @@ -879,18 +879,18 @@
  33.332  goal thy "!!y. ~Forall P y  \
  33.333  \  ==> ? x. y= (Takewhile P`y @@ (x >> TL`(Dropwhile P`y))) & \
  33.334  \      Finite (Takewhile P`y) & (~ P x)";
  33.335 -bd (nForall_HDFilter RS mp) 1;
  33.336 +by (dtac (nForall_HDFilter RS mp) 1);
  33.337  by (safe_tac set_cs);
  33.338  by (res_inst_tac [("x","x")] exI 1);
  33.339  by (cut_inst_tac [("P1","%x. ~ P x")] (divide_Seq_lemma RS mp) 1);
  33.340 -auto();
  33.341 +by (Auto_tac());
  33.342  qed"divide_Seq2";
  33.343  
  33.344  
  33.345  goal thy  "!! y. ~Forall P y \
  33.346  \  ==> ? x bs rs. y= (bs @@ (x>>rs)) & Finite bs & Forall P bs & (~ P x)";
  33.347  by (cut_inst_tac [] divide_Seq2 1);
  33.348 -auto();
  33.349 +by (Auto_tac());
  33.350  qed"divide_Seq3";
  33.351  
  33.352  Addsimps [FilterPQ,FilterConc,Conc_cong];
  33.353 @@ -903,8 +903,8 @@
  33.354  
  33.355  goal thy "(!n. seq_take n`x = seq_take n`x') = (x = x')";
  33.356  by (rtac iffI 1);
  33.357 -br seq.take_lemma 1;
  33.358 -auto();
  33.359 +by (rtac seq.take_lemma 1);
  33.360 +by (Auto_tac());
  33.361  qed"seq_take_lemma";
  33.362  
  33.363  goal thy 
  33.364 @@ -913,9 +913,9 @@
  33.365  by (Seq_induct_tac "x" [] 1);
  33.366  by (strip_tac 1);
  33.367  by (res_inst_tac [("n","n")] natE 1);
  33.368 -auto();
  33.369 +by (Auto_tac());
  33.370  by (res_inst_tac [("n","n")] natE 1);
  33.371 -auto();
  33.372 +by (Auto_tac());
  33.373  qed"take_reduction1";
  33.374  
  33.375  
  33.376 @@ -935,9 +935,9 @@
  33.377  by (Seq_induct_tac "x" [] 1);
  33.378  by (strip_tac 1);
  33.379  by (res_inst_tac [("n","n")] natE 1);
  33.380 -auto();
  33.381 +by (Auto_tac());
  33.382  by (res_inst_tac [("n","n")] natE 1);
  33.383 -auto();
  33.384 +by (Auto_tac());
  33.385  qed"take_reduction_less1";
  33.386  
  33.387  
  33.388 @@ -953,9 +953,9 @@
  33.389  by (res_inst_tac [("t","s1")] (seq.reach RS subst)  1);
  33.390  by (res_inst_tac [("t","s2")] (seq.reach RS subst)  1);
  33.391  by (rtac (fix_def2 RS ssubst ) 1);
  33.392 -by (rtac (contlub_cfun_fun RS ssubst) 1);
  33.393 +by (stac contlub_cfun_fun 1);
  33.394  by (rtac is_chain_iterate 1);
  33.395 -by (rtac (contlub_cfun_fun RS ssubst) 1);
  33.396 +by (stac contlub_cfun_fun 1);
  33.397  by (rtac is_chain_iterate 1);
  33.398  by (rtac lub_mono 1);
  33.399  by (rtac (is_chain_iterate RS ch2ch_fappL) 1);
  33.400 @@ -967,9 +967,9 @@
  33.401  
  33.402  goal thy "(!n. seq_take n`x << seq_take n`x') = (x << x')";
  33.403  by (rtac iffI 1);
  33.404 -br take_lemma_less1 1;
  33.405 -auto();
  33.406 -be monofun_cfun_arg 1;
  33.407 +by (rtac take_lemma_less1 1);
  33.408 +by (Auto_tac());
  33.409 +by (etac monofun_cfun_arg 1);
  33.410  qed"take_lemma_less";
  33.411  
  33.412  (* ------------------------------------------------------------------
  33.413 @@ -991,8 +991,8 @@
  33.414  \              ==> A x --> (f x)=(g x)";
  33.415  by (case_tac "Forall Q x" 1);
  33.416  by (auto_tac (!claset addSDs [divide_Seq3],!simpset));
  33.417 -br seq.take_lemma 1;
  33.418 -auto();
  33.419 +by (rtac seq.take_lemma 1);
  33.420 +by (Auto_tac());
  33.421  qed"take_lemma_principle2";
  33.422  
  33.423  
  33.424 @@ -1011,14 +1011,14 @@
  33.425  \                         ==>   seq_take (Suc n)`(f (s1 @@ y>>s2)) \
  33.426  \                             = seq_take (Suc n)`(g (s1 @@ y>>s2)) |] \
  33.427  \              ==> A x --> (f x)=(g x)";
  33.428 -br impI 1;
  33.429 -br seq.take_lemma 1;
  33.430 -br mp 1;
  33.431 -ba 2;
  33.432 +by (rtac impI 1);
  33.433 +by (rtac seq.take_lemma 1);
  33.434 +by (rtac mp 1);
  33.435 +by (assume_tac 2);
  33.436  by (res_inst_tac [("x","x")] spec 1);
  33.437 -br nat_induct 1;
  33.438 +by (rtac nat_induct 1);
  33.439  by (Simp_tac 1);
  33.440 -br allI 1;
  33.441 +by (rtac allI 1);
  33.442  by (case_tac "Forall Q xa" 1);
  33.443  by (SELECT_GOAL (auto_tac (!claset addSIs [seq_take_lemma RS iffD2 RS spec],
  33.444                             !simpset)) 1);
  33.445 @@ -1033,13 +1033,13 @@
  33.446  \                         ==>   seq_take n`(f (s1 @@ y>>s2)) \
  33.447  \                             = seq_take n`(g (s1 @@ y>>s2)) |] \
  33.448  \              ==> A x --> (f x)=(g x)";
  33.449 -br impI 1;
  33.450 -br seq.take_lemma 1;
  33.451 -br mp 1;
  33.452 -ba 2;
  33.453 +by (rtac impI 1);
  33.454 +by (rtac seq.take_lemma 1);
  33.455 +by (rtac mp 1);
  33.456 +by (assume_tac 2);
  33.457  by (res_inst_tac [("x","x")] spec 1);
  33.458 -br less_induct 1;
  33.459 -br allI 1;
  33.460 +by (rtac less_induct 1);
  33.461 +by (rtac allI 1);
  33.462  by (case_tac "Forall Q xa" 1);
  33.463  by (SELECT_GOAL (auto_tac (!claset addSIs [seq_take_lemma RS iffD2 RS spec],
  33.464                             !simpset)) 1);
  33.465 @@ -1057,14 +1057,14 @@
  33.466  \                             = seq_take n`(g (s1 @@ y>>s2) h1 h2) |] \
  33.467  \              ==> ! h1 h2. (A x h1 h2) --> (f x h1 h2)=(g x h1 h2)";
  33.468  by (strip_tac 1);
  33.469 -br seq.take_lemma 1;
  33.470 -br mp 1;
  33.471 -ba 2;
  33.472 +by (rtac seq.take_lemma 1);
  33.473 +by (rtac mp 1);
  33.474 +by (assume_tac 2);
  33.475  by (res_inst_tac [("x","h2a")] spec 1);
  33.476  by (res_inst_tac [("x","h1a")] spec 1);
  33.477  by (res_inst_tac [("x","x")] spec 1);
  33.478 -br less_induct 1;
  33.479 -br allI 1;
  33.480 +by (rtac less_induct 1);
  33.481 +by (rtac allI 1);
  33.482  by (case_tac "Forall Q xa" 1);
  33.483  by (SELECT_GOAL (auto_tac (!claset addSIs [seq_take_lemma RS iffD2 RS spec],
  33.484                             !simpset)) 1);
  33.485 @@ -1083,15 +1083,15 @@
  33.486  
  33.487  by (res_inst_tac [("t","f x = g x"),
  33.488                    ("s","!n. seq_take n`(f x) = seq_take n`(g x)")] subst 1);
  33.489 -br seq_take_lemma 1;
  33.490 +by (rtac seq_take_lemma 1);
  33.491  
  33.492  wie ziehe ich n durch P, d.h. evtl. ns in P muessen umbenannt werden.....
  33.493  
  33.494  
  33.495  FIX
  33.496  
  33.497 -br less_induct 1;
  33.498 -br allI 1;
  33.499 +by (rtac less_induct 1);
  33.500 +by (rtac allI 1);
  33.501  by (case_tac "Forall Q xa" 1);
  33.502  by (SELECT_GOAL (auto_tac (!claset addSIs [seq_take_lemma RS iffD2 RS spec],
  33.503                             !simpset)) 1);
  33.504 @@ -1110,14 +1110,14 @@
  33.505  \                    ==>   seq_take (Suc n)`(f (y>>s)) \
  33.506  \                        = seq_take (Suc n)`(g (y>>s)) |] \
  33.507  \              ==> A x --> (f x)=(g x)";
  33.508 -br impI 1;
  33.509 -br seq.take_lemma 1;
  33.510 -br mp 1;
  33.511 -ba 2;
  33.512 +by (rtac impI 1);
  33.513 +by (rtac seq.take_lemma 1);
  33.514 +by (rtac mp 1);
  33.515 +by (assume_tac 2);
  33.516  by (res_inst_tac [("x","x")] spec 1);
  33.517 -br nat_induct 1;
  33.518 +by (rtac nat_induct 1);
  33.519  by (Simp_tac 1);
  33.520 -br allI 1;
  33.521 +by (rtac allI 1);
  33.522  by (Seq_case_simp_tac "xa" 1);
  33.523  qed"take_lemma_in_eq_out";
  33.524  
  33.525 @@ -1181,7 +1181,7 @@
  33.526  
  33.527  goal thy "Map f`(x@@y) = (Map f`x) @@ (Map f`y)";
  33.528  by (res_inst_tac [("A1","%x.True"),("x1","x")] (take_lemma_in_eq_out RS mp) 1);
  33.529 -auto();
  33.530 +by (Auto_tac());
  33.531  qed"MapConc_takelemma";
  33.532  
  33.533  
    34.1 --- a/src/HOLCF/IOA/meta_theory/ShortExecutions.ML	Mon Jun 23 10:35:49 1997 +0200
    34.2 +++ b/src/HOLCF/IOA/meta_theory/ShortExecutions.ML	Mon Jun 23 10:42:03 1997 +0200
    34.3 @@ -47,7 +47,7 @@
    34.4  goal thy "oraclebuild P`s`(x>>t) = \
    34.5  \         (Takewhile (%a.~ P a)`s)   \
    34.6  \          @@ (x>>(oraclebuild P`(TL`(Dropwhile (%a.~ P a)`s))`t))";     
    34.7 -br trans 1;
    34.8 +by (rtac trans 1);
    34.9  by (stac oraclebuild_unfold 1);
   34.10  by (asm_full_simp_tac (!simpset addsimps [Cons_def]) 1);
   34.11  by (simp_tac (!simpset addsimps [Cons_def]) 1);
   34.12 @@ -65,7 +65,7 @@
   34.13  \           ==> Cut P s =nil";
   34.14  by (subgoal_tac "Filter P`s = nil" 1);
   34.15  by (asm_simp_tac (!simpset addsimps [oraclebuild_nil]) 1);
   34.16 -br ForallQFilterPnil 1;
   34.17 +by (rtac ForallQFilterPnil 1);
   34.18  by (REPEAT (atac 1));
   34.19  qed"Cut_nil";
   34.20  
   34.21 @@ -74,7 +74,7 @@
   34.22  \           ==> Cut P s =UU";
   34.23  by (subgoal_tac "Filter P`s= UU" 1);
   34.24  by (asm_simp_tac (!simpset addsimps [oraclebuild_UU]) 1);
   34.25 -br ForallQFilterPUU 1;
   34.26 +by (rtac ForallQFilterPUU 1);
   34.27  by (REPEAT (atac 1));
   34.28  qed"Cut_UU";
   34.29  
   34.30 @@ -106,7 +106,7 @@
   34.31               ForallQFilterPUU]) 1);
   34.32  (* main case *)
   34.33  by (asm_full_simp_tac (!simpset addsimps [Cut_Cons,ForallQFilterPnil]) 1);
   34.34 -auto();
   34.35 +by (Auto_tac());
   34.36  qed"FilterCut";
   34.37  
   34.38  
   34.39 @@ -123,8 +123,8 @@
   34.40               ForallQFilterPUU]) 1);
   34.41  (* main case *)
   34.42  by (asm_full_simp_tac (!simpset addsimps [Cut_Cons,ForallQFilterPnil]) 1);
   34.43 -br take_reduction 1;
   34.44 -auto();
   34.45 +by (rtac take_reduction 1);
   34.46 +by (Auto_tac());
   34.47  qed"Cut_idemp";
   34.48  
   34.49  
   34.50 @@ -136,45 +136,45 @@
   34.51  by (Fast_tac 3);
   34.52  by (case_tac "Finite s" 1);
   34.53  by (asm_full_simp_tac (!simpset addsimps [Cut_nil]) 1); 
   34.54 -br (Cut_nil RS sym) 1;
   34.55 +by (rtac (Cut_nil RS sym) 1);
   34.56  by (asm_full_simp_tac (!simpset addsimps [ForallMap,o_def]) 1); 
   34.57  by (asm_full_simp_tac (!simpset addsimps [Map2Finite]) 1);
   34.58  (* csae ~ Finite s *)
   34.59  by (asm_full_simp_tac (!simpset addsimps [Cut_UU]) 1);
   34.60 -br (Cut_UU RS sym) 1;
   34.61 +by (rtac (Cut_UU RS sym) 1);
   34.62  by (asm_full_simp_tac (!simpset addsimps [ForallMap,o_def]) 1); 
   34.63  by (asm_full_simp_tac (!simpset addsimps [Map2Finite]) 1);
   34.64  (* main case *)
   34.65  by (asm_full_simp_tac (!simpset addsimps [Cut_Cons,MapConc,
   34.66            ForallMap,FiniteMap1,o_def]) 1);
   34.67 -br take_reduction 1;
   34.68 -auto();
   34.69 +by (rtac take_reduction 1);
   34.70 +by (Auto_tac());
   34.71  qed"MapCut";
   34.72  
   34.73  
   34.74  goal thy "~Finite s --> Cut P s << s";
   34.75  by (strip_tac 1);
   34.76 -br (take_lemma_less RS iffD1) 1;
   34.77 +by (rtac (take_lemma_less RS iffD1) 1);
   34.78  by (strip_tac 1);
   34.79 -br mp 1;
   34.80 -ba 2;
   34.81 +by (rtac mp 1);
   34.82 +by (assume_tac 2);
   34.83  by (thin_tac' 1 1);
   34.84  by (res_inst_tac [("x","s")] spec 1);
   34.85 -br less_induct 1;
   34.86 +by (rtac less_induct 1);
   34.87  by (strip_tac 1);
   34.88  ren "na n s" 1;
   34.89  by (case_tac "Forall (%x. ~ P x) s" 1);
   34.90 -br (take_lemma_less RS iffD2 RS spec) 1;
   34.91 +by (rtac (take_lemma_less RS iffD2 RS spec) 1);
   34.92  by (asm_full_simp_tac (!simpset addsimps [Cut_UU]) 1);
   34.93  (* main case *)
   34.94 -bd divide_Seq3 1;
   34.95 +by (dtac divide_Seq3 1);
   34.96  by (REPEAT (etac exE 1));
   34.97  by (REPEAT (etac conjE 1));
   34.98  by (hyp_subst_tac 1);
   34.99  by (asm_full_simp_tac (!simpset addsimps [Cut_Cons]) 1);
  34.100 -br take_reduction_less 1;
  34.101 +by (rtac take_reduction_less 1);
  34.102  (* auto makes also reasoning about Finiteness of parts of s ! *)
  34.103 -auto();
  34.104 +by (Auto_tac());
  34.105  qed_spec_mp"Cut_prefixcl_nFinite";
  34.106  
  34.107  
  34.108 @@ -184,24 +184,24 @@
  34.109  goal thy "Finite s --> (? y. s = Cut P s @@ y)";
  34.110  by (strip_tac 1);
  34.111  by (rtac exI 1);
  34.112 -br seq.take_lemma 1;
  34.113 -br mp 1;
  34.114 -ba 2;
  34.115 +by (rtac seq.take_lemma 1);
  34.116 +by (rtac mp 1);
  34.117 +by (assume_tac 2);
  34.118  by (thin_tac' 1 1);
  34.119  by (res_inst_tac [("x","s")] spec 1);
  34.120 -br less_induct 1;
  34.121 +by (rtac less_induct 1);
  34.122  by (strip_tac 1);
  34.123  ren "na n s" 1;
  34.124  by (case_tac "Forall (%x. ~ P x) s" 1);
  34.125 -br (seq_take_lemma RS iffD2 RS spec) 1;
  34.126 +by (rtac (seq_take_lemma RS iffD2 RS spec) 1);
  34.127  by (asm_full_simp_tac (!simpset addsimps [Cut_nil]) 1);
  34.128  (* main case *)
  34.129 -bd divide_Seq3 1;
  34.130 +by (dtac divide_Seq3 1);
  34.131  by (REPEAT (etac exE 1));
  34.132  by (REPEAT (etac conjE 1));
  34.133  by (hyp_subst_tac 1);
  34.134  by (asm_full_simp_tac (!simpset addsimps [Cut_Cons,Conc_assoc]) 1);
  34.135 -br take_reduction 1;
  34.136 +by (rtac take_reduction 1);
  34.137  
  34.138  qed_spec_mp"Cut_prefixcl_Finite";
  34.139  
  34.140 @@ -212,13 +212,13 @@
  34.141  goal thy "!!ex .is_exec_frag A (s,ex) ==> is_exec_frag A (s,Cut P ex)";
  34.142  by (case_tac "Finite ex" 1);
  34.143  by (cut_inst_tac [("s","ex"),("P","P")] Cut_prefixcl_Finite 1);
  34.144 -ba 1;
  34.145 -be exE 1;
  34.146 -br exec_prefix2closed 1;
  34.147 +by (assume_tac 1);
  34.148 +by (etac exE 1);
  34.149 +by (rtac exec_prefix2closed 1);
  34.150  by (eres_inst_tac [("s","ex"),("t","Cut P ex @@ y")] subst 1);
  34.151 -ba 1;
  34.152 -be exec_prefixclosed 1;
  34.153 -be Cut_prefixcl_nFinite 1;
  34.154 +by (assume_tac 1);
  34.155 +by (etac exec_prefixclosed 1);
  34.156 +by (etac Cut_prefixcl_nFinite 1);
  34.157  qed"execThruCut";
  34.158  
  34.159  
  34.160 @@ -251,14 +251,14 @@
  34.161  
  34.162  by (simp_tac (!simpset addsimps [filter_act_def]) 1);
  34.163  by (subgoal_tac "Map fst`(Cut (%a.fst a: ext A) y)= Cut (%a.a:ext A) (Map fst`y)" 1);
  34.164 -br (rewrite_rule [o_def] MapCut) 2;
  34.165 +by (rtac (rewrite_rule [o_def] MapCut) 2);
  34.166  by (asm_full_simp_tac (!simpset addsimps [FilterCut RS sym]) 1);
  34.167  
  34.168  (* Subgoal 3: Lemma: Cut idempotent  *)
  34.169  
  34.170  by (simp_tac (!simpset addsimps [LastActExtsch_def,filter_act_def]) 1);
  34.171  by (subgoal_tac "Map fst`(Cut (%a.fst a: ext A) y)= Cut (%a.a:ext A) (Map fst`y)" 1);
  34.172 -br (rewrite_rule [o_def] MapCut) 2;
  34.173 +by (rtac (rewrite_rule [o_def] MapCut) 2);
  34.174  by (asm_full_simp_tac (!simpset addsimps [Cut_idemp]) 1);
  34.175  qed"exists_LastActExtsch";
  34.176  
  34.177 @@ -270,19 +270,19 @@
  34.178  goalw  thy [LastActExtsch_def]
  34.179    "!! A. [| LastActExtsch A sch; Filter (%x.x:ext A)`sch = nil |] \
  34.180  \   ==> sch=nil";
  34.181 -bd FilternPnilForallP 1;
  34.182 -be conjE 1;
  34.183 -bd Cut_nil 1;
  34.184 -ba 1;
  34.185 +by (dtac FilternPnilForallP 1);
  34.186 +by (etac conjE 1);
  34.187 +by (dtac Cut_nil 1);
  34.188 +by (assume_tac 1);
  34.189  by (Asm_full_simp_tac 1);
  34.190  qed"LastActExtimplnil";
  34.191  
  34.192  goalw  thy [LastActExtsch_def]
  34.193    "!! A. [| LastActExtsch A sch; Filter (%x.x:ext A)`sch = UU |] \
  34.194  \   ==> sch=UU";
  34.195 -bd FilternPUUForallP 1;
  34.196 -be conjE 1;
  34.197 -bd Cut_UU 1;
  34.198 -ba 1;
  34.199 +by (dtac FilternPUUForallP 1);
  34.200 +by (etac conjE 1);
  34.201 +by (dtac Cut_UU 1);
  34.202 +by (assume_tac 1);
  34.203  by (Asm_full_simp_tac 1);
  34.204  qed"LastActExtimplUU";
    35.1 --- a/src/HOLCF/IOA/meta_theory/Traces.ML	Mon Jun 23 10:35:49 1997 +0200
    35.2 +++ b/src/HOLCF/IOA/meta_theory/Traces.ML	Mon Jun 23 10:42:03 1997 +0200
    35.3 @@ -71,9 +71,9 @@
    35.4  \             `x) \
    35.5  \   ))";
    35.6  by (rtac trans 1);
    35.7 -br fix_eq2 1;
    35.8 -br is_exec_fragC_def 1;
    35.9 -br beta_cfun 1;
   35.10 +by (rtac fix_eq2 1);
   35.11 +by (rtac is_exec_fragC_def 1);
   35.12 +by (rtac beta_cfun 1);
   35.13  by (simp_tac (!simpset addsimps [flift1_def]) 1);
   35.14  qed"is_exec_fragC_unfold";
   35.15  
   35.16 @@ -90,7 +90,7 @@
   35.17  goal thy "(is_exec_fragC A`(pr>>xs)) s = \
   35.18  \                        (Def ((s,pr):trans_of A) \
   35.19  \                andalso (is_exec_fragC A`xs)(snd pr))";
   35.20 -br trans 1;
   35.21 +by (rtac trans 1);
   35.22  by (stac is_exec_fragC_unfold 1);
   35.23  by (asm_full_simp_tac (!simpset addsimps [Cons_def,flift1_def]) 1);
   35.24  by (Simp_tac 1);
   35.25 @@ -178,8 +178,8 @@
   35.26  
   35.27  by (asm_full_simp_tac (!simpset addsimps [executions_def]) 1);
   35.28  by (pair_tac "x" 1);
   35.29 -br (execfrag_in_sig RS spec RS mp) 1;
   35.30 -auto();
   35.31 +by (rtac (execfrag_in_sig RS spec RS mp) 1);
   35.32 +by (Auto_tac());
   35.33  qed"exec_in_sig";
   35.34  
   35.35  goalw thy [schedules_def,has_schedule_def]
   35.36 @@ -200,7 +200,7 @@
   35.37  by (strip_tac 1);
   35.38  by (Seq_case_simp_tac "xa" 1);
   35.39  by (pair_tac "a" 1);
   35.40 -auto();
   35.41 +by (Auto_tac());
   35.42  qed"execfrag_prefixclosed";
   35.43  
   35.44  bind_thm ("exec_prefixclosed",conjI RS (execfrag_prefixclosed RS spec RS spec RS mp));
   35.45 @@ -213,6 +213,6 @@
   35.46  by (strip_tac 1);
   35.47  by (Seq_case_simp_tac "s" 1);
   35.48  by (pair_tac "a" 1);
   35.49 -auto();
   35.50 +by (Auto_tac());
   35.51  qed_spec_mp"exec_prefix2closed";
   35.52  
    36.1 --- a/src/HOLCF/Lift.ML	Mon Jun 23 10:35:49 1997 +0200
    36.2 +++ b/src/HOLCF/Lift.ML	Mon Jun 23 10:42:03 1997 +0200
    36.3 @@ -8,7 +8,7 @@
    36.4  
    36.5  (* flift1 is continuous in its argument itself*)
    36.6  goal thy "cont (lift_case UU f)"; 
    36.7 -br flatdom_strict2cont 1;
    36.8 +by (rtac flatdom_strict2cont 1);
    36.9  by (Simp_tac 1);
   36.10  qed"cont_flift1_arg";
   36.11  
   36.12 @@ -17,7 +17,7 @@
   36.13  
   36.14  goal thy "!!f. [| !! a.cont (%y. (f y) a) |] ==> \
   36.15  \          cont (%y. lift_case UU (f y))";
   36.16 -br cont2cont_CF1L_rev 1;
   36.17 +by (rtac cont2cont_CF1L_rev 1);
   36.18  by (strip_tac 1);
   36.19  by (res_inst_tac [("x","y")] Lift_cases 1);
   36.20  by (Asm_simp_tac 1);
   36.21 @@ -29,18 +29,18 @@
   36.22  
   36.23  goal thy "!!f. [| !! a.cont (%y. (f y) a); cont g|] ==> \
   36.24  \   cont (%y. lift_case UU (f y) (g y))";
   36.25 -br cont2cont_app 1;
   36.26 +by (rtac cont2cont_app 1);
   36.27  back();
   36.28  by (safe_tac set_cs);
   36.29 -br cont_flift1_not_arg 1;
   36.30 -auto();
   36.31 -br cont_flift1_arg 1;
   36.32 +by (rtac cont_flift1_not_arg 1);
   36.33 +by (Auto_tac());
   36.34 +by (rtac cont_flift1_arg 1);
   36.35  qed"cont_flift1_arg_and_not_arg";
   36.36  
   36.37  (* flift2 is continuous in its argument itself *)
   36.38  
   36.39  goal thy "cont (lift_case UU (%y. Def (f y)))";
   36.40 -br flatdom_strict2cont 1;
   36.41 +by (rtac flatdom_strict2cont 1);
   36.42  by (Simp_tac 1);
   36.43  qed"cont_flift2_arg";
   36.44  
    37.1 --- a/src/HOLCF/Lift3.ML	Mon Jun 23 10:35:49 1997 +0200
    37.2 +++ b/src/HOLCF/Lift3.ML	Mon Jun 23 10:42:03 1997 +0200
    37.3 @@ -71,7 +71,7 @@
    37.4  (* --------------------------------------------------------*)
    37.5  
    37.6  goal thy "(x::'a lift) << y = (x=y | x=UU)";
    37.7 -br (inst_lift_po RS ssubst) 1;
    37.8 +by (stac inst_lift_po 1);
    37.9  by (Simp_tac 1);
   37.10  qed"less_lift";
   37.11  
   37.12 @@ -96,13 +96,13 @@
   37.13  
   37.14  goal thy
   37.15    "P(lift_case a b x) = ((x=UU --> P a) & (!y. x = Def y --> P(b y)))";
   37.16 -by(lift.induct_tac "x" 1);
   37.17 -by(ALLGOALS Asm_simp_tac);
   37.18 +by (lift.induct_tac "x" 1);
   37.19 +by (ALLGOALS Asm_simp_tac);
   37.20  qed "expand_lift_case";
   37.21  
   37.22  goal thy "(x~=UU)=(? y.x=Def y)";
   37.23 -br iffI 1;
   37.24 -br Lift_cases 1;
   37.25 +by (rtac iffI 1);
   37.26 +by (rtac Lift_cases 1);
   37.27  by (REPEAT (fast_tac (HOL_cs addSIs lift.distinct) 1));
   37.28  qed"not_Undef_is_Def";
   37.29  
   37.30 @@ -126,7 +126,7 @@
   37.31  back();
   37.32  by (rtac iffI 1);
   37.33  by (asm_full_simp_tac (!simpset addsimps [inst_lift_po] ) 1);
   37.34 -be (antisym_less_inverse RS conjunct1) 1;
   37.35 +by (etac (antisym_less_inverse RS conjunct1) 1);
   37.36  qed"Def_inject_less_eq";
   37.37  
   37.38  goal thy "Def x << y = (Def x = y)";
   37.39 @@ -146,15 +146,15 @@
   37.40  (* Two specific lemmas for the combination of LCF and HOL terms *)
   37.41  
   37.42  goal thy "!!f.[|cont g; cont f|] ==> cont(%x. ((f x)`(g x)) s)";
   37.43 -br cont2cont_CF1L 1;
   37.44 +by (rtac cont2cont_CF1L 1);
   37.45  by (REPEAT (resolve_tac cont_lemmas1 1));
   37.46 -auto();
   37.47 +by (Auto_tac());
   37.48  qed"cont_fapp_app";
   37.49  
   37.50  goal thy "!!f.[|cont g; cont f|] ==> cont(%x. ((f x)`(g x)) s t)";
   37.51 -br cont2cont_CF1L 1;
   37.52 -be cont_fapp_app 1;
   37.53 -ba 1;
   37.54 +by (rtac cont2cont_CF1L 1);
   37.55 +by (etac cont_fapp_app 1);
   37.56 +by (assume_tac 1);
   37.57  qed"cont_fapp_app_app";
   37.58  
   37.59