# HG changeset patch
# User paulson
# Date 867055323 -7200
# Node ID a8ab7c64817c785e0fae3520dba58987c123b11d
# Parent  fdb1768ebd3e2528e101a2317e7e889067cbfaae
Ran expandshort

diff -r fdb1768ebd3e -r a8ab7c64817c src/HOL/Arith.ML
--- a/src/HOL/Arith.ML	Mon Jun 23 10:35:49 1997 +0200
+++ b/src/HOL/Arith.ML	Mon Jun 23 10:42:03 1997 +0200
@@ -12,11 +12,11 @@
 (*** Basic rewrite rules for the arithmetic operators ***)
 
 goalw Arith.thy [pred_def] "pred 0 = 0";
-by(Simp_tac 1);
+by (Simp_tac 1);
 qed "pred_0";
 
 goalw Arith.thy [pred_def] "pred(Suc n) = n";
-by(Simp_tac 1);
+by (Simp_tac 1);
 qed "pred_Suc";
 
 Addsimps [pred_0,pred_Suc];
@@ -175,8 +175,8 @@
 qed "add_lessD1";
 
 goal Arith.thy "!!i::nat. ~ (i+j < i)";
-br notI 1;
-be (add_lessD1 RS less_irrefl) 1;
+by (rtac notI 1);
+by (etac (add_lessD1 RS less_irrefl) 1);
 qed "not_add_less1";
 
 goal Arith.thy "!!i::nat. ~ (j+i < i)";
@@ -506,7 +506,7 @@
 qed "mult_less_mono2";
 
 goal Arith.thy "!!i::nat. [| i<j; 0<k |] ==> i*k < j*k";
-bd mult_less_mono2 1;
+by (dtac mult_less_mono2 1);
 by (ALLGOALS (asm_full_simp_tac (!simpset addsimps [mult_commute])));
 qed "mult_less_mono1";
 
@@ -531,21 +531,21 @@
 qed "mult_less_cancel2";
 
 goal Arith.thy "!!k. 0<k ==> (k*m < k*n) = (m<n)";
-bd mult_less_cancel2 1;
+by (dtac mult_less_cancel2 1);
 by (asm_full_simp_tac (!simpset addsimps [mult_commute]) 1);
 qed "mult_less_cancel1";
 Addsimps [mult_less_cancel1, mult_less_cancel2];
 
 goal Arith.thy "!!k. 0<k ==> (m*k = n*k) = (m=n)";
 by (cut_facts_tac [less_linear] 1);
-by(Step_tac 1);
-ba 2;
+by (Step_tac 1);
+by (assume_tac 2);
 by (ALLGOALS (dtac mult_less_mono1 THEN' assume_tac));
 by (ALLGOALS Asm_full_simp_tac);
 qed "mult_cancel2";
 
 goal Arith.thy "!!k. 0<k ==> (k*m = k*n) = (m=n)";
-bd mult_cancel2 1;
+by (dtac mult_cancel2 1);
 by (asm_full_simp_tac (!simpset addsimps [mult_commute]) 1);
 qed "mult_cancel1";
 Addsimps [mult_cancel1, mult_cancel2];
@@ -574,13 +574,13 @@
 qed "diff_less_mono";
 
 goal Arith.thy "!! a b c::nat. a+b < c ==> a < c-b";
-bd diff_less_mono 1;
-br le_add2 1;
+by (dtac diff_less_mono 1);
+by (rtac le_add2 1);
 by (Asm_full_simp_tac 1);
 qed "add_less_imp_less_diff";
 
 goal Arith.thy "!! n. n <= m ==> Suc m - n = Suc (m - n)";
-br Suc_diff_n 1;
+by (rtac Suc_diff_n 1);
 by (asm_full_simp_tac (!simpset addsimps [le_eq_less_Suc]) 1);
 qed "Suc_diff_le";
 
@@ -597,7 +597,7 @@
 Addsimps [diff_diff_cancel];
 
 goal Arith.thy "!!k::nat. k <= n ==> m <= n + m - k";
-be rev_mp 1;
+by (etac rev_mp 1);
 by (res_inst_tac [("m", "k"), ("n", "n")] diff_induct 1);
 by (Simp_tac 1);
 by (simp_tac (!simpset addsimps [less_add_Suc2, less_imp_le]) 1);
diff -r fdb1768ebd3e -r a8ab7c64817c src/HOL/Divides.ML
--- a/src/HOL/Divides.ML	Mon Jun 23 10:35:49 1997 +0200
+++ b/src/HOL/Divides.ML	Mon Jun 23 10:42:03 1997 +0200
@@ -189,7 +189,7 @@
 
 goal thy "!!n. 0<n ==> m*n div n = m";
 by (cut_inst_tac [("m", "m*n")] mod_div_equality 1);
-ba 1;
+by (assume_tac 1);
 by (asm_full_simp_tac (!simpset addsimps [mod_mult_self_is_0]) 1);
 qed "div_mult_self_is_m";
 Addsimps [div_mult_self_is_m];
@@ -264,7 +264,7 @@
 qed "dvd_diff";
 
 goal thy "!!k. [| k dvd (m-n); k dvd n; n<=m |] ==> k dvd m";
-be (not_less_iff_le RS iffD2 RS add_diff_inverse RS subst) 1;
+by (etac (not_less_iff_le RS iffD2 RS add_diff_inverse RS subst) 1);
 by (blast_tac (!claset addIs [dvd_add]) 1);
 qed "dvd_diffD";
 
@@ -316,9 +316,9 @@
 goalw thy [dvd_def] "!!n. [| k dvd n; 0 < n |] ==> k <= n";
 by (Step_tac 1);
 by (ALLGOALS (full_simp_tac (!simpset addsimps [zero_less_mult_iff])));
-be conjE 1;
-br le_trans 1;
-br (le_refl RS mult_le_mono) 2;
+by (etac conjE 1);
+by (rtac le_trans 1);
+by (rtac (le_refl RS mult_le_mono) 2);
 by (etac Suc_leI 2);
 by (Simp_tac 1);
 qed "dvd_imp_le";
diff -r fdb1768ebd3e -r a8ab7c64817c src/HOL/Finite.ML
--- a/src/HOL/Finite.ML	Mon Jun 23 10:35:49 1997 +0200
+++ b/src/HOL/Finite.ML	Mon Jun 23 10:42:03 1997 +0200
@@ -41,7 +41,7 @@
 \       !!F a. [| finite F; a:A; a ~: F;  P(F) |] ==> P(insert a F) \
 \    |] ==> F <= A --> P(F)";
 by (rtac (major RS finite_induct) 1);
-by(ALLGOALS (blast_tac (!claset addIs prems)));
+by (ALLGOALS (blast_tac (!claset addIs prems)));
 val lemma = result();
 
 val prems = goal Finite.thy 
@@ -49,7 +49,7 @@
 \       P({}); \
 \       !!F a. [| finite F; a:A; a ~: F;  P(F) |] ==> P(insert a F) \
 \    |] ==> P(F)";
-by(blast_tac (HOL_cs addIs ((lemma RS mp)::prems)) 1);
+by (blast_tac (HOL_cs addIs ((lemma RS mp)::prems)) 1);
 qed "finite_subset_induct";
 
 Addsimps Finites.intrs;
@@ -122,7 +122,7 @@
 
 goal Finite.thy "finite(A-{a}) = finite(A)";
 by (case_tac "a:A" 1);
-br (finite_insert RS sym RS trans) 1;
+by (rtac (finite_insert RS sym RS trans) 1);
 by (stac insert_Diff 1);
 by (ALLGOALS Asm_simp_tac);
 qed "finite_Diff_singleton";
@@ -134,21 +134,21 @@
 by (Step_tac 1);
 by (subgoal_tac "EX y:A. f y = x & F = f``(A-{y})" 1);
  by (Step_tac 1);
- bw inj_onto_def;
+ by (rewtac inj_onto_def);
  by (Blast_tac 1);
 by (thin_tac "ALL A. ?PP(A)" 1);
 by (forward_tac [[equalityD2, insertI1] MRS subsetD] 1);
 by (Step_tac 1);
 by (res_inst_tac [("x","xa")] bexI 1);
 by (ALLGOALS Asm_simp_tac);
-be equalityE 1;
-br equalityI 1;
+by (etac equalityE 1);
+by (rtac equalityI 1);
 by (Blast_tac 2);
 by (Best_tac 1);
 val lemma = result();
 
 goal Finite.thy "!!A. [| finite(f``A);  inj_onto f A |] ==> finite A";
-bd lemma 1;
+by (dtac lemma 1);
 by (Blast_tac 1);
 qed "finite_imageD";
 
@@ -157,15 +157,15 @@
 
 goal Finite.thy "!!A. finite(Pow A) ==> finite A";
 by (subgoal_tac "finite ((%x.{x})``A)" 1);
-br finite_subset 2;
-ba 3;
+by (rtac finite_subset 2);
+by (assume_tac 3);
 by (ALLGOALS
     (fast_tac (!claset addSDs [rewrite_rule [inj_onto_def] finite_imageD])));
 val lemma = result();
 
 goal Finite.thy "finite(Pow A) = finite A";
-br iffI 1;
-be lemma 1;
+by (rtac iffI 1);
+by (etac lemma 1);
 (*Opposite inclusion: finite A ==> finite (Pow A) *)
 by (etac finite_induct 1);
 by (ALLGOALS 
@@ -175,19 +175,19 @@
 AddIffs [finite_Pow_iff];
 
 goal Finite.thy "finite(r^-1) = finite r";
-by(subgoal_tac "r^-1 = (%(x,y).(y,x))``r" 1);
- by(Asm_simp_tac 1);
- br iffI 1;
-  be (rewrite_rule [inj_onto_def] finite_imageD) 1;
-  by(simp_tac (!simpset setloop (split_tac[expand_split])) 1);
- be finite_imageI 1;
-by(simp_tac (!simpset addsimps [inverse_def,image_def]) 1);
-by(Auto_tac());
- br bexI 1;
- ba 2;
- by(Simp_tac 1);
-by(split_all_tac 1);
-by(Asm_full_simp_tac 1);
+by (subgoal_tac "r^-1 = (%(x,y).(y,x))``r" 1);
+ by (Asm_simp_tac 1);
+ by (rtac iffI 1);
+  by (etac (rewrite_rule [inj_onto_def] finite_imageD) 1);
+  by (simp_tac (!simpset setloop (split_tac[expand_split])) 1);
+ by (etac finite_imageI 1);
+by (simp_tac (!simpset addsimps [inverse_def,image_def]) 1);
+by (Auto_tac());
+ by (rtac bexI 1);
+ by (assume_tac 2);
+ by (Simp_tac 1);
+by (split_all_tac 1);
+by (Asm_full_simp_tac 1);
 qed "finite_inverse";
 AddIffs [finite_inverse];
 
@@ -249,7 +249,7 @@
    by (Asm_simp_tac 1);
   by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
   by (Blast_tac 1);
- bd sym 1;
+ by (dtac sym 1);
  by (rotate_tac ~1 1);
  by (Asm_full_simp_tac 1);
  by (res_inst_tac [("x","%i. if f i = f m then a else f i")] exI 1);
@@ -282,21 +282,21 @@
 goal Finite.thy "!!A. [| finite A; x ~: A |] ==> \
 \ (LEAST n. ? f. insert x A = {f i|i.i<n}) = Suc(LEAST n. ? f. A={f i|i.i<n})";
 by (rtac Least_equality 1);
- bd finite_has_card 1;
- be exE 1;
+ by (dtac finite_has_card 1);
+ by (etac exE 1);
  by (dres_inst_tac [("P","%n.? f. A={f i|i.i<n}")] LeastI 1);
- be exE 1;
+ by (etac exE 1);
  by (res_inst_tac
    [("x","%i. if i<(LEAST n. ? f. A={f i |i. i < n}) then f i else x")] exI 1);
  by (simp_tac
     (!simpset addsimps [Collect_conv_insert, less_Suc_eq] 
               addcongs [rev_conj_cong]) 1);
- be subst 1;
- br refl 1;
+ by (etac subst 1);
+ by (rtac refl 1);
 by (rtac notI 1);
 by (etac exE 1);
 by (dtac lemma 1);
- ba 1;
+ by (assume_tac 1);
 by (etac exE 1);
 by (etac conjE 1);
 by (dres_inst_tac [("P","%x. ? g. A = {g i |i. i < x}")] Least_le 1);
@@ -339,9 +339,9 @@
 goal Finite.thy "!!A. [| finite A; B<=A |] ==> card A - card B = card (A - B)";
 by (subgoal_tac "(A-B) Un B = A" 1);
 by (Blast_tac 2);
-br (add_right_cancel RS iffD1) 1;
-br (card_Un_disjoint RS subst) 1;
-be ssubst 4;
+by (rtac (add_right_cancel RS iffD1) 1);
+by (rtac (card_Un_disjoint RS subst) 1);
+by (etac ssubst 4);
 by (Blast_tac 3);
 by (ALLGOALS 
     (asm_simp_tac
@@ -382,7 +382,7 @@
 by (etac finite_induct 1);
 by (ALLGOALS Asm_simp_tac);
 by (Step_tac 1);
-bw inj_onto_def;
+by (rewtac inj_onto_def);
 by (Blast_tac 1);
 by (stac card_insert_disjoint 1);
 by (etac finite_imageI 1);
@@ -397,7 +397,7 @@
 by (EVERY (map (blast_tac (!claset addIs [finite_imageI])) [3,2,1]));
 by (subgoal_tac "inj_onto (insert x) (Pow F)" 1);
 by (asm_simp_tac (!simpset addsimps [card_image, Pow_insert]) 1);
-bw inj_onto_def;
+by (rewtac inj_onto_def);
 by (blast_tac (!claset addSEs [equalityE]) 1);
 qed "card_Pow";
 Addsimps [card_Pow];
diff -r fdb1768ebd3e -r a8ab7c64817c src/HOL/IMP/Denotation.ML
--- a/src/HOL/IMP/Denotation.ML	Mon Jun 23 10:35:49 1997 +0200
+++ b/src/HOL/IMP/Denotation.ML	Mon Jun 23 10:42:03 1997 +0200
@@ -29,7 +29,7 @@
 
 (* start with rule induction *)
 by (etac evalc.induct 1);
-auto();
+by (Auto_tac());
 (* while *)
 by (rewtac Gamma_def);
 by (stac (rewrite_rule [Gamma_def] (Gamma_mono RS lfp_Tarski)) 1);
diff -r fdb1768ebd3e -r a8ab7c64817c src/HOL/Induct/Com.ML
--- a/src/HOL/Induct/Com.ML	Mon Jun 23 10:35:49 1997 +0200
+++ b/src/HOL/Induct/Com.ML	Mon Jun 23 10:42:03 1997 +0200
@@ -52,7 +52,7 @@
 qed "assign_different";
 
 goalw thy [assign_def] "s[s x/x] = s";
-br ext 1;
+by (rtac ext 1);
 by (simp_tac (!simpset setloop split_tac[expand_if]) 1);
 qed "assign_triv";
 
diff -r fdb1768ebd3e -r a8ab7c64817c src/HOL/Integ/Equiv.ML
--- a/src/HOL/Integ/Equiv.ML	Mon Jun 23 10:35:49 1997 +0200
+++ b/src/HOL/Integ/Equiv.ML	Mon Jun 23 10:42:03 1997 +0200
@@ -263,14 +263,14 @@
 goal thy "!!A. [| finite A; r <= A Times A |] ==> finite (A/r)";
 by (rtac finite_subset 1);
 by (etac (finite_Pow_iff RS iffD2) 2);
-by (rewrite_goals_tac [quotient_def]);
+by (rewtac quotient_def);
 by (Blast_tac 1);
 qed "finite_quotient";
 
 goalw thy [quotient_def]
     "!!A. [| finite A;  r <= A Times A;  X : A/r |] ==> finite X";
 by (rtac finite_subset 1);
-ba 2;
+by (assume_tac 2);
 by (Blast_tac 1);
 qed "finite_equiv_class";
 
diff -r fdb1768ebd3e -r a8ab7c64817c src/HOL/List.ML
--- a/src/HOL/List.ML	Mon Jun 23 10:35:49 1997 +0200
+++ b/src/HOL/List.ML	Mon Jun 23 10:42:03 1997 +0200
@@ -38,8 +38,8 @@
 qed "expand_list_case";
 
 val prems = goal thy "[| P([]); !!x xs. P(x#xs) |] ==> P(xs)";
-by(induct_tac "xs" 1);
-by(REPEAT(resolve_tac prems 1));
+by (induct_tac "xs" 1);
+by (REPEAT(resolve_tac prems 1));
 qed "list_cases";
 
 goal thy  "(xs=[] --> P([])) & (!y ys. xs=y#ys --> P(y#ys)) --> P(xs)";
@@ -73,7 +73,7 @@
 goal thy "([] = xs@ys) = (xs=[] & ys=[])";
 by (induct_tac "xs" 1);
 by (ALLGOALS Asm_simp_tac);
-by(Blast_tac 1);
+by (Blast_tac 1);
 qed "Nil_is_append_conv";
 AddIffs [Nil_is_append_conv];
 
@@ -84,19 +84,19 @@
 AddIffs [same_append_eq];
 
 goal thy "!ys. (xs @ [x] = ys @ [y]) = (xs = ys & x = y)"; 
-by(induct_tac "xs" 1);
- br allI 1;
- by(induct_tac "ys" 1);
-  by(ALLGOALS Asm_simp_tac);
-br allI 1;
-by(induct_tac "ys" 1);
- by(ALLGOALS Asm_simp_tac);
+by (induct_tac "xs" 1);
+ by (rtac allI 1);
+ by (induct_tac "ys" 1);
+  by (ALLGOALS Asm_simp_tac);
+by (rtac allI 1);
+by (induct_tac "ys" 1);
+ by (ALLGOALS Asm_simp_tac);
 qed_spec_mp "append1_eq_conv";
 AddIffs [append1_eq_conv];
 
 goal thy "xs ~= [] --> hd xs # tl xs = xs";
-by(induct_tac "xs" 1);
-by(ALLGOALS Asm_simp_tac);
+by (induct_tac "xs" 1);
+by (ALLGOALS Asm_simp_tac);
 qed_spec_mp "hd_Cons_tl";
 Addsimps [hd_Cons_tl];
 
@@ -106,15 +106,15 @@
 qed "hd_append";
 
 goal thy "tl(xs@ys) = (case xs of [] => tl(ys) | z#zs => zs@ys)";
-by(simp_tac (!simpset setloop(split_tac[expand_list_case])) 1);
+by (simp_tac (!simpset setloop(split_tac[expand_list_case])) 1);
 qed "tl_append";
 
 (** map **)
 
 goal thy
   "(!x. x : set_of_list xs --> f x = g x) --> map f xs = map g xs";
-by(induct_tac "xs" 1);
-by(ALLGOALS Asm_simp_tac);
+by (induct_tac "xs" 1);
+by (ALLGOALS Asm_simp_tac);
 bind_thm("map_ext", impI RS (allI RS (result() RS mp)));
 
 goal thy "map (%x.x) = (%xs.xs)";
@@ -190,20 +190,20 @@
 qed "set_of_list_subset_Cons";
 
 goal thy "(set_of_list xs = {}) = (xs = [])";
-by(induct_tac "xs" 1);
-by(ALLGOALS Asm_simp_tac);
+by (induct_tac "xs" 1);
+by (ALLGOALS Asm_simp_tac);
 qed "set_of_list_empty";
 Addsimps [set_of_list_empty];
 
 goal thy "set_of_list(rev xs) = set_of_list(xs)";
-by(induct_tac "xs" 1);
-by(ALLGOALS Asm_simp_tac);
+by (induct_tac "xs" 1);
+by (ALLGOALS Asm_simp_tac);
 qed "set_of_list_rev";
 Addsimps [set_of_list_rev];
 
 goal thy "set_of_list(map f xs) = f``(set_of_list xs)";
-by(induct_tac "xs" 1);
-by(ALLGOALS Asm_simp_tac);
+by (induct_tac "xs" 1);
+by (ALLGOALS Asm_simp_tac);
 qed "set_of_list_map";
 Addsimps [set_of_list_map];
 
@@ -232,14 +232,14 @@
 (** filter **)
 
 goal thy "filter P (xs@ys) = filter P xs @ filter P ys";
-by(induct_tac "xs" 1);
- by(ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
+by (induct_tac "xs" 1);
+ by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
 qed "filter_append";
 Addsimps [filter_append];
 
 goal thy "size (filter P xs) <= size xs";
-by(induct_tac "xs" 1);
- by(ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
+by (induct_tac "xs" 1);
+ by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
 qed "filter_size";
 
 
@@ -277,14 +277,14 @@
 Addsimps [length_rev];
 
 goal thy "(length xs = 0) = (xs = [])";
-by(induct_tac "xs" 1);
-by(ALLGOALS Asm_simp_tac);
+by (induct_tac "xs" 1);
+by (ALLGOALS Asm_simp_tac);
 qed "length_0_conv";
 AddIffs [length_0_conv];
 
 goal thy "(0 < length xs) = (xs ~= [])";
-by(induct_tac "xs" 1);
-by(ALLGOALS Asm_simp_tac);
+by (induct_tac "xs" 1);
+by (ALLGOALS Asm_simp_tac);
 qed "length_greater_0_conv";
 AddIffs [length_greater_0_conv];
 
@@ -294,14 +294,14 @@
 goal thy
   "!xs. nth n (xs@ys) = \
 \          (if n < length xs then nth n xs else nth (n - length xs) ys)";
-by(nat_ind_tac "n" 1);
- by(Asm_simp_tac 1);
- br allI 1;
- by(exhaust_tac "xs" 1);
-  by(ALLGOALS Asm_simp_tac);
-br allI 1;
-by(exhaust_tac "xs" 1);
- by(ALLGOALS Asm_simp_tac);
+by (nat_ind_tac "n" 1);
+ by (Asm_simp_tac 1);
+ by (rtac allI 1);
+ by (exhaust_tac "xs" 1);
+  by (ALLGOALS Asm_simp_tac);
+by (rtac allI 1);
+by (exhaust_tac "xs" 1);
+ by (ALLGOALS Asm_simp_tac);
 qed_spec_mp "nth_append";
 
 goal thy "!n. n < length xs --> nth n (map f xs) = f (nth n xs)";
@@ -365,118 +365,118 @@
 Addsimps [take_0,take_Suc_Cons,drop_0,drop_Suc_Cons];
 
 goal thy "!xs. length(take n xs) = min (length xs) n";
-by(nat_ind_tac "n" 1);
- by(ALLGOALS Asm_simp_tac);
-br allI 1;
-by(exhaust_tac "xs" 1);
- by(ALLGOALS Asm_simp_tac);
+by (nat_ind_tac "n" 1);
+ by (ALLGOALS Asm_simp_tac);
+by (rtac allI 1);
+by (exhaust_tac "xs" 1);
+ by (ALLGOALS Asm_simp_tac);
 qed_spec_mp "length_take";
 Addsimps [length_take];
 
 goal thy "!xs. length(drop n xs) = (length xs - n)";
-by(nat_ind_tac "n" 1);
- by(ALLGOALS Asm_simp_tac);
-br allI 1;
-by(exhaust_tac "xs" 1);
- by(ALLGOALS Asm_simp_tac);
+by (nat_ind_tac "n" 1);
+ by (ALLGOALS Asm_simp_tac);
+by (rtac allI 1);
+by (exhaust_tac "xs" 1);
+ by (ALLGOALS Asm_simp_tac);
 qed_spec_mp "length_drop";
 Addsimps [length_drop];
 
 goal thy "!xs. length xs <= n --> take n xs = xs";
-by(nat_ind_tac "n" 1);
- by(ALLGOALS Asm_simp_tac);
-br allI 1;
-by(exhaust_tac "xs" 1);
- by(ALLGOALS Asm_simp_tac);
+by (nat_ind_tac "n" 1);
+ by (ALLGOALS Asm_simp_tac);
+by (rtac allI 1);
+by (exhaust_tac "xs" 1);
+ by (ALLGOALS Asm_simp_tac);
 qed_spec_mp "take_all";
 
 goal thy "!xs. length xs <= n --> drop n xs = []";
-by(nat_ind_tac "n" 1);
- by(ALLGOALS Asm_simp_tac);
-br allI 1;
-by(exhaust_tac "xs" 1);
- by(ALLGOALS Asm_simp_tac);
+by (nat_ind_tac "n" 1);
+ by (ALLGOALS Asm_simp_tac);
+by (rtac allI 1);
+by (exhaust_tac "xs" 1);
+ by (ALLGOALS Asm_simp_tac);
 qed_spec_mp "drop_all";
 
 goal thy 
   "!xs. take n (xs @ ys) = (take n xs @ take (n - length xs) ys)";
-by(nat_ind_tac "n" 1);
- by(ALLGOALS Asm_simp_tac);
-br allI 1;
-by(exhaust_tac "xs" 1);
- by(ALLGOALS Asm_simp_tac);
+by (nat_ind_tac "n" 1);
+ by (ALLGOALS Asm_simp_tac);
+by (rtac allI 1);
+by (exhaust_tac "xs" 1);
+ by (ALLGOALS Asm_simp_tac);
 qed_spec_mp "take_append";
 Addsimps [take_append];
 
 goal thy "!xs. drop n (xs@ys) = drop n xs @ drop (n - length xs) ys"; 
-by(nat_ind_tac "n" 1);
- by(ALLGOALS Asm_simp_tac);
-br allI 1;
-by(exhaust_tac "xs" 1);
- by(ALLGOALS Asm_simp_tac);
+by (nat_ind_tac "n" 1);
+ by (ALLGOALS Asm_simp_tac);
+by (rtac allI 1);
+by (exhaust_tac "xs" 1);
+ by (ALLGOALS Asm_simp_tac);
 qed_spec_mp "drop_append";
 Addsimps [drop_append];
 
 goal thy "!xs n. take n (take m xs) = take (min n m) xs"; 
-by(nat_ind_tac "m" 1);
- by(ALLGOALS Asm_simp_tac);
-br allI 1;
-by(exhaust_tac "xs" 1);
- by(ALLGOALS Asm_simp_tac);
-br allI 1;
-by(exhaust_tac "n" 1);
- by(ALLGOALS Asm_simp_tac);
+by (nat_ind_tac "m" 1);
+ by (ALLGOALS Asm_simp_tac);
+by (rtac allI 1);
+by (exhaust_tac "xs" 1);
+ by (ALLGOALS Asm_simp_tac);
+by (rtac allI 1);
+by (exhaust_tac "n" 1);
+ by (ALLGOALS Asm_simp_tac);
 qed_spec_mp "take_take";
 
 goal thy "!xs. drop n (drop m xs) = drop (n + m) xs"; 
-by(nat_ind_tac "m" 1);
- by(ALLGOALS Asm_simp_tac);
-br allI 1;
-by(exhaust_tac "xs" 1);
- by(ALLGOALS Asm_simp_tac);
+by (nat_ind_tac "m" 1);
+ by (ALLGOALS Asm_simp_tac);
+by (rtac allI 1);
+by (exhaust_tac "xs" 1);
+ by (ALLGOALS Asm_simp_tac);
 qed_spec_mp "drop_drop";
 
 goal thy "!xs n. take n (drop m xs) = drop m (take (n + m) xs)"; 
-by(nat_ind_tac "m" 1);
- by(ALLGOALS Asm_simp_tac);
-br allI 1;
-by(exhaust_tac "xs" 1);
- by(ALLGOALS Asm_simp_tac);
+by (nat_ind_tac "m" 1);
+ by (ALLGOALS Asm_simp_tac);
+by (rtac allI 1);
+by (exhaust_tac "xs" 1);
+ by (ALLGOALS Asm_simp_tac);
 qed_spec_mp "take_drop";
 
 goal thy "!xs. take n (map f xs) = map f (take n xs)"; 
-by(nat_ind_tac "n" 1);
-by(ALLGOALS Asm_simp_tac);
-br allI 1;
-by(exhaust_tac "xs" 1);
-by(ALLGOALS Asm_simp_tac);
+by (nat_ind_tac "n" 1);
+by (ALLGOALS Asm_simp_tac);
+by (rtac allI 1);
+by (exhaust_tac "xs" 1);
+by (ALLGOALS Asm_simp_tac);
 qed_spec_mp "take_map"; 
 
 goal thy "!xs. drop n (map f xs) = map f (drop n xs)"; 
-by(nat_ind_tac "n" 1);
-by(ALLGOALS Asm_simp_tac);
-br allI 1;
-by(exhaust_tac "xs" 1);
-by(ALLGOALS Asm_simp_tac);
+by (nat_ind_tac "n" 1);
+by (ALLGOALS Asm_simp_tac);
+by (rtac allI 1);
+by (exhaust_tac "xs" 1);
+by (ALLGOALS Asm_simp_tac);
 qed_spec_mp "drop_map";
 
 goal thy "!n i. i < n --> nth i (take n xs) = nth i xs";
-by(induct_tac "xs" 1);
- by(ALLGOALS Asm_simp_tac);
-by(strip_tac 1);
-by(exhaust_tac "n" 1);
- by(Blast_tac 1);
-by(exhaust_tac "i" 1);
-by(ALLGOALS Asm_full_simp_tac);
+by (induct_tac "xs" 1);
+ by (ALLGOALS Asm_simp_tac);
+by (strip_tac 1);
+by (exhaust_tac "n" 1);
+ by (Blast_tac 1);
+by (exhaust_tac "i" 1);
+by (ALLGOALS Asm_full_simp_tac);
 qed_spec_mp "nth_take";
 Addsimps [nth_take];
 
 goal thy  "!xs i. n + i < length xs --> nth i (drop n xs) = nth (n + i) xs";
-by(nat_ind_tac "n" 1);
- by(ALLGOALS Asm_simp_tac);
-br allI 1;
-by(exhaust_tac "xs" 1);
- by(ALLGOALS Asm_simp_tac);
+by (nat_ind_tac "n" 1);
+ by (ALLGOALS Asm_simp_tac);
+by (rtac allI 1);
+by (exhaust_tac "xs" 1);
+ by (ALLGOALS Asm_simp_tac);
 qed_spec_mp "nth_drop";
 Addsimps [nth_drop];
 
@@ -484,41 +484,41 @@
 
 goal thy
   "x:set_of_list xs & ~P(x) --> takeWhile P (xs @ ys) = takeWhile P xs";
-by(induct_tac "xs" 1);
- by(Simp_tac 1);
-by(asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1);
-by(Blast_tac 1);
+by (induct_tac "xs" 1);
+ by (Simp_tac 1);
+by (asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1);
+by (Blast_tac 1);
 bind_thm("takeWhile_append1", conjI RS (result() RS mp));
 Addsimps [takeWhile_append1];
 
 goal thy
   "(!x:set_of_list xs.P(x)) --> takeWhile P (xs @ ys) = xs @ takeWhile P ys";
-by(induct_tac "xs" 1);
- by(Simp_tac 1);
-by(asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1);
+by (induct_tac "xs" 1);
+ by (Simp_tac 1);
+by (asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1);
 bind_thm("takeWhile_append2", ballI RS (result() RS mp));
 Addsimps [takeWhile_append2];
 
 goal thy
   "x:set_of_list xs & ~P(x) --> dropWhile P (xs @ ys) = (dropWhile P xs)@ys";
-by(induct_tac "xs" 1);
- by(Simp_tac 1);
-by(asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1);
-by(Blast_tac 1);
+by (induct_tac "xs" 1);
+ by (Simp_tac 1);
+by (asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1);
+by (Blast_tac 1);
 bind_thm("dropWhile_append1", conjI RS (result() RS mp));
 Addsimps [dropWhile_append1];
 
 goal thy
   "(!x:set_of_list xs.P(x)) --> dropWhile P (xs @ ys) = dropWhile P ys";
-by(induct_tac "xs" 1);
- by(Simp_tac 1);
-by(asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1);
+by (induct_tac "xs" 1);
+ by (Simp_tac 1);
+by (asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1);
 bind_thm("dropWhile_append2", ballI RS (result() RS mp));
 Addsimps [dropWhile_append2];
 
 goal thy "x:set_of_list(takeWhile P xs) --> x:set_of_list xs & P x";
-by(induct_tac "xs" 1);
- by(Simp_tac 1);
-by(asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1);
+by (induct_tac "xs" 1);
+ by (Simp_tac 1);
+by (asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1);
 qed_spec_mp"set_of_list_take_whileD";
 
diff -r fdb1768ebd3e -r a8ab7c64817c src/HOL/Modelcheck/MCSyn.ML
--- a/src/HOL/Modelcheck/MCSyn.ML	Mon Jun 23 10:35:49 1997 +0200
+++ b/src/HOL/Modelcheck/MCSyn.ML	Mon Jun 23 10:42:03 1997 +0200
@@ -19,16 +19,16 @@
 
 
 goal Prod.thy "(? x. P x) = (? a b. P(a,b))";
-auto();
+by (Auto_tac());
 by (split_all_tac 1);
-auto();
+by (Auto_tac());
 qed "split_paired_Ex";
 
 
 goalw thy [split_def] "(f::'a*'b=>'c) = (%(x, y). f (x, y))";
-  br ext 1;
+  by (rtac ext 1);
   by (stac (surjective_pairing RS sym) 1);
-  br refl 1;
+  by (rtac refl 1);
 qed "pair_eta_expand";
 
 local
diff -r fdb1768ebd3e -r a8ab7c64817c src/HOL/NatDef.ML
--- a/src/HOL/NatDef.ML	Mon Jun 23 10:35:49 1997 +0200
+++ b/src/HOL/NatDef.ML	Mon Jun 23 10:42:03 1997 +0200
@@ -135,7 +135,7 @@
 bind_thm ("Suc_n_not_n", n_not_Suc_n RS not_sym);
 
 goal thy "!!n. n ~= 0 ==> EX m. n = Suc m";
-br natE 1;
+by (rtac natE 1);
 by (REPEAT (Blast_tac 1));
 qed "not0_implies_Suc";
 
@@ -567,15 +567,15 @@
 (** LEAST -- the least number operator **)
 
 goal thy "(! m::nat. P m --> n <= m) = (! m. m < n --> ~ P m)";
-by(blast_tac (!claset addIs [leI] addEs [leE]) 1);
+by (blast_tac (!claset addIs [leI] addEs [leE]) 1);
 val lemma = result();
 
 (* This is an old def of Least for nat, which is derived for compatibility *)
 goalw thy [Least_def]
   "(LEAST n::nat. P n) == (@n. P(n) & (ALL m. m < n --> ~P(m)))";
-by(simp_tac (!simpset addsimps [lemma]) 1);
-br eq_reflection 1;
-br refl 1;
+by (simp_tac (!simpset addsimps [lemma]) 1);
+by (rtac eq_reflection 1);
+by (rtac refl 1);
 qed "Least_nat_def";
 
 val [prem1,prem2] = goalw thy [Least_nat_def]
diff -r fdb1768ebd3e -r a8ab7c64817c src/HOL/Power.ML
--- a/src/HOL/Power.ML	Mon Jun 23 10:35:49 1997 +0200
+++ b/src/HOL/Power.ML	Mon Jun 23 10:42:03 1997 +0200
@@ -28,15 +28,15 @@
 qed "zero_less_power";
 
 goalw thy [dvd_def] "!!m::nat. m<=n ==> i^m dvd i^n";
-be (not_less_iff_le RS iffD2 RS add_diff_inverse RS subst) 1;
+by (etac (not_less_iff_le RS iffD2 RS add_diff_inverse RS subst) 1);
 by (asm_simp_tac (!simpset addsimps [power_add]) 1);
 by (Blast_tac 1);
 qed "le_imp_power_dvd";
 
 goal thy "!! i r. [| 0 < i; i^m < i^n |] ==> m<n";
-br ccontr 1;
-bd (leI RS le_imp_power_dvd RS dvd_imp_le RS leD) 1;
-be zero_less_power 1;
+by (rtac ccontr 1);
+by (dtac (leI RS le_imp_power_dvd RS dvd_imp_le RS leD) 1);
+by (etac zero_less_power 1);
 by (contr_tac 1);
 qed "power_less_imp_less";
 
diff -r fdb1768ebd3e -r a8ab7c64817c src/HOL/Quot/HQUOT.ML
--- a/src/HOL/Quot/HQUOT.ML	Mon Jun 23 10:35:49 1997 +0200
+++ b/src/HOL/Quot/HQUOT.ML	Mon Jun 23 10:42:03 1997 +0200
@@ -14,7 +14,7 @@
 
 val prems = goal thy "Rep_quot a = Rep_quot b ==> a=b";
 by (cut_facts_tac prems 1);
-br (Rep_quot_inverse RS subst) 1;
+by (rtac (Rep_quot_inverse RS subst) 1);
 by (res_inst_tac [("t","a")] (Rep_quot_inverse RS subst) 1);
 by (Asm_simp_tac 1);
 qed "quot_eq";
@@ -22,8 +22,8 @@
 (* prepare induction and exhaustiveness *)
 val prems = goal thy "!s.s:quot --> P (Abs_quot s) ==> P x";
 by (cut_facts_tac prems 1);
-br (Abs_quot_inverse RS subst) 1;
-br Rep_quot 1;
+by (rtac (Abs_quot_inverse RS subst) 1);
+by (rtac Rep_quot 1);
 by (dres_inst_tac [("x","Rep_quot x")] spec 1);
 by (asm_full_simp_tac (HOL_ss addsimps [Rep_quot,Rep_quot_inverse]) 1);
 qed "all_q";
@@ -39,90 +39,90 @@
 val prems = goalw thy [peclass_def] "x===y==><[x]>=<[y]>";
 by (cut_facts_tac prems 1);
 by (res_inst_tac [("f","Abs_quot")] arg_cong 1);
-br Collect_cong 1;
-br iffI 1;
-be per_trans 1;ba 1;
-be per_trans 1;
-be per_sym 1;
+by (rtac Collect_cong 1);
+by (rtac iffI 1);
+by (etac per_trans 1);by (assume_tac 1);
+by (etac per_trans 1);
+by (etac per_sym 1);
 qed "per_class_eqI";
 
 val prems = goalw thy [peclass_def] "<[(x::'a::er)]>=<[y]>==>x===y";
 by (cut_facts_tac prems 1);
 by (dres_inst_tac [("f","Rep_quot")] arg_cong 1);
 by (asm_full_simp_tac(HOL_ss addsimps [Abs_quot_inverse,per_class_rep_quot])1);
-by (dres_inst_tac [("c","x")] equalityCE 1);ba 3;
+by (dres_inst_tac [("c","x")] equalityCE 1);by (assume_tac 3);
 by (safe_tac set_cs);
 by (fast_tac (set_cs addIs [er_refl]) 1);
 qed "er_class_eqE";
 
 val prems = goalw thy [peclass_def] "[|x:D;<[x]>=<[y]>|]==>x===y";
 by (cut_facts_tac prems 1);
-bd DomainD 1;
+by (dtac DomainD 1);
 by (dres_inst_tac [("f","Rep_quot")] arg_cong 1);
 by (asm_full_simp_tac(HOL_ss addsimps [Abs_quot_inverse,per_class_rep_quot])1);
-by (dres_inst_tac [("c","x")] equalityCE 1);ba 3;
+by (dres_inst_tac [("c","x")] equalityCE 1);by (assume_tac 3);
 by (safe_tac set_cs);
 qed "per_class_eqE";
 
 goal thy "<[(x::'a::er)]>=<[y]>=x===y";
-br iffI 1;
-be er_class_eqE 1;
-be per_class_eqI 1;
+by (rtac iffI 1);
+by (etac er_class_eqE 1);
+by (etac per_class_eqI 1);
 qed "er_class_eq";
 
 val prems = goal thy "x:D==><[x]>=<[y]>=x===y";
 by (cut_facts_tac prems 1);
-br iffI 1;
-be per_class_eqE 1;ba 1;
-be per_class_eqI 1;
+by (rtac iffI 1);
+by (etac per_class_eqE 1);by (assume_tac 1);
+by (etac per_class_eqI 1);
 qed "per_class_eq";
 
 (* inequality *)
 val prems = goal thy "[|x:D;~x===y|]==><[x]>~=<[y]>";
 by (cut_facts_tac prems 1);
-br notI 1;
-bd per_class_eqE 1;
-auto();
+by (rtac notI 1);
+by (dtac per_class_eqE 1);
+by (Auto_tac());
 qed "per_class_neqI";
 
 val prems = goal thy "~(x::'a::er)===y==><[x]>~=<[y]>";
 by (cut_facts_tac prems 1);
-br notI 1;
-bd er_class_eqE 1;
-auto();
+by (rtac notI 1);
+by (dtac er_class_eqE 1);
+by (Auto_tac());
 qed "er_class_neqI";
 
 val prems = goal thy "<[x]>~=<[y]>==>~x===y";
 by (cut_facts_tac prems 1);
-br notI 1;
-be notE 1;
-be per_class_eqI 1;
+by (rtac notI 1);
+by (etac notE 1);
+by (etac per_class_eqI 1);
 qed "per_class_neqE";
 
 val prems = goal thy "x:D==><[x]>~=<[y]>=(~x===y)";
 by (cut_facts_tac prems 1);
-br iffI 1;
-be per_class_neqE 1;
-be per_class_neqI 1;ba 1;
+by (rtac iffI 1);
+by (etac per_class_neqE 1);
+by (etac per_class_neqI 1);by (assume_tac 1);
 qed "per_class_not";
 
 goal thy "<[(x::'a::er)]>~=<[y]>=(~x===y)";
-br iffI 1;
-be per_class_neqE 1;
-be er_class_neqI 1;
+by (rtac iffI 1);
+by (etac per_class_neqE 1);
+by (etac er_class_neqI 1);
 qed "er_class_not";
 
 (* exhaustiveness and induction *)
 goalw thy [peclass_def] "? s.x=<[s]>";
-br all_q 1;
+by (rtac all_q 1);
 by (strip_tac 1);
 by (asm_full_simp_tac (HOL_ss addsimps [mem_Collect_eq,quot_def]) 1);
-be exE 1;
+by (etac exE 1);
 by (res_inst_tac [("x","r")] exI 1);
-br quot_eq 1;
+by (rtac quot_eq 1);
 by (subgoal_tac "s:quot" 1);
 by (asm_simp_tac(HOL_ss addsimps [Abs_quot_inverse,per_class_rep_quot])1);
-br set_ext 1;
+by (rtac set_ext 1);
 by (fast_tac set_cs 1);
 by (asm_full_simp_tac (HOL_ss addsimps [mem_Collect_eq,quot_def]) 1);
 by (fast_tac set_cs 1);
diff -r fdb1768ebd3e -r a8ab7c64817c src/HOL/Quot/NPAIR.ML
--- a/src/HOL/Quot/NPAIR.ML	Mon Jun 23 10:35:49 1997 +0200
+++ b/src/HOL/Quot/NPAIR.ML	Mon Jun 23 10:42:03 1997 +0200
@@ -7,13 +7,13 @@
 open NPAIR;
 
 goalw thy [rep_NP_def] "rep_NP(abs_NP np) = np";
-auto();
+by (Auto_tac());
 qed "rep_abs_NP";
 
 Addsimps [rep_abs_NP];
 
 val prems = goalw thy [per_NP_def] "eqv (x::NP) y ==> eqv y x";
 by (cut_facts_tac prems 1);
-auto();
+by (Auto_tac());
 qed "per_sym_NP";
 
diff -r fdb1768ebd3e -r a8ab7c64817c src/HOL/Quot/PER.ML
--- a/src/HOL/Quot/PER.ML	Mon Jun 23 10:35:49 1997 +0200
+++ b/src/HOL/Quot/PER.ML	Mon Jun 23 10:42:03 1997 +0200
@@ -7,13 +7,13 @@
 open PER;
 
 goalw thy [fun_per_def,per_def] "f===g=(!x y.x:D&y:D&x===y-->f x===g y)";
-br refl 1;
+by (rtac refl 1);
 qed "inst_fun_per";
 
 (* Witness that quot is not empty *)
 goal thy "?z:{s.? r.!y.y:s=y===r}";
 fr CollectI;
 by (res_inst_tac [("x","x")] exI 1);
-br allI 1;
-br mem_Collect_eq 1;
+by (rtac allI 1);
+by (rtac mem_Collect_eq 1);
 qed "quotNE";
diff -r fdb1768ebd3e -r a8ab7c64817c src/HOL/Quot/PER0.ML
--- a/src/HOL/Quot/PER0.ML	Mon Jun 23 10:35:49 1997 +0200
+++ b/src/HOL/Quot/PER0.ML	Mon Jun 23 10:42:03 1997 +0200
@@ -9,37 +9,37 @@
 (* derive the characteristic axioms *)
 val prems = goalw thy [per_def] "x === y ==> y === x";
 by (cut_facts_tac prems 1);
-be ax_per_sym 1;
+by (etac ax_per_sym 1);
 qed "per_sym";
 
 val prems = goalw thy [per_def] "[| x === y; y === z |] ==> x === z";
 by (cut_facts_tac prems 1);
-be ax_per_trans 1;
-ba 1;
+by (etac ax_per_trans 1);
+by (assume_tac 1);
 qed "per_trans";
 
 goalw thy [per_def] "(x::'a::er) === x";
-br ax_er_refl 1;
+by (rtac ax_er_refl 1);
 qed "er_refl";
 
 (* now everything works without axclasses *)
 
 goal thy "x===y=y===x";
-br iffI 1;
-be per_sym 1;
-be per_sym 1;
+by (rtac iffI 1);
+by (etac per_sym 1);
+by (etac per_sym 1);
 qed "per_sym2";
 
 val prems = goal  thy "x===y ==> x===x";
 by (cut_facts_tac prems 1);
-br per_trans 1;ba 1;
-be per_sym 1;
+by (rtac per_trans 1);by (assume_tac 1);
+by (etac per_sym 1);
 qed "sym2refl1";
 
 val prems = goal  thy "x===y ==> y===y";
 by (cut_facts_tac prems 1);
-br per_trans 1;ba 2;
-be per_sym 1;
+by (rtac per_trans 1);by (assume_tac 2);
+by (etac per_sym 1);
 qed "sym2refl2";
 
 val prems = goalw thy [Dom] "x:D ==> x === x";
@@ -53,44 +53,44 @@
 qed "DomainI";
 
 goal thy "x:D = x===x";
-br iffI 1;
-be DomainD 1;
-be DomainI 1;
+by (rtac iffI 1);
+by (etac DomainD 1);
+by (etac DomainI 1);
 qed "DomainEq";
 
 goal thy "(~ x === y) = (~ y === x)";
-br (per_sym2 RS arg_cong) 1;
+by (rtac (per_sym2 RS arg_cong) 1);
 qed "per_not_sym";
 
 (* show that PER work only on D *)
 val prems = goal thy "x===y ==> x:D";
 by (cut_facts_tac prems 1);
-be (sym2refl1 RS DomainI) 1;
+by (etac (sym2refl1 RS DomainI) 1);
 qed "DomainI_left"; 
 
 val prems = goal thy "x===y ==> y:D";
 by (cut_facts_tac prems 1);
-be (sym2refl2 RS DomainI) 1;
+by (etac (sym2refl2 RS DomainI) 1);
 qed "DomainI_right"; 
 
 val prems = goalw thy [Dom] "x~:D ==> ~x===y";
 by (cut_facts_tac prems 1);
-by (res_inst_tac [("Q","x===y")] (excluded_middle RS disjE) 1);ba 1;
-bd sym2refl1 1;
+by (res_inst_tac [("Q","x===y")] (excluded_middle RS disjE) 1);by (assume_tac 1);
+by (dtac sym2refl1 1);
 by (fast_tac set_cs 1);
 qed "notDomainE1"; 
 
 val prems = goalw thy [Dom] "x~:D ==> ~y===x";
 by (cut_facts_tac prems 1);
-by (res_inst_tac [("Q","y===x")] (excluded_middle RS disjE) 1);ba 1;
-bd sym2refl2 1;
+by (res_inst_tac [("Q","y===x")] (excluded_middle RS disjE) 1);by (assume_tac 1);
+by (dtac sym2refl2 1);
 by (fast_tac set_cs 1);
 qed "notDomainE2"; 
 
 (* theorems for equivalence relations *)
 goal thy "(x::'a::er) : D";
-br DomainI 1;
-br er_refl 1;
+by (rtac DomainI 1);
+by (rtac er_refl 1);
 qed "er_Domain";
 
 (* witnesses for "=>" ::(per,per)per  *)
@@ -106,9 +106,9 @@
 by (safe_tac HOL_cs);
 by (REPEAT (dtac spec 1));
 by (res_inst_tac [("y","g y")] per_trans 1);
-br mp 1;ba 1;
+by (rtac mp 1);by (assume_tac 1);
 by (Asm_simp_tac 1);
-br mp 1;ba 1;
+by (rtac mp 1);by (assume_tac 1);
 by (asm_simp_tac (!simpset addsimps [sym2refl2]) 1);
 qed "per_trans_fun";
 
diff -r fdb1768ebd3e -r a8ab7c64817c src/HOL/Subst/Subst.ML
--- a/src/HOL/Subst/Subst.ML	Mon Jun 23 10:35:49 1997 +0200
+++ b/src/HOL/Subst/Subst.ML	Mon Jun 23 10:42:03 1997 +0200
@@ -25,7 +25,7 @@
 
 goal Subst.thy  "~ (Var(v) <: t) --> t <| (v,t <| s) # s = t <| s";
 by (case_tac "t = Var(v)" 1);
-be rev_mp 2;
+by (etac rev_mp 2);
 by (res_inst_tac [("P",
     "%x.~x=Var(v) --> ~(Var(v) <: x) --> x <| (v,t<|s)#s=x<|s")]
     uterm.induct 2);
@@ -41,7 +41,7 @@
 qed "agreement";
 
 goal Subst.thy   "~ v: vars_of(t) --> t <| (v,u)#s = t <| s";
-by(simp_tac (!simpset addsimps [agreement]
+by (simp_tac (!simpset addsimps [agreement]
                       setloop (split_tac [expand_if])) 1);
 qed_spec_mp"repl_invariance";
 
diff -r fdb1768ebd3e -r a8ab7c64817c src/HOL/Subst/Unifier.ML
--- a/src/HOL/Subst/Unifier.ML	Mon Jun 23 10:35:49 1997 +0200
+++ b/src/HOL/Subst/Unifier.ML	Mon Jun 23 10:42:03 1997 +0200
@@ -56,7 +56,7 @@
 by (simp_tac(!simpset addsimps [MGU_iff, Unifier_def, MoreGeneral_def]
 	              delsimps [subst_Var]) 1);
 by (Step_tac 1);
-br exI 1;
+by (rtac exI 1);
 by (etac subst 1 THEN rtac (Cons_trivial RS subst_sym) 1);
 by (etac ssubst_subst2 1);
 by (asm_simp_tac (!simpset addsimps [Var_not_occs]) 1);
diff -r fdb1768ebd3e -r a8ab7c64817c src/HOL/Trancl.ML
--- a/src/HOL/Trancl.ML	Mon Jun 23 10:35:49 1997 +0200
+++ b/src/HOL/Trancl.ML	Mon Jun 23 10:42:03 1997 +0200
@@ -195,16 +195,16 @@
 qed "rtranclE2";
 
 goal Trancl.thy "r O r^* = r^* O r";
-by(Step_tac 1);
- by(blast_tac (!claset addEs [rtranclE2] addIs [rtrancl_into_rtrancl]) 1);
-by(blast_tac (!claset addEs [rtranclE] addIs [rtrancl_into_rtrancl2]) 1);
+by (Step_tac 1);
+ by (blast_tac (!claset addEs [rtranclE2] addIs [rtrancl_into_rtrancl]) 1);
+by (blast_tac (!claset addEs [rtranclE] addIs [rtrancl_into_rtrancl2]) 1);
 qed "r_comp_rtrancl_eq";
 
 
 (**** The relation trancl ****)
 
 goalw Trancl.thy [trancl_def] "!!p.[| p:r^+; r <= s |] ==> p:s^+";
-by(blast_tac (!claset addIs [rtrancl_mono RS subsetD]) 1);
+by (blast_tac (!claset addIs [rtrancl_mono RS subsetD]) 1);
 qed "trancl_mono";
 
 (** Conversions between trancl and rtrancl **)
@@ -279,7 +279,7 @@
 
 goalw Trancl.thy [trancl_def]
   "!!r. [| (x,y):r^*; (y,z):r^+ |] ==> (x,z):r^+";
-by(blast_tac (!claset addIs [rtrancl_trans,r_into_rtrancl]) 1);
+by (blast_tac (!claset addIs [rtrancl_trans,r_into_rtrancl]) 1);
 qed "rtrancl_trancl_trancl";
 
 val prems = goal Trancl.thy
@@ -291,22 +291,22 @@
 
 (* primitive recursion for trancl over finite relations: *)
 goal Trancl.thy "(insert (y,x) r)^+ = r^+ Un {(a,b). (a,y):r^* & (x,b):r^*}";
-br equalityI 1;
- br subsetI 1;
- by(split_all_tac 1);
- be trancl_induct 1;
-  by(blast_tac (!claset addIs [r_into_trancl]) 1);
- by(blast_tac (!claset addIs
+by (rtac equalityI 1);
+ by (rtac subsetI 1);
+ by (split_all_tac 1);
+ by (etac trancl_induct 1);
+  by (blast_tac (!claset addIs [r_into_trancl]) 1);
+ by (blast_tac (!claset addIs
      [rtrancl_into_trancl1,trancl_into_rtrancl,r_into_trancl,trancl_trans]) 1);
-br subsetI 1;
-by(blast_tac (!claset addIs
+by (rtac subsetI 1);
+by (blast_tac (!claset addIs
      [rtrancl_into_trancl2, rtrancl_trancl_trancl,
       impOfSubs rtrancl_mono, trancl_mono]) 1);
 qed "trancl_insert";
 
 goalw Trancl.thy [trancl_def] "(r^-1)^+ = (r^+)^-1";
-by(simp_tac (!simpset addsimps [rtrancl_inverse,inverse_comp]) 1);
-by(simp_tac (!simpset addsimps [rtrancl_inverse RS sym,r_comp_rtrancl_eq]) 1);
+by (simp_tac (!simpset addsimps [rtrancl_inverse,inverse_comp]) 1);
+by (simp_tac (!simpset addsimps [rtrancl_inverse RS sym,r_comp_rtrancl_eq]) 1);
 qed "trancl_inverse";
 
 
diff -r fdb1768ebd3e -r a8ab7c64817c src/HOL/WF.ML
--- a/src/HOL/WF.ML	Mon Jun 23 10:35:49 1997 +0200
+++ b/src/HOL/WF.ML	Mon Jun 23 10:42:03 1997 +0200
@@ -107,23 +107,23 @@
  *---------------------------------------------------------------------------*)
 
 goal WF.thy "wf(insert (y,x) r) = (wf(r) & (x,y) ~: r^*)";
-br iffI 1;
- by(blast_tac (!claset addEs [wf_trancl RS wf_irrefl] addIs
+by (rtac iffI 1);
+ by (blast_tac (!claset addEs [wf_trancl RS wf_irrefl] addIs
       [rtrancl_into_trancl1,wf_subset,impOfSubs rtrancl_mono]) 1);
-by(asm_full_simp_tac (!simpset addsimps [wf_eq_minimal]) 1);
-by(safe_tac (!claset));
-by(EVERY1[rtac allE, atac, etac impE, Blast_tac]);
-be bexE 1;
-by(rename_tac "a" 1);
-by(case_tac "a = x" 1);
- by(res_inst_tac [("x","a")]bexI 2);
-  ba 3;
- by(Blast_tac 2);
-by(case_tac "y:Q" 1);
- by(Blast_tac 2);
-by(res_inst_tac [("x","{z. z:Q & (z,y) : r^*}")]allE 1);
- ba 1;
-by(fast_tac (!claset addIs [rtrancl_into_rtrancl2]) 1);
+by (asm_full_simp_tac (!simpset addsimps [wf_eq_minimal]) 1);
+by (safe_tac (!claset));
+by (EVERY1[rtac allE, atac, etac impE, Blast_tac]);
+by (etac bexE 1);
+by (rename_tac "a" 1);
+by (case_tac "a = x" 1);
+ by (res_inst_tac [("x","a")]bexI 2);
+  by (assume_tac 3);
+ by (Blast_tac 2);
+by (case_tac "y:Q" 1);
+ by (Blast_tac 2);
+by (res_inst_tac [("x","{z. z:Q & (z,y) : r^*}")]allE 1);
+ by (assume_tac 1);
+by (fast_tac (!claset addIs [rtrancl_into_rtrancl2]) 1);
 qed "wf_insert";
 AddIffs [wf_insert];
 
@@ -131,18 +131,18 @@
 
 goalw WF.thy [acyclic_def]
  "!!r. wf r ==> acyclic r";
-by(blast_tac (!claset addEs [wf_trancl RS wf_irrefl]) 1);
+by (blast_tac (!claset addEs [wf_trancl RS wf_irrefl]) 1);
 qed "wf_acyclic";
 
 goalw WF.thy [acyclic_def]
   "acyclic(insert (y,x) r) = (acyclic r & (x,y) ~: r^*)";
-by(simp_tac (!simpset addsimps [trancl_insert]) 1);
-by(blast_tac (!claset addEs [make_elim rtrancl_trans]) 1);
+by (simp_tac (!simpset addsimps [trancl_insert]) 1);
+by (blast_tac (!claset addEs [make_elim rtrancl_trans]) 1);
 qed "acyclic_insert";
 AddIffs [acyclic_insert];
 
 goalw WF.thy [acyclic_def] "acyclic(r^-1) = acyclic r";
-by(simp_tac (!simpset addsimps [trancl_inverse]) 1);
+by (simp_tac (!simpset addsimps [trancl_inverse]) 1);
 qed "acyclic_inverse";
 
 (** cut **)
diff -r fdb1768ebd3e -r a8ab7c64817c src/HOL/WF_Rel.ML
--- a/src/HOL/WF_Rel.ML	Mon Jun 23 10:35:49 1997 +0200
+++ b/src/HOL/WF_Rel.ML	Mon Jun 23 10:42:03 1997 +0200
@@ -106,14 +106,14 @@
  *---------------------------------------------------------------------------*)
 
 goal thy "!!r. finite r ==> acyclic r --> wf r";
-be finite_induct 1;
- by(Blast_tac 1);
-by(split_all_tac 1);
-by(Asm_full_simp_tac 1);
+by (etac finite_induct 1);
+ by (Blast_tac 1);
+by (split_all_tac 1);
+by (Asm_full_simp_tac 1);
 qed_spec_mp "finite_acyclic_wf";
 
 goal thy "!!r. finite r ==> wf r = acyclic r";
-by(blast_tac (!claset addIs [finite_acyclic_wf,wf_acyclic]) 1);
+by (blast_tac (!claset addIs [finite_acyclic_wf,wf_acyclic]) 1);
 qed "wf_iff_acyclic_if_finite";
 
 
@@ -123,26 +123,26 @@
 
 goalw thy [wf_eq_minimal RS eq_reflection]
   "wf r = (~(? f. !i. (f(Suc i),f i) : r))";
-br iffI 1;
- br notI 1;
- be exE 1;
- by(eres_inst_tac [("x","{w. ? i. w=f i}")] allE 1);
- by(Blast_tac 1);
-be swap 1;
+by (rtac iffI 1);
+ by (rtac notI 1);
+ by (etac exE 1);
+ by (eres_inst_tac [("x","{w. ? i. w=f i}")] allE 1);
+ by (Blast_tac 1);
+by (etac swap 1);
 by (Asm_full_simp_tac 1);
 by (Step_tac 1);
-by(subgoal_tac "!n. nat_rec x (%i y. @z. z:Q & (z,y):r) n : Q" 1);
+by (subgoal_tac "!n. nat_rec x (%i y. @z. z:Q & (z,y):r) n : Q" 1);
  by (res_inst_tac[("x","nat_rec x (%i y. @z. z:Q & (z,y):r)")]exI 1);
- br allI 1;
- by(Simp_tac 1);
- br selectI2EX 1;
-  by(Blast_tac 1);
- by(Blast_tac 1);
-br allI 1;
-by(induct_tac "n" 1);
- by(Asm_simp_tac 1);
-by(Simp_tac 1);
-br selectI2EX 1;
- by(Blast_tac 1);
-by(Blast_tac 1);
+ by (rtac allI 1);
+ by (Simp_tac 1);
+ by (rtac selectI2EX 1);
+  by (Blast_tac 1);
+ by (Blast_tac 1);
+by (rtac allI 1);
+by (induct_tac "n" 1);
+ by (Asm_simp_tac 1);
+by (Simp_tac 1);
+by (rtac selectI2EX 1);
+ by (Blast_tac 1);
+by (Blast_tac 1);
 qed "wf_iff_no_infinite_down_chain";
diff -r fdb1768ebd3e -r a8ab7c64817c src/HOL/equalities.ML
--- a/src/HOL/equalities.ML	Mon Jun 23 10:35:49 1997 +0200
+++ b/src/HOL/equalities.ML	Mon Jun 23 10:42:03 1997 +0200
@@ -100,7 +100,7 @@
 qed "image_id";
 
 goal Set.thy "f``(range g) = range (%x. f (g x))";
-by(Blast_tac 1);
+by (Blast_tac 1);
 qed "image_range";
 
 qed_goal "ball_image" Set.thy "(!y:F``S. P y) = (!x:S. P (F x))"
@@ -379,7 +379,7 @@
 Addsimps[UN_empty];
 
 goal Set.thy "(UN x:A. {}) = {}";
-by(Blast_tac 1);
+by (Blast_tac 1);
 qed "UN_empty2";
 Addsimps[UN_empty2];
 
@@ -635,7 +635,7 @@
 
 goal Set.thy "Pow (insert a A) = Pow A Un (insert a `` Pow A)";
 by (Step_tac 1);
-be swap 1;
+by (etac swap 1);
 by (res_inst_tac [("x", "x-{a}")] image_eqI 1);
 by (ALLGOALS Blast_tac);
 qed "Pow_insert";
diff -r fdb1768ebd3e -r a8ab7c64817c src/HOL/ex/Primes.ML
--- a/src/HOL/ex/Primes.ML	Mon Jun 23 10:35:49 1997 +0200
+++ b/src/HOL/ex/Primes.ML	Mon Jun 23 10:42:03 1997 +0200
@@ -89,8 +89,8 @@
 goalw thy [prime_def] "!!p. [| p: prime; p dvd (m*n) |] ==> p dvd m | p dvd n";
 by (Step_tac 1);
 by (subgoal_tac "m = gcd(m*p, m*n)" 1);
-be ssubst 1;
-br gcd_greatest 1;
+by (etac ssubst 1);
+by (rtac gcd_greatest 1);
 by (ALLGOALS (asm_simp_tac (!simpset addsimps [gcd_mult_distrib2 RS sym])));
 (*Now deduce  gcd(p,n)=1  to finish the proof*)
 by (cut_inst_tac [("m","p"),("n","n")] gcd_divides_both 1);
diff -r fdb1768ebd3e -r a8ab7c64817c src/HOL/ex/Primrec.ML
--- a/src/HOL/ex/Primrec.ML	Mon Jun 23 10:35:49 1997 +0200
+++ b/src/HOL/ex/Primrec.ML	Mon Jun 23 10:42:03 1997 +0200
@@ -128,7 +128,7 @@
 val lemma = result();
 
 goal thy "!!i j k. i<j ==> ack(i,k) < ack(j,k)";
-be less_natE 1;
+by (etac less_natE 1);
 by (blast_tac (!claset addSIs [lemma]) 1);
 qed "ack_less_mono1";
 
@@ -248,8 +248,8 @@
  "!!f g. [| ALL l. f l < ack(kf, list_add l);        \
 \           ALL l. g l < ack(kg, list_add l)         \
 \        |] ==> EX k. ALL l. PREC f g l< ack(k, list_add l)";
-br exI 1;
-br allI 1;
+by (rtac exI 1);
+by (rtac allI 1);
 by (rtac ([le_add1, PREC_case_lemma] MRS le_less_trans) 1);
 by (REPEAT (blast_tac (!claset addIs [ack_add_bound2]) 1));
 qed "PREC_case";
diff -r fdb1768ebd3e -r a8ab7c64817c src/HOLCF/IMP/Denotational.ML
--- a/src/HOLCF/IMP/Denotational.ML	Mon Jun 23 10:35:49 1997 +0200
+++ b/src/HOLCF/IMP/Denotational.ML	Mon Jun 23 10:42:03 1997 +0200
@@ -7,25 +7,25 @@
 *)
 
 goalw thy [dlift_def] "dlift f`(Def x) = f`(Discr x)";
-by(Simp_tac 1);
+by (Simp_tac 1);
 qed "dlift_Def";
 Addsimps [dlift_Def];
 
 goalw thy [dlift_def] "cont(%f. dlift f)";
-by(Simp_tac 1);
+by (Simp_tac 1);
 qed "cont_dlift";
 AddIffs [cont_dlift];
 
 goalw thy [dlift_def]
  "(dlift f`l = Def y) = (? x. l = Def x & f`(Discr x) = Def y)";
-by(simp_tac (!simpset setloop (split_tac[expand_lift_case])) 1);
+by (simp_tac (!simpset setloop (split_tac[expand_lift_case])) 1);
 qed "dlift_is_Def";
 Addsimps [dlift_is_Def];
 
 goal thy "!!c. <c,s> -c-> t ==> D c`(Discr s) = (Def t)";
-be evalc.induct 1;
+by (etac evalc.induct 1);
       by (ALLGOALS Asm_simp_tac);
- by (ALLGOALS (rtac (fix_eq RS ssubst) THEN' Asm_full_simp_tac));
+ by (ALLGOALS (stac fix_eq THEN' Asm_full_simp_tac));
 qed_spec_mp "eval_implies_D";
 
 goal thy "!s t. D c`(Discr s) = (Def t) --> <c,s> -c-> t";
@@ -36,8 +36,8 @@
  by (simp_tac (!simpset setloop (split_tac[expand_if])) 1);
  by (fast_tac ((HOL_cs addIs evalc.intrs) addss !simpset) 1);
 by (Simp_tac 1);
-br fix_ind 1;
-  by(fast_tac (HOL_cs addSIs (adm_lemmas@[adm_chfindom,ax_flat_lift])) 1);
+by (rtac fix_ind 1);
+  by (fast_tac (HOL_cs addSIs (adm_lemmas@[adm_chfindom,ax_flat_lift])) 1);
  by (Simp_tac 1);
 by (simp_tac (!simpset setloop (split_tac[expand_if])) 1);
 by (safe_tac HOL_cs);
diff -r fdb1768ebd3e -r a8ab7c64817c src/HOLCF/IOA/meta_theory/Automata.ML
--- a/src/HOLCF/IOA/meta_theory/Automata.ML	Mon Jun 23 10:35:49 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/Automata.ML	Mon Jun 23 10:42:03 1997 +0200
@@ -32,7 +32,7 @@
 
 goal thy
 "starts_of(A || B) = {p. fst(p):starts_of(A) & snd(p):starts_of(B)}";
-  by(simp_tac (!simpset addsimps (par_def::ioa_projections)) 1);
+  by (simp_tac (!simpset addsimps (par_def::ioa_projections)) 1);
 qed "starts_of_par";
 
 
@@ -43,14 +43,14 @@
 
 goal thy 
 "actions(asig_comp a b) = actions(a) Un actions(b)";
-  by(simp_tac (!simpset addsimps
+  by (simp_tac (!simpset addsimps
                ([actions_def,asig_comp_def]@asig_projections)) 1);
   by (fast_tac (set_cs addSIs [equalityI]) 1);
 qed "actions_asig_comp";
 
 
 goal thy "asig_of(A || B) = asig_comp (asig_of A) (asig_of B)";
-  by(simp_tac (!simpset addsimps (par_def::ioa_projections)) 1);
+  by (simp_tac (!simpset addsimps (par_def::ioa_projections)) 1);
 qed "asig_of_par";
 
 
@@ -90,7 +90,7 @@
 
 goal thy"compatible A B = compatible B A";
 by (asm_full_simp_tac (!simpset addsimps [compatible_def,Int_commute]) 1);
-auto();
+by (Auto_tac());
 qed"compat_commute";
 
 goalw thy [externals_def,actions_def,compatible_def]
@@ -167,21 +167,21 @@
 
 goal thy "starts_of(restrict ioa acts) = starts_of(ioa) &     \
 \             trans_of(restrict ioa acts) = trans_of(ioa)";
-by(simp_tac (!simpset addsimps ([restrict_def]@ioa_projections)) 1);
+by (simp_tac (!simpset addsimps ([restrict_def]@ioa_projections)) 1);
 qed "cancel_restrict_a";
 
 goal thy "reachable (restrict ioa acts) s = reachable ioa s";
 by (rtac iffI 1);
-be reachable.induct 1;
-by(asm_full_simp_tac (!simpset addsimps [cancel_restrict_a,reachable_0]) 1);
+by (etac reachable.induct 1);
+by (asm_full_simp_tac (!simpset addsimps [cancel_restrict_a,reachable_0]) 1);
 by (etac reachable_n 1);
-by(asm_full_simp_tac (!simpset addsimps [cancel_restrict_a]) 1);
+by (asm_full_simp_tac (!simpset addsimps [cancel_restrict_a]) 1);
 (* <--  *)
-be reachable.induct 1;
+by (etac reachable.induct 1);
 by (rtac reachable_0 1);
-by(asm_full_simp_tac (!simpset addsimps [cancel_restrict_a]) 1);
+by (asm_full_simp_tac (!simpset addsimps [cancel_restrict_a]) 1);
 by (etac reachable_n 1);
-by(asm_full_simp_tac (!simpset addsimps [cancel_restrict_a]) 1);
+by (asm_full_simp_tac (!simpset addsimps [cancel_restrict_a]) 1);
 qed "cancel_restrict_b";
 
 goal thy "starts_of(restrict ioa acts) = starts_of(ioa) &     \
@@ -202,14 +202,14 @@
 
 
 goal thy "!!s.[| reachable (rename C g) s |] ==> reachable C s";
-be reachable.induct 1;
-br reachable_0 1;
-by(asm_full_simp_tac (!simpset addsimps [rename_def]@ioa_projections) 1);
-bd trans_rename 1;
-be exE 1;
-be conjE 1;
-be reachable_n 1;
-ba 1;
+by (etac reachable.induct 1);
+by (rtac reachable_0 1);
+by (asm_full_simp_tac (!simpset addsimps [rename_def]@ioa_projections) 1);
+by (dtac trans_rename 1);
+by (etac exE 1);
+by (etac conjE 1);
+by (etac reachable_n 1);
+by (assume_tac 1);
 qed"reachable_rename";
 
 
@@ -282,7 +282,7 @@
 \     (snd(snd(snd(s))),a,snd(snd(snd(t)))):trans_of(D)                      \
 \   else snd(snd(snd(t)))=snd(snd(snd(s)))))";
 
-  by(simp_tac (!simpset addsimps ([par_def,actions_asig_comp,Pair_fst_snd_eq,Let_def]@
+  by (simp_tac (!simpset addsimps ([par_def,actions_asig_comp,Pair_fst_snd_eq,Let_def]@
                             ioa_projections)
                   setloop (split_tac [expand_if])) 1);
 qed "trans_of_par4";
diff -r fdb1768ebd3e -r a8ab7c64817c src/HOLCF/IOA/meta_theory/CompoExecs.ML
--- a/src/HOLCF/IOA/meta_theory/CompoExecs.ML	Mon Jun 23 10:35:49 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/CompoExecs.ML	Mon Jun 23 10:42:03 1997 +0200
@@ -89,9 +89,9 @@
 \             `x) \
 \           ))";
 by (rtac trans 1);
-br fix_eq2 1;
-br stutter2_def 1;
-br beta_cfun 1;
+by (rtac fix_eq2 1);
+by (rtac stutter2_def 1);
+by (rtac beta_cfun 1);
 by (simp_tac (!simpset addsimps [flift1_def]) 1);
 qed"stutter2_unfold";
 
@@ -108,7 +108,7 @@
 goal thy "(stutter2 A`(at>>xs)) s = \
 \              ((if (fst at)~:act A then Def (s=snd at) else TT) \
 \                andalso (stutter2 A`xs) (snd at))"; 
-br trans 1;
+by (rtac trans 1);
 by (stac stutter2_unfold 1);
 by (asm_full_simp_tac (!simpset addsimps [Cons_def,flift1_def,If_and_if]) 1);
 by (Simp_tac 1);
diff -r fdb1768ebd3e -r a8ab7c64817c src/HOLCF/IOA/meta_theory/CompoScheds.ML
--- a/src/HOLCF/IOA/meta_theory/CompoScheds.ML	Mon Jun 23 10:35:49 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/CompoScheds.ML	Mon Jun 23 10:42:03 1997 +0200
@@ -69,7 +69,7 @@
 goal thy "!!x.[| x:act A; x~:act B; HD`exA=Def a|] \
 \   ==> (mkex2 A B`(x>>sch)`exA`exB) s t =   \
 \       (x,snd a,t) >> (mkex2 A B`sch`(TL`exA)`exB) (snd a) t";
-br trans 1;
+by (rtac trans 1);
 by (stac mkex2_unfold 1);
 by (asm_full_simp_tac (!simpset addsimps [Cons_def,If_and_if]) 1);
 by (asm_full_simp_tac (!simpset addsimps [Cons_def]) 1);
@@ -78,7 +78,7 @@
 goal thy "!!x.[| x~:act A; x:act B; HD`exB=Def b|] \
 \   ==> (mkex2 A B`(x>>sch)`exA`exB) s t = \
 \       (x,s,snd b) >> (mkex2 A B`sch`exA`(TL`exB)) s (snd b)";
-br trans 1;
+by (rtac trans 1);
 by (stac mkex2_unfold 1);
 by (asm_full_simp_tac (!simpset addsimps [Cons_def,If_and_if]) 1);
 by (asm_full_simp_tac (!simpset addsimps [Cons_def]) 1);
@@ -88,7 +88,7 @@
 \   ==> (mkex2 A B`(x>>sch)`exA`exB) s t =  \
 \        (x,snd a,snd b) >> \
 \           (mkex2 A B`sch`(TL`exA)`(TL`exB)) (snd a) (snd b)";
-br trans 1;
+by (rtac trans 1);
 by (stac mkex2_unfold 1);
 by (asm_full_simp_tac (!simpset addsimps [Cons_def,If_and_if]) 1);
 by (asm_full_simp_tac (!simpset addsimps [Cons_def]) 1);
@@ -115,7 +115,7 @@
 by (simp_tac (!simpset addsimps [mkex_def] 
                        setloop (split_tac [expand_if]) ) 1);
 by (cut_inst_tac [("exA","a>>exA")] mkex2_cons_1 1);
-auto();
+by (Auto_tac());
 qed"mkex_cons_1";
 
 goal thy "!!x.[| x~:act A; x:act B |] \
@@ -124,7 +124,7 @@
 by (simp_tac (!simpset addsimps [mkex_def] 
                        setloop (split_tac [expand_if]) ) 1);
 by (cut_inst_tac [("exB","b>>exB")] mkex2_cons_2 1);
-auto();
+by (Auto_tac());
 qed"mkex_cons_2";
 
 goal thy "!!x.[| x:act A; x:act B |]  \
@@ -133,7 +133,7 @@
 by (simp_tac (!simpset addsimps [mkex_def] 
                        setloop (split_tac [expand_if]) ) 1);
 by (cut_inst_tac [("exB","b>>exB"),("exA","a>>exA")] mkex2_cons_3 1);
-auto();
+by (Auto_tac());
 qed"mkex_cons_3";
 
 Delsimps [mkex2_UU,mkex2_nil,mkex2_cons_1,mkex2_cons_2,mkex2_cons_3];
@@ -289,8 +289,8 @@
 by (cut_facts_tac [stutterA_mkex] 1);
 by (asm_full_simp_tac (!simpset addsimps [stutter_def,ProjA_def,mkex_def]) 1);
 by (REPEAT (etac allE 1));
-bd mp 1;
-ba 2;
+by (dtac mp 1);
+by (assume_tac 2);
 by (Asm_full_simp_tac 1);
 qed"stutter_mkex_on_A";
 
@@ -320,8 +320,8 @@
 by (cut_facts_tac [stutterB_mkex] 1);
 by (asm_full_simp_tac (!simpset addsimps [stutter_def,ProjB_def,mkex_def]) 1);
 by (REPEAT (etac allE 1));
-bd mp 1;
-ba 2;
+by (dtac mp 1);
+by (assume_tac 2);
 by (Asm_full_simp_tac 1);
 qed"stutter_mkex_on_B";
 
@@ -380,11 +380,11 @@
 by (asm_full_simp_tac (!simpset addsimps [ProjA_def,Filter_ex_def]) 1);
 by (pair_tac "exA" 1);
 by (pair_tac "exB" 1);
-br conjI 1;
+by (rtac conjI 1);
 by (simp_tac (!simpset addsimps [mkex_def]) 1);
 by (stac trick_against_eq_in_ass 1);
 back();
-ba 1;
+by (assume_tac 1);
 by (asm_full_simp_tac (!simpset addsimps [filter_mkex_is_exA_tmp]) 1);
 qed"filter_mkex_is_exA";
  
@@ -424,11 +424,11 @@
 by (asm_full_simp_tac (!simpset addsimps [ProjB_def,Filter_ex_def]) 1);
 by (pair_tac "exA" 1);
 by (pair_tac "exB" 1);
-br conjI 1;
+by (rtac conjI 1);
 by (simp_tac (!simpset addsimps [mkex_def]) 1);
 by (stac trick_against_eq_in_ass 1);
 back();
-ba 1;
+by (assume_tac 1);
 by (asm_full_simp_tac (!simpset addsimps [filter_mkex_is_exB_tmp]) 1);
 qed"filter_mkex_is_exB";
 
@@ -473,7 +473,7 @@
                                  lemma_2_1a,lemma_2_1b]) 1);
 by (asm_full_simp_tac (!simpset addsimps [executions_def]) 1);
 by (pair_tac "ex" 1);
-be conjE 1;
+by (etac conjE 1);
 by (asm_full_simp_tac (!simpset addsimps [sch_actions_in_AorB]) 1);
 
 (* <== *)
diff -r fdb1768ebd3e -r a8ab7c64817c src/HOLCF/IOA/meta_theory/CompoTraces.ML
--- a/src/HOLCF/IOA/meta_theory/CompoTraces.ML	Mon Jun 23 10:35:49 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/CompoTraces.ML	Mon Jun 23 10:42:03 1997 +0200
@@ -65,7 +65,7 @@
 \         (Takewhile (%a.a:int A)`schA) \
 \         @@ (x>>(mksch A B`tr`(TL`(Dropwhile (%a.a:int A)`schA)) \
 \                             `schB))";
-br trans 1;
+by (rtac trans 1);
 by (stac mksch_unfold 1);
 by (asm_full_simp_tac (!simpset addsimps [Cons_def,If_and_if]) 1);
 by (simp_tac (!simpset addsimps [Cons_def]) 1);
@@ -76,7 +76,7 @@
 \        (Takewhile (%a.a:int B)`schB)  \
 \         @@ (x>>(mksch A B`tr`schA`(TL`(Dropwhile (%a.a:int B)`schB))  \
 \                            ))";
-br trans 1;
+by (rtac trans 1);
 by (stac mksch_unfold 1);
 by (asm_full_simp_tac (!simpset addsimps [Cons_def,If_and_if]) 1);
 by (simp_tac (!simpset addsimps [Cons_def]) 1);
@@ -89,7 +89,7 @@
 \         @@ (x>>(mksch A B`tr`(TL`(Dropwhile (%a.a:int A)`schA)) \
 \                            `(TL`(Dropwhile (%a.a:int B)`schB))))  \
 \             )";
-br trans 1;
+by (rtac trans 1);
 by (stac mksch_unfold 1);
 by (asm_full_simp_tac (!simpset addsimps [Cons_def,If_and_if]) 1);
 by (simp_tac (!simpset addsimps [Cons_def]) 1);
@@ -136,13 +136,13 @@
 (* Lemma for substitution of looping assumption in another specific assumption *) 
 val [p1,p2] = goal thy "[| f << (g x) ; x=(h x) |] ==> f << g (h x)";
 by (cut_facts_tac [p1] 1);
-be (p2 RS subst) 1;
+by (etac (p2 RS subst) 1);
 qed"subst_lemma1";
 
 (* Lemma for substitution of looping assumption in another specific assumption *) 
 val [p1,p2] = goal thy "[| (f x) = y >> g; x=(h x) |] ==> (f (h x)) = y >> g";
 by (cut_facts_tac [p1] 1);
-be (p2 RS subst) 1;
+by (etac (p2 RS subst) 1);
 qed"subst_lemma2";
 
 
@@ -156,21 +156,21 @@
 by (case_tac "a:act B" 1);
 (* a:A, a:B *)
 by (Asm_full_simp_tac 1);
-br (Forall_Conc_impl RS mp) 1;
+by (rtac (Forall_Conc_impl RS mp) 1);
 by (asm_full_simp_tac (!simpset addsimps [ForallPTakewhileQ,intA_is_not_actB,int_is_act]) 1);
-br (Forall_Conc_impl RS mp) 1;
+by (rtac (Forall_Conc_impl RS mp) 1);
 by (asm_full_simp_tac (!simpset addsimps [ForallPTakewhileQ,intA_is_not_actB,int_is_act]) 1);
 (* a:A,a~:B *)
 by (Asm_full_simp_tac 1);
-br (Forall_Conc_impl RS mp) 1;
+by (rtac (Forall_Conc_impl RS mp) 1);
 by (asm_full_simp_tac (!simpset addsimps [ForallPTakewhileQ,intA_is_not_actB,int_is_act]) 1);
 by (case_tac "a:act B" 1);
 (* a~:A, a:B *)
 by (Asm_full_simp_tac 1);
-br (Forall_Conc_impl RS mp) 1;
+by (rtac (Forall_Conc_impl RS mp) 1);
 by (asm_full_simp_tac (!simpset addsimps [ForallPTakewhileQ,intA_is_not_actB,int_is_act]) 1);
 (* a~:A,a~:B *)
-auto();
+by (Auto_tac());
 qed"ForallAorB_mksch1";
 
 bind_thm ("ForallAorB_mksch",ForallAorB_mksch1 RS spec RS spec RS mp);
@@ -181,7 +181,7 @@
 
 by (Seq_induct_tac "tr" [Forall_def,sforall_def,mksch_def] 1);
 by (safe_tac set_cs);
-br (Forall_Conc_impl RS mp) 1;
+by (rtac (Forall_Conc_impl RS mp) 1);
 by (asm_full_simp_tac (!simpset addsimps [ForallPTakewhileQ,
                             intA_is_not_actB,int_is_act]) 1);
 qed"ForallBnA_mksch";
@@ -196,7 +196,7 @@
 by (Seq_induct_tac "tr" [Forall_def,sforall_def,mksch_def] 1);
 by (safe_tac set_cs);
 by (Asm_full_simp_tac 1);
-br (Forall_Conc_impl RS mp) 1;
+by (rtac (Forall_Conc_impl RS mp) 1);
 by (asm_full_simp_tac (!simpset addsimps [ForallPTakewhileQ,
                        intA_is_not_actB,int_is_act]) 1);
 qed"ForallAnB_mksch";
@@ -214,7 +214,7 @@
 \          Forall (%x. x:ext (A||B)) tr \
 \          --> Finite (mksch A B`tr`x`y)";
 
-be Seq_Finite_ind  1;
+by (etac Seq_Finite_ind  1);
 by (Asm_full_simp_tac 1);
 (* main case *)
 by (asm_full_simp_tac (!simpset setloop split_tac [expand_if]) 1);
@@ -231,10 +231,10 @@
 (* now for conclusion IH applicable, but assumptions have to be transformed *)
 by (dres_inst_tac [("x","x"),
                    ("g","Filter (%a. a:act A)`s")] subst_lemma2 1);
-ba 1;
+by (assume_tac 1);
 by (dres_inst_tac [("x","y"),
                    ("g","Filter (%a. a:act B)`s")] subst_lemma2 1);
-ba 1;
+by (assume_tac 1);
 (* IH *)
 by (asm_full_simp_tac (!simpset addsimps [not_ext_is_int_or_not_act,
                    FilterPTakewhileQnil,ForallTL,ForallDropwhile]) 1);
@@ -249,7 +249,7 @@
 (* now for conclusion IH applicable, but assumptions have to be transformed *)
 by (dres_inst_tac [("x","y"),
                    ("g","Filter (%a. a:act B)`s")] subst_lemma2 1);
-ba 1;
+by (assume_tac 1);
 (* IH *)
 by (asm_full_simp_tac (!simpset addsimps [not_ext_is_int_or_not_act,
                    FilterPTakewhileQnil,ForallTL,ForallDropwhile]) 1);
@@ -264,7 +264,7 @@
 (* now for conclusion IH applicable, but assumptions have to be transformed *)
 by (dres_inst_tac [("x","x"),
                    ("g","Filter (%a. a:act A)`s")] subst_lemma2 1);
-ba 1;
+by (assume_tac 1);
 (* IH *)
 by (asm_full_simp_tac (!simpset addsimps [not_ext_is_int_or_not_act,
                    FilterPTakewhileQnil,ForallTL,ForallDropwhile]) 1);
@@ -290,7 +290,7 @@
 \                   Finite y1 & y = (y1 @@ y2) & \
 \                   Filter (%a. a:ext B)`y1 = bs)";
 by (forw_inst_tac [("A2","A")] (compat_commute RS iffD1) 1);
-be Seq_Finite_ind  1;
+by (etac Seq_Finite_ind  1);
 by (REPEAT (rtac allI 1));
 by (rtac impI 1);
 by (res_inst_tac [("x","nil")] exI 1);
@@ -308,7 +308,7 @@
 (* transform assumption f eB y = f B (s@z) *)
 by (dres_inst_tac [("x","y"),
                    ("g","Filter (%a. a:act B)`(s@@z)")] subst_lemma2 1);
-ba 1;
+by (assume_tac 1);
 Addsimps [FilterConc]; 
 by (asm_full_simp_tac (!simpset addsimps [FilterPTakewhileQnil,not_ext_is_int_or_not_act]) 1);
 (* apply IH *)
@@ -345,7 +345,7 @@
 \                   Finite x1 & x = (x1 @@ x2) & \
 \                   Filter (%a. a:ext A)`x1 = as)";
 by (forw_inst_tac [("A2","A")] (compat_commute RS iffD1) 1);
-be Seq_Finite_ind  1;
+by (etac Seq_Finite_ind  1);
 by (REPEAT (rtac allI 1));
 by (rtac impI 1);
 by (res_inst_tac [("x","nil")] exI 1);
@@ -363,7 +363,7 @@
 (* transform assumption f eA x = f A (s@z) *)
 by (dres_inst_tac [("x","x"),
                    ("g","Filter (%a. a:act A)`(s@@z)")] subst_lemma2 1);
-ba 1;
+by (assume_tac 1);
 Addsimps [FilterConc]; 
 by (asm_full_simp_tac (!simpset addsimps [FilterPTakewhileQnil,not_ext_is_int_or_not_act]) 1);
 (* apply IH *)
@@ -394,13 +394,13 @@
 goal thy "!! y.Finite y ==> ! z tr. Forall (%a.a:ext (A||B)) tr & \
 \                             y = z @@ mksch A B`tr`a`b\
 \                             --> Finite tr";
-be Seq_Finite_ind  1;
-auto();
+by (etac Seq_Finite_ind  1);
+by (Auto_tac());
 by (Seq_case_simp_tac "tr" 1);
 (* tr = UU *)
 by (asm_full_simp_tac (!simpset addsimps [nil_is_Conc]) 1);
 (* tr = nil *)
-auto();
+by (Auto_tac());
 (* tr = Conc *)
 ren "s ss" 1;
 
@@ -419,7 +419,7 @@
 by (Seq_case_simp_tac "tr" 1);
 (* tr = UU *)
 by (asm_full_simp_tac (!simpset addsimps [Conc_Conc_eq]) 1);
-auto();
+by (Auto_tac());
 (* tr = nil ok *)
 (* tr = Conc *)
 by (Seq_case_simp_tac "z" 1);
@@ -452,19 +452,19 @@
 
 goal thy "(x>>xs = y @@ z) = ((y=nil & x>>xs=z) | (? ys. y=x>>ys & xs=ys@@z))";
 by (Seq_case_simp_tac "y" 1);
-auto();
+by (Auto_tac());
 qed"Conc_Conc_eq";
 
 goal thy "!! (y::'a Seq).Finite y ==> ~ y= x@@UU";
-be Seq_Finite_ind 1;
+by (etac Seq_Finite_ind 1);
 by (Seq_case_simp_tac "x" 1);
 by (Seq_case_simp_tac "x" 1);
-auto();
+by (Auto_tac());
 qed"FiniteConcUU1";
 
 goal thy "~ Finite ((x::'a Seq)@@UU)";
-br (FiniteConcUU1 COMP rev_contrapos) 1;
-auto();
+by (rtac (FiniteConcUU1 COMP rev_contrapos) 1);
+by (Auto_tac());
 qed"FiniteConcUU";
 
 finiteR_mksch
@@ -505,9 +505,9 @@
            externals_of_par, intA_is_not_extB,int_is_not_ext]) 1);
 (* conclusion of IH ok, but assumptions of IH have to be transformed *)
 by (dres_inst_tac [("x","schA")] subst_lemma1 1);
-ba 1;
+by (assume_tac 1);
 by (dres_inst_tac [("x","schB")] subst_lemma1 1);
-ba 1;
+by (assume_tac 1);
 (* IH *)
 by (asm_full_simp_tac (!simpset addsimps [not_ext_is_int_or_not_act,
                    FilterPTakewhileQnil,ForallTL,ForallDropwhile]) 1);
@@ -521,7 +521,7 @@
            externals_of_par, intA_is_not_extB,int_is_not_ext]) 1);
 by (dres_inst_tac [("x","schB")] subst_lemma1 1);
 back();
-ba 1;
+by (assume_tac 1);
 by (asm_full_simp_tac (!simpset addsimps [not_ext_is_int_or_not_act,
                     FilterPTakewhileQnil,ForallTL,ForallDropwhile]) 1);
 (* Case a:A, a~:B *)
@@ -533,7 +533,7 @@
           [FilterPTakewhileQnil,not_ext_is_int_or_not_act,
            externals_of_par, intA_is_not_extB,int_is_not_ext]) 1);
 by (dres_inst_tac [("x","schA")] subst_lemma1 1);
-ba 1;
+by (assume_tac 1);
 by (asm_full_simp_tac (!simpset addsimps [not_ext_is_int_or_not_act,
                     FilterPTakewhileQnil,ForallTL,ForallDropwhile]) 1);
 (* Case a~:A, a~:B *)
@@ -614,8 +614,8 @@
 (* eliminate the B-only prefix *)
 
 by (subgoal_tac "(Filter (%a.a :act A)`y1) = nil" 1);
-be ForallQFilterPnil 2;
-ba 2;
+by (etac ForallQFilterPnil 2);
+by (assume_tac 2);
 by (Fast_tac 2);
 
 (* Now real recursive step follows (in y) *)
@@ -630,8 +630,8 @@
 by (rotate_tac ~1 1);
 by (Asm_full_simp_tac  1);
 (* eliminate introduced subgoal 2 *)
-be ForallQFilterPnil 2;
-ba 2;
+by (etac ForallQFilterPnil 2);
+by (assume_tac 2);
 by (Fast_tac 2);
  
 (* bring in divide Seq for s *)
@@ -643,15 +643,15 @@
 back();
 back();
 back();
-ba 1;
+by (assume_tac 1);
 
 (* reduce trace_takes from n to strictly smaller k *)
-br take_reduction 1;
+by (rtac take_reduction 1);
 
 (* f A (tw iA) = tw ~eA *)
 by (asm_full_simp_tac (!simpset addsimps [FilterPTakewhileQid,int_is_act,
                               not_ext_is_int_or_not_act]) 1);
-br refl 1;
+by (rtac refl 1);
 
 (* now conclusion fulfills induction hypothesis, but assumptions are not ready *)
 (*
@@ -665,12 +665,12 @@
 (* assumption schA *)
 by (dres_inst_tac [("x","schA"),
                    ("g","Filter (%a. a:act A)`s2")] subst_lemma2 1);
-ba 1;
+by (assume_tac 1);
 by (asm_full_simp_tac (!simpset addsimps [FilterPTakewhileQnil]) 1);
 (* assumptions concerning LastActExtsch, cannot be rewritten, as LastActExtsmalli are looping  *)
 by (dres_inst_tac [("sch","schA"),("P","%a. a:int A")] LastActExtsmall1 1);
 by (dres_inst_tac [("sch1.0","y1")]  LastActExtsmall2 1);
-ba 1;
+by (assume_tac 1);
 
 FIX: problem: schA and schB are not quantified in the new take lemma version !!!
 
@@ -699,15 +699,15 @@
 \ --> Filter (%a.a:act A)`(mksch A B`tr`schA`schB) = schA";
 
 by (strip_tac 1);
-br seq.take_lemma 1;
-br mp 1;
-ba 2;
+by (rtac seq.take_lemma 1);
+by (rtac mp 1);
+by (assume_tac 2);
 back();back();back();back();
 by (res_inst_tac [("x","schA")] spec 1);
 by (res_inst_tac [("x","schB")] spec 1);
 by (res_inst_tac [("x","tr")] spec 1);
 by (thin_tac' 5 1);
-br less_induct 1;
+by (rtac less_induct 1);
 by (REPEAT (rtac allI 1));
 ren "tr schB schA" 1;
 by (strip_tac 1);
@@ -715,7 +715,7 @@
 
 by (case_tac "Forall (%x. x:act B & x~:act A) tr" 1);
 
-br (seq_take_lemma RS iffD2 RS spec) 1;
+by (rtac (seq_take_lemma RS iffD2 RS spec) 1);
 by (thin_tac' 5 1);
 
 
@@ -731,7 +731,7 @@
 by (eres_inst_tac [("A","A")] LastActExtimplnil 1);
 by (Asm_simp_tac 1);
 by (eres_inst_tac [("Q","%x.x:act B & x~:act A")] ForallQFilterPnil 1);
-ba 1;
+by (assume_tac 1);
 by (Fast_tac 1);
 
 (* case ~ Finite s *)
@@ -748,12 +748,12 @@
 by (eres_inst_tac [("A","A")] LastActExtimplUU 1);
 by (Asm_simp_tac 1);
 by (eres_inst_tac [("Q","%x.x:act B & x~:act A")] ForallQFilterPUU 1);
-ba 1;
+by (assume_tac 1);
 by (Fast_tac 1);
 
 (* case" ~ Forall (%x.x:act B & x~:act A) s" *)
 
-bd divide_Seq3 1;
+by (dtac divide_Seq3 1);
 
 by (REPEAT (etac exE 1));
 by (REPEAT (etac conjE 1));
@@ -772,8 +772,8 @@
 (* eliminate the B-only prefix *)
 
 by (subgoal_tac "(Filter (%a.a :act A)`y1) = nil" 1);
-be ForallQFilterPnil 2;
-ba 2;
+by (etac ForallQFilterPnil 2);
+by (assume_tac 2);
 by (Fast_tac 2);
 
 (* Now real recursive step follows (in y) *)
@@ -788,8 +788,8 @@
 by (rotate_tac ~1 1);
 by (Asm_full_simp_tac  1);
 (* eliminate introduced subgoal 2 *)
-be ForallQFilterPnil 2;
-ba 2;
+by (etac ForallQFilterPnil 2);
+by (assume_tac 2);
 by (Fast_tac 2);
  
 (* bring in divide Seq for s *)
@@ -801,15 +801,15 @@
 back();
 back();
 back();
-ba 1;
+by (assume_tac 1);
 
 (* reduce trace_takes from n to strictly smaller k *)
-br take_reduction 1;
+by (rtac take_reduction 1);
 
 (* f A (tw iA) = tw ~eA *)
 by (asm_full_simp_tac (!simpset addsimps [FilterPTakewhileQid,int_is_act,
                               not_ext_is_int_or_not_act]) 1);
-br refl 1;
+by (rtac refl 1);
 by (asm_full_simp_tac (!simpset addsimps [int_is_act,
                               not_ext_is_int_or_not_act]) 1);
 by (rotate_tac ~11 1);
@@ -824,17 +824,17 @@
 (* assumption schA *)
 by (dres_inst_tac [("x","schA"),
                    ("g","Filter (%a. a:act A)`rs")] subst_lemma2 1);
-ba 1;
+by (assume_tac 1);
 by (asm_full_simp_tac (!simpset addsimps [FilterPTakewhileQnil,int_is_not_ext]) 1);
 (* assumptions concerning LastActExtsch, cannot be rewritten, as LastActExtsmalli are looping  *)
 by (dres_inst_tac [("sch","schA"),("P","%a. a:int A")] LastActExtsmall1 1);
 by (forw_inst_tac [("sch1.0","y1")]  LastActExtsmall2 1);
-ba 1;
+by (assume_tac 1);
 
 (* assumption Forall schA *)
 by (dres_inst_tac [("s","schA"),
                    ("P","Forall (%x.x:act A)")] subst 1);
-ba 1;
+by (assume_tac 1);
 by (asm_full_simp_tac (!simpset addsimps [ForallPTakewhileQ, int_is_act]) 1);
 
 (* case x:actions(asig_of A) & x: actions(asig_of B) *)
@@ -847,8 +847,8 @@
 by (rotate_tac ~1 1);
 by (Asm_full_simp_tac  1);
 (* eliminate introduced subgoal 2 *)
-be ForallQFilterPnil 2;
-ba 2;
+by (etac ForallQFilterPnil 2);
+by (assume_tac 2);
 by (Fast_tac 2);
  
 (* bring in divide Seq for s *)
@@ -860,7 +860,7 @@
 back();
 back();
 back();
-ba 1;
+by (assume_tac 1);
 
 (* f A (tw iA) = tw ~eA *)
 by (asm_full_simp_tac (!simpset addsimps [FilterPTakewhileQid,int_is_act,
@@ -876,7 +876,7 @@
 (* assumption schA *)
 by (dres_inst_tac [("x","schA"),
                    ("g","Filter (%a. a:act A)`rs")] subst_lemma2 1);
-ba 1;
+by (assume_tac 1);
 by (asm_full_simp_tac (!simpset addsimps [FilterPTakewhileQnil,int_is_not_ext]) 1);
 
 (* f A (tw iB schB2) = nil *) 
@@ -885,22 +885,22 @@
 
 
 (* reduce trace_takes from n to strictly smaller k *)
-br take_reduction 1;
-br refl 1;
-br refl 1;
+by (rtac take_reduction 1);
+by (rtac refl 1);
+by (rtac refl 1);
 
 (* now conclusion fulfills induction hypothesis, but assumptions are not all ready *)
 
 (* assumption schB *)
 by (dres_inst_tac [("x","y2"),
                    ("g","Filter (%a. a:act B)`rs")] subst_lemma2 1);
-ba 1;
+by (assume_tac 1);
 by (asm_full_simp_tac (!simpset addsimps [FilterPTakewhileQnil,intA_is_not_actB,int_is_not_ext]) 1);
 
 (* conclusions concerning LastActExtsch, cannot be rewritten, as LastActExtsmalli are looping  *)
 by (dres_inst_tac [("sch","schA"),("P","%a. a:int A")] LastActExtsmall1 1);
 by (forw_inst_tac [("sch1.0","y1")]  LastActExtsmall2 1);
-ba 1;
+by (assume_tac 1);
 by (dres_inst_tac [("sch","y2"),("P","%a. a:int B")] LastActExtsmall1 1);
 
 (* assumption Forall schA, and Forall schA are performed by ForallTL,ForallDropwhile *)
@@ -941,15 +941,15 @@
 \ --> Filter (%a.a:act B)`(mksch A B`tr`schA`schB) = schB";
 
 by (strip_tac 1);
-br seq.take_lemma 1;
-br mp 1;
-ba 2;
+by (rtac seq.take_lemma 1);
+by (rtac mp 1);
+by (assume_tac 2);
 back();back();back();back();
 by (res_inst_tac [("x","schA")] spec 1);
 by (res_inst_tac [("x","schB")] spec 1);
 by (res_inst_tac [("x","tr")] spec 1);
 by (thin_tac' 5 1);
-br less_induct 1;
+by (rtac less_induct 1);
 by (REPEAT (rtac allI 1));
 ren "tr schB schA" 1;
 by (strip_tac 1);
@@ -957,7 +957,7 @@
 
 by (case_tac "Forall (%x. x:act A & x~:act B) tr" 1);
 
-br (seq_take_lemma RS iffD2 RS spec) 1;
+by (rtac (seq_take_lemma RS iffD2 RS spec) 1);
 by (thin_tac' 5 1);
 
 
@@ -973,7 +973,7 @@
 by (eres_inst_tac [("A","B")] LastActExtimplnil 1);
 by (Asm_simp_tac 1);
 by (eres_inst_tac [("Q","%x.x:act A & x~:act B")] ForallQFilterPnil 1);
-ba 1;
+by (assume_tac 1);
 by (Fast_tac 1);
 
 (* case ~ Finite tr *)
@@ -990,12 +990,12 @@
 by (eres_inst_tac [("A","B")] LastActExtimplUU 1);
 by (Asm_simp_tac 1);
 by (eres_inst_tac [("Q","%x.x:act A & x~:act B")] ForallQFilterPUU 1);
-ba 1;
+by (assume_tac 1);
 by (Fast_tac 1);
 
 (* case" ~ Forall (%x.x:act B & x~:act A) s" *)
 
-bd divide_Seq3 1;
+by (dtac divide_Seq3 1);
 
 by (REPEAT (etac exE 1));
 by (REPEAT (etac conjE 1));
@@ -1014,8 +1014,8 @@
 (* eliminate the A-only prefix *)
 
 by (subgoal_tac "(Filter (%a.a :act B)`x1) = nil" 1);
-be ForallQFilterPnil 2;
-ba 2;
+by (etac ForallQFilterPnil 2);
+by (assume_tac 2);
 by (Fast_tac 2);
 
 (* Now real recursive step follows (in x) *)
@@ -1030,8 +1030,8 @@
 by (rotate_tac ~1 1);
 by (Asm_full_simp_tac  1);
 (* eliminate introduced subgoal 2 *)
-be ForallQFilterPnil 2;
-ba 2;
+by (etac ForallQFilterPnil 2);
+by (assume_tac 2);
 by (Fast_tac 2);
  
 (* bring in divide Seq for s *)
@@ -1043,15 +1043,15 @@
 back();
 back();
 back();
-ba 1;
+by (assume_tac 1);
 
 (* reduce trace_takes from n to strictly smaller k *)
-br take_reduction 1;
+by (rtac take_reduction 1);
 
 (* f B (tw iB) = tw ~eB *)
 by (asm_full_simp_tac (!simpset addsimps [FilterPTakewhileQid,int_is_act,
                               not_ext_is_int_or_not_act]) 1);
-br refl 1;
+by (rtac refl 1);
 by (asm_full_simp_tac (!simpset addsimps [int_is_act,
                               not_ext_is_int_or_not_act]) 1);
 by (rotate_tac ~11 1);
@@ -1066,17 +1066,17 @@
 (* assumption schB *)
 by (dres_inst_tac [("x","schB"),
                    ("g","Filter (%a. a:act B)`rs")] subst_lemma2 1);
-ba 1;
+by (assume_tac 1);
 by (asm_full_simp_tac (!simpset addsimps [FilterPTakewhileQnil,int_is_not_ext]) 1);
 (* assumptions concerning LastActExtsch, cannot be rewritten, as LastActExtsmalli are looping  *)
 by (dres_inst_tac [("sch","schB"),("P","%a. a:int B")] LastActExtsmall1 1);
 by (forw_inst_tac [("sch1.0","x1")]  LastActExtsmall2 1);
-ba 1;
+by (assume_tac 1);
 
 (* assumption Forall schB *)
 by (dres_inst_tac [("s","schB"),
                    ("P","Forall (%x.x:act B)")] subst 1);
-ba 1;
+by (assume_tac 1);
 by (asm_full_simp_tac (!simpset addsimps [ForallPTakewhileQ, int_is_act]) 1);
 
 (* case x:actions(asig_of A) & x: actions(asig_of B) *)
@@ -1089,8 +1089,8 @@
 by (rotate_tac ~1 1);
 by (Asm_full_simp_tac  1);
 (* eliminate introduced subgoal 2 *)
-be ForallQFilterPnil 2;
-ba 2;
+by (etac ForallQFilterPnil 2);
+by (assume_tac 2);
 by (Fast_tac 2);
  
 (* bring in divide Seq for s *)
@@ -1102,7 +1102,7 @@
 back();
 back();
 back();
-ba 1;
+by (assume_tac 1);
 
 (* f B (tw iB) = tw ~eB *)
 by (asm_full_simp_tac (!simpset addsimps [FilterPTakewhileQid,int_is_act,
@@ -1118,7 +1118,7 @@
 (* assumption schA *)
 by (dres_inst_tac [("x","schB"),
                    ("g","Filter (%a. a:act B)`rs")] subst_lemma2 1);
-ba 1;
+by (assume_tac 1);
 by (asm_full_simp_tac (!simpset addsimps [FilterPTakewhileQnil,int_is_not_ext]) 1);
 
 (* f B (tw iA schA2) = nil *) 
@@ -1127,22 +1127,22 @@
 
 
 (* reduce trace_takes from n to strictly smaller k *)
-br take_reduction 1;
-br refl 1;
-br refl 1;
+by (rtac take_reduction 1);
+by (rtac refl 1);
+by (rtac refl 1);
 
 (* now conclusion fulfills induction hypothesis, but assumptions are not all ready *)
 
 (* assumption schA *)
 by (dres_inst_tac [("x","x2"),
                    ("g","Filter (%a. a:act A)`rs")] subst_lemma2 1);
-ba 1;
+by (assume_tac 1);
 by (asm_full_simp_tac (!simpset addsimps [FilterPTakewhileQnil,intA_is_not_actB,int_is_not_ext]) 1);
 
 (* conclusions concerning LastActExtsch, cannot be rewritten, as LastActExtsmalli are looping  *)
 by (dres_inst_tac [("sch","schB"),("P","%a. a:int B")] LastActExtsmall1 1);
 by (forw_inst_tac [("sch1.0","x1")]  LastActExtsmall2 1);
-ba 1;
+by (assume_tac 1);
 by (dres_inst_tac [("sch","x2"),("P","%a. a:int A")] LastActExtsmall1 1);
 
 (* assumption Forall schA, and Forall schA are performed by ForallTL,ForallDropwhile *)
@@ -1192,22 +1192,22 @@
 by (asm_full_simp_tac (!simpset addsimps [compatibility_consequence2,
                   externals_of_par,ext1_ext2_is_not_act2]) 1);
 (* Traces of A||B have only external actions from A or B *)  
-br ForallPFilterP 1;
+by (rtac ForallPFilterP 1);
 
 (* <== *)
 
 (* replace schA and schB by Cut(schA) and Cut(schB) *)
 by (dtac exists_LastActExtsch 1);
-ba 1;
+by (assume_tac 1);
 by (dtac exists_LastActExtsch 1);
-ba 1;
+by (assume_tac 1);
 by (REPEAT (etac exE 1));
 by (REPEAT (etac conjE 1));
 (* Schedules of A(B) have only actions of A(B) *)
-bd scheds_in_sig 1;
-ba 1;
-bd scheds_in_sig 1;
-ba 1;
+by (dtac scheds_in_sig 1);
+by (assume_tac 1);
+by (dtac scheds_in_sig 1);
+by (assume_tac 1);
 
 ren "h1 h2 schA schB" 1;
 (* mksch is exactly the construction of trA||B out of schA, schB, and the oracle tr,
@@ -1220,9 +1220,9 @@
 (* mksch is a schedule -- use compositionality on sch-level *)
 by (asm_full_simp_tac (!simpset addsimps [compositionality_sch]) 1);
 by (asm_full_simp_tac (!simpset addsimps [FilterAmksch_is_schA,FilterBmksch_is_schB]) 1);
-be ForallAorB_mksch 1;
-be ForallPForallQ 1;
-be ext_is_act 1;
+by (etac ForallAorB_mksch 1);
+by (etac ForallPForallQ 1);
+by (etac ext_is_act 1);
 qed"compositionality_tr";
 
 
diff -r fdb1768ebd3e -r a8ab7c64817c src/HOLCF/IOA/meta_theory/Compositionality.ML
--- a/src/HOLCF/IOA/meta_theory/Compositionality.ML	Mon Jun 23 10:35:49 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/Compositionality.ML	Mon Jun 23 10:42:03 1997 +0200
@@ -9,16 +9,16 @@
 
 
 goal thy "!! A. [|eA --> A ; eB & ~eA --> ~A|] ==> (eA | eB) --> A=eA";
-auto();
+by (Auto_tac());
 qed"compatibility_consequence3";
 
 
 goal thy 
 "!! A B. [| compatible A B; Forall (%a. a: ext A | a: ext B) tr |] ==> \
 \           Filter (%a. a: act A)`tr= Filter (%a. a: ext A)`tr";
-br ForallPFilterQR 1;
-ba 2;
-br compatibility_consequence3 1;
+by (rtac ForallPFilterQR 1);
+by (assume_tac 2);
+by (rtac compatibility_consequence3 1);
 by (REPEAT (asm_full_simp_tac (!simpset 
                   addsimps [ext_is_act,ext1_ext2_is_not_act1]) 1));
 qed"Filter_actAisFilter_extA";
@@ -28,15 +28,15 @@
     or even better A||B= B||A, FIX *)
 
 goal thy "!! A. [|eA --> A ; eB & ~eA --> ~A|] ==> (eB | eA) --> A=eA";
-auto();
+by (Auto_tac());
 qed"compatibility_consequence4";
 
 goal thy 
 "!! A B. [| compatible A B; Forall (%a. a: ext B | a: ext A) tr |] ==> \
 \           Filter (%a. a: act A)`tr= Filter (%a. a: ext A)`tr";
-br ForallPFilterQR 1;
-ba 2;
-br compatibility_consequence4 1;
+by (rtac ForallPFilterQR 1);
+by (assume_tac 2);
+by (rtac compatibility_consequence4 1);
 by (REPEAT (asm_full_simp_tac (!simpset 
                   addsimps [ext_is_act,ext1_ext2_is_not_act1]) 1));
 qed"Filter_actAisFilter_extA2";
@@ -73,11 +73,11 @@
 (* 2 goals, the 3rd has been solved automatically *)
 (* 1: Filter A2 x : traces A2 *)
 by (dres_inst_tac [("A","traces A1")] subsetD 1);
-ba 1;
+by (assume_tac 1);
 by (asm_full_simp_tac (!simpset addsimps [Filter_actAisFilter_extA]) 1);
 (* 2: Filter B2 x : traces B2 *)
 by (dres_inst_tac [("A","traces B1")] subsetD 1);
-ba 1;
+by (assume_tac 1);
 by (asm_full_simp_tac (!simpset addsimps [Filter_actAisFilter_extA2]) 1);
 qed"compositionality";
 
diff -r fdb1768ebd3e -r a8ab7c64817c src/HOLCF/IOA/meta_theory/Deadlock.ML
--- a/src/HOLCF/IOA/meta_theory/Deadlock.ML	Mon Jun 23 10:35:49 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/Deadlock.ML	Mon Jun 23 10:42:03 1997 +0200
@@ -20,28 +20,28 @@
 ren "sch s ex" 1;
 by (subgoal_tac "Finite ex" 1);
 by (asm_full_simp_tac (!simpset addsimps [filter_act_def]) 2);
-br (Map2Finite RS iffD1) 2;
+by (rtac (Map2Finite RS iffD1) 2);
 by (res_inst_tac [("t","Map fst`ex")] subst 2);
-ba 2;
-be FiniteFilter 2;
+by (assume_tac 2);
+by (etac FiniteFilter 2);
 (* subgoal 1 *)
 by (forward_tac [exists_laststate] 1);
-be allE 1;
-be exE 1;
+by (etac allE 1);
+by (etac exE 1);
 (* using input-enabledness *)
 by (asm_full_simp_tac (!simpset addsimps [ioa_def,input_enabled_def]) 1);
 by (REPEAT (etac conjE 1));
 by (eres_inst_tac [("x","a")] allE 1);
 by (Asm_full_simp_tac 1);
 by (eres_inst_tac [("x","u")] allE 1);
-be exE 1;
+by (etac exE 1);
 (* instantiate execution *)
 by (res_inst_tac [("x","(s,ex @@ (a,s2)>>nil)")] exI 1);
 by (asm_full_simp_tac (!simpset addsimps [filter_act_def,MapConc]) 1);
 by (eres_inst_tac [("t","u")] lemma_2_1 1);
 by (Asm_full_simp_tac 1);
-br sym 1;
-ba 1;
+by (rtac sym 1);
+by (assume_tac 1);
 qed"scheds_input_enabled";
 
 (********************************************************************************
@@ -56,18 +56,18 @@
 \          ==> (sch @@ a>>nil) : schedules (A||B)";
 
 by (asm_full_simp_tac (!simpset addsimps [compositionality_sch,locals_def]) 1);
-br conjI 1;
+by (rtac conjI 1);
 (* a : act (A||B) *)
 by (asm_full_simp_tac (!simpset addsimps [actions_of_par]) 2);
-br disjI1 2;
-be disjE 2;
-be int_is_act 2;
-be out_is_act 2;
+by (rtac disjI1 2);
+by (etac disjE 2);
+by (etac int_is_act 2);
+by (etac out_is_act 2);
 (* Filter B (sch@@[a]) : schedules B *)
 
 by (case_tac "a:int A" 1);
-bd intA_is_not_actB 1;
-ba 1;  (* --> a~:act B *)
+by (dtac intA_is_not_actB 1);
+by (assume_tac 1);  (* --> a~:act B *)
 by (Asm_full_simp_tac 1);
 
 (* case a~:int A , i.e. a:out A *)
@@ -77,10 +77,10 @@
 by (Asm_full_simp_tac 1);
 by (subgoal_tac "a:out A" 1);
 by (Fast_tac 2);
-bd  outAactB_is_inpB 1;
-ba 1;
-ba 1;
-br scheds_input_enabled 1;
+by (dtac outAactB_is_inpB 1);
+by (assume_tac 1);
+by (assume_tac 1);
+by (rtac scheds_input_enabled 1);
 by (Asm_full_simp_tac 1);
 by (REPEAT (atac 1));
 qed"IOA_deadlock_free";
diff -r fdb1768ebd3e -r a8ab7c64817c src/HOLCF/IOA/meta_theory/RefCorrectness.ML
--- a/src/HOLCF/IOA/meta_theory/RefCorrectness.ML	Mon Jun 23 10:35:49 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/RefCorrectness.ML	Mon Jun 23 10:42:03 1997 +0200
@@ -24,9 +24,9 @@
 \                              @@ ((corresp_exC A f `xs) (snd pr)))   \
 \                        `x) ))";
 by (rtac trans 1);
-br fix_eq2 1;
-br corresp_exC_def 1;
-br beta_cfun 1;
+by (rtac fix_eq2 1);
+by (rtac corresp_exC_def 1);
+by (rtac beta_cfun 1);
 by (simp_tac (!simpset addsimps [flift1_def]) 1);
 qed"corresp_exC_unfold";
 
@@ -43,7 +43,7 @@
 goal thy "(corresp_exC A f`(at>>xs)) s = \
 \          (@cex. move A cex (f s) (fst at) (f (snd at)))  \
 \          @@ ((corresp_exC A f`xs) (snd at))";
-br trans 1;
+by (rtac trans 1);
 by (stac corresp_exC_unfold 1);
 by (asm_full_simp_tac (!simpset addsimps [Cons_def,flift1_def]) 1);
 by (Simp_tac 1);
@@ -140,7 +140,7 @@
 by (safe_tac set_cs);
 by (asm_full_simp_tac (!simpset addsimps [mk_traceConc]) 1);
 by (forward_tac [reachable.reachable_n] 1);
-ba 1;
+by (assume_tac 1);
 by (eres_inst_tac [("x","y")] allE 1);
 by (Asm_full_simp_tac 1);
 by (asm_full_simp_tac (!simpset addsimps [move_subprop4] 
@@ -165,7 +165,7 @@
 \     t = laststate (s,xs) \
 \ --> is_exec_frag A (s,xs @@ ys))";
 
-br impI 1;
+by (rtac impI 1);
 by (Seq_Finite_induct_tac 1);
 (* base_case *)
 by (fast_tac HOL_cs 1);
@@ -193,12 +193,12 @@
 by (res_inst_tac [("t","f y")]  lemma_2_1 1);
 
 (* Finite *)
-be move_subprop2 1;
+by (etac move_subprop2 1);
 by (REPEAT (atac 1));
 by (rtac conjI 1);
 
 (* is_exec_frag *)
-be  move_subprop1 1;
+by (etac move_subprop1 1);
 by (REPEAT (atac 1));
 by (rtac conjI 1);
 
@@ -207,10 +207,10 @@
 by (eres_inst_tac [("x","y")] allE 1);
 by (Asm_full_simp_tac 1);
 by (forward_tac [reachable.reachable_n] 1);
-ba 1;
+by (assume_tac 1);
 by (Asm_full_simp_tac 1);
 (* laststate *)
-be (move_subprop3 RS sym) 1;
+by (etac (move_subprop3 RS sym) 1);
 by (REPEAT (atac 1));
 qed"lemma_2";
 
diff -r fdb1768ebd3e -r a8ab7c64817c src/HOLCF/IOA/meta_theory/RefMappings.ML
--- a/src/HOLCF/IOA/meta_theory/RefMappings.ML	Mon Jun 23 10:35:49 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/RefMappings.ML	Mon Jun 23 10:42:03 1997 +0200
@@ -25,8 +25,8 @@
 by (case_tac "ex=nil" 1);
 by (Asm_simp_tac 1);
 by (Asm_simp_tac 1);
-bd (Finite_Last1 RS mp) 1;
-ba 1;
+by (dtac (Finite_Last1 RS mp) 1);
+by (assume_tac 1);
 by (def_tac 1);
 qed"laststate_cons";
 
@@ -92,7 +92,7 @@
 
 
 val prems = goal HOL.thy "(P ==> Q-->R) ==> P&Q --> R";
-  by(fast_tac (!claset addDs prems) 1);
+  by (fast_tac (!claset addDs prems) 1);
 qed "imp_conj_lemma";
 
 goal thy "!!f.[| is_weak_ref_map f C A |]\
@@ -108,7 +108,7 @@
 by (asm_full_simp_tac (!simpset addsimps [externals_def,asig_inputs_def,
 asig_outputs_def,asig_of_def,trans_of_def]) 1);
 by (safe_tac (!claset));
-by (rtac (expand_if RS ssubst) 1);
+by (stac expand_if 1);
  by (rtac conjI 1);
  by (rtac impI 1);
  by (etac disjE 1);
diff -r fdb1768ebd3e -r a8ab7c64817c src/HOLCF/IOA/meta_theory/Seq.ML
--- a/src/HOLCF/IOA/meta_theory/Seq.ML	Mon Jun 23 10:35:49 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/Seq.ML	Mon Jun 23 10:42:03 1997 +0200
@@ -48,10 +48,10 @@
 
 goal thy 
 "!!x.[|x~=UU|] ==> smap`f`(x##xs)= (f`x)##smap`f`xs"; 
-br trans 1;
+by (rtac trans 1);
 by (stac smap_unfold 1);
 by (Asm_full_simp_tac 1);
-br refl 1;
+by (rtac refl 1);
 qed"smap_cons";
 
 (* ----------------------------------------------------------- *)
@@ -76,10 +76,10 @@
 goal thy 
 "!!x.x~=UU ==> sfilter`P`(x##xs)=   \
 \             (If P`x then x##(sfilter`P`xs) else sfilter`P`xs fi)";
-br trans 1;
+by (rtac trans 1);
 by (stac sfilter_unfold 1);
 by (Asm_full_simp_tac 1);
-br refl 1;
+by (rtac refl 1);
 qed"sfilter_cons";
 
 (* ----------------------------------------------------------- *)
@@ -103,10 +103,10 @@
 
 goal thy 
 "!!x.x~=UU ==> sforall2`P`(x##xs)= ((P`x) andalso sforall2`P`xs)";
-br trans 1;
+by (rtac trans 1);
 by (stac sforall2_unfold 1);
 by (Asm_full_simp_tac 1);
-br refl 1;
+by (rtac refl 1);
 qed"sforall2_cons";
 
 
@@ -133,10 +133,10 @@
 goal thy 
 "!!x.x~=UU ==> stakewhile`P`(x##xs) =   \
 \             (If P`x then x##(stakewhile`P`xs) else nil fi)";
-br trans 1;
+by (rtac trans 1);
 by (stac stakewhile_unfold 1);
 by (Asm_full_simp_tac 1);
-br refl 1;
+by (rtac refl 1);
 qed"stakewhile_cons";
 
 (* ----------------------------------------------------------- *)
@@ -162,10 +162,10 @@
 goal thy 
 "!!x.x~=UU ==> sdropwhile`P`(x##xs) =   \
 \             (If P`x then sdropwhile`P`xs else x##xs fi)";
-br trans 1;
+by (rtac trans 1);
 by (stac sdropwhile_unfold 1);
 by (Asm_full_simp_tac 1);
-br refl 1;
+by (rtac refl 1);
 qed"sdropwhile_cons";
 
 
@@ -192,10 +192,10 @@
 
 goal thy 
 "!!x.x~=UU ==> slast`(x##xs)= (If is_nil`xs then x else slast`xs fi)";
-br trans 1;
+by (rtac trans 1);
 by (stac slast_unfold 1);
 by (Asm_full_simp_tac 1);
-br refl 1;
+by (rtac refl 1);
 qed"slast_cons";
 
 
@@ -220,7 +220,7 @@
 qed"sconc_UU";
 
 goal thy "(x##xs) @@ y=x##(xs @@ y)";
-br trans 1;
+by (rtac trans 1);
 by (stac sconc_unfold 1);
 by (Asm_full_simp_tac 1);
 by (case_tac "x=UU" 1);
@@ -250,7 +250,7 @@
 qed"sflat_UU";
 
 goal thy "sflat`(x##xs)= x@@(sflat`xs)"; 
-br trans 1;
+by (rtac trans 1);
 by (stac sflat_unfold 1);
 by (Asm_full_simp_tac 1);
 by (case_tac "x=UU" 1);
@@ -289,13 +289,13 @@
 qed"szip_UU2";
 
 goal thy "!!x.x~=UU ==> szip`(x##xs)`nil=UU";
-br trans 1;
+by (rtac trans 1);
 by (stac szip_unfold 1);
 by (REPEAT (Asm_full_simp_tac 1));
 qed"szip_cons_nil";
 
 goal thy "!!x.[| x~=UU; y~=UU|] ==> szip`(x##xs)`(y##ys) = <x,y>##szip`xs`ys";
-br trans 1;
+by (rtac trans 1);
 by (stac szip_unfold 1);
 by (REPEAT (Asm_full_simp_tac 1));
 qed"szip_cons";
@@ -320,7 +320,7 @@
  "!!x. [|x~=UU;y~=UU|]==> (x##xs=y##ys) = (x=y & xs=ys)";
 by (rtac iffI 1);
 by (etac (hd seq.injects) 1);
-auto();
+by (Auto_tac());
 qed"scons_inject_eq";
 
 goal thy "!!x. nil<<x ==> nil=x";
@@ -399,8 +399,8 @@
 (* ----------------------------------------------------  *)
 
 goal thy "Finite x --> x~=UU";
-br impI 1;
-be sfinite.induct 1;
+by (rtac impI 1);
+by (etac sfinite.induct 1);
  by (Asm_full_simp_tac 1);
 by (Asm_full_simp_tac 1);
 qed"Finite_UU_a";
@@ -412,7 +412,7 @@
 
 goal thy "Finite x --> a~=UU --> x=a##xs --> Finite xs";
 by (strip_tac 1);
-be sfinite.elim 1;
+by (etac sfinite.elim 1);
 by (fast_tac (HOL_cs addss !simpset) 1);
 by (fast_tac (HOL_cs addSDs seq.injects) 1);
 qed"Finite_cons_a";
@@ -454,8 +454,8 @@
 \  !! x s1.[|x~=UU;P(s1)|] ==> P(x##s1)\
 \  |] ==> seq_finite(s) --> P(s)";
 by (rtac seq_finite_ind_lemma 1);
-be seq.finite_ind 1;
- ba 1;
+by (etac seq.finite_ind 1);
+ by (assume_tac 1);
 by (Asm_full_simp_tac 1);
 qed"seq_finite_ind";
 
diff -r fdb1768ebd3e -r a8ab7c64817c src/HOLCF/IOA/meta_theory/Sequence.ML
--- a/src/HOLCF/IOA/meta_theory/Sequence.ML	Mon Jun 23 10:35:49 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/Sequence.ML	Mon Jun 23 10:42:03 1997 +0200
@@ -13,8 +13,8 @@
 \           ==> adm (%x. P x = Q x)";
 by (res_inst_tac [("P2","(%x.(P x --> Q x) & (Q x --> P x))")] (adm_cong RS iffD1) 1);
 by (Fast_tac 1);
-be adm_conj 1;
-ba 1;
+by (etac adm_conj 1);
+by (assume_tac 1);
 qed"adm_iff";
 
 Addsimps [adm_iff];
@@ -169,9 +169,9 @@
 \                                                  Undef => UU \
 \                                                | Def b => Def (a,b)##(Zip`xs`ys)))))";
 by (rtac trans 1);
-br fix_eq2 1;
-br Zip_def 1;
-br beta_cfun 1;
+by (rtac fix_eq2 1);
+by (rtac Zip_def 1);
+by (rtac beta_cfun 1);
 by (Simp_tac 1);
 qed"Zip_unfold";
 
@@ -198,7 +198,7 @@
 qed"Zip_cons_nil";
 
 goal thy "Zip`(x>>xs)`(y>>ys)= (x,y) >> Zip`xs`ys"; 
-br trans 1;
+by (rtac trans 1);
 by (stac Zip_unfold 1);
 by (Simp_tac 1);
 (* FIX: Why Simp_tac 2 times. Does continuity in simpflication make job sometimes not 
@@ -236,9 +236,9 @@
  \       | x##xs => (case x of Undef => UU | Def y => \
 \                   (if P y then y>>(Filter2 P`xs) else Filter2 P`xs)))";
 by (rtac trans 1);
-br fix_eq2 1;
-br Filter2_def 1;
-br beta_cfun 1;
+by (rtac fix_eq2 1);
+by (rtac Filter2_def 1);
+by (rtac beta_cfun 1);
 by (Simp_tac 1);
 
 is also possible, if then else has to be proven continuous and it would be nice if a case for 
@@ -265,9 +265,9 @@
 
 goal thy "!!P. [| x = UU ==> P; x = nil ==> P; !!a s. x = a >> s  ==> P |] ==> P";
 by (cut_inst_tac [("x","x")] Seq_exhaust 1);
-be disjE 1;
+by (etac disjE 1);
 by (Asm_full_simp_tac 1);
-be disjE 1;
+by (etac disjE 1);
 by (Asm_full_simp_tac 1);
 by (REPEAT (etac exE 1));
 by (Asm_full_simp_tac 1);
@@ -284,7 +284,7 @@
 goal thy "a>>s ~= UU";
 by (stac Cons_def2 1);
 by (resolve_tac seq.con_rews 1);
-br Def_not_UU 1;
+by (rtac Def_not_UU 1);
 qed"Cons_not_UU";
 
 
@@ -298,7 +298,7 @@
 goal thy "~a>>s << nil";
 by (stac Cons_def2 1);
 by (resolve_tac seq.rews 1);
-br Def_not_UU 1;
+by (rtac Def_not_UU 1);
 qed"Cons_not_less_nil";
 
 goal thy "a>>s ~= nil";
@@ -353,7 +353,7 @@
 section "induction";
 
 goal thy "!! P. [| adm P; P UU; P nil; !! a s. P s ==> P (a>>s)|] ==> P x";
-be seq.ind 1;
+by (etac seq.ind 1);
 by (REPEAT (atac 1));
 by (def_tac 1);
 by (asm_full_simp_tac (!simpset addsimps [Cons_def]) 1);
@@ -361,15 +361,15 @@
 
 goal thy "!! P.[|P UU;P nil; !! a s. P s ==> P(a>>s) |]  \
 \               ==> seq_finite x --> P x";
-be seq_finite_ind 1;
+by (etac seq_finite_ind 1);
 by (REPEAT (atac 1));
 by (def_tac 1);
 by (asm_full_simp_tac (!simpset addsimps [Cons_def]) 1);
 qed"Seq_FinitePartial_ind";
 
 goal thy "!! P.[| Finite x; P nil; !! a s. [| Finite s; P s|] ==> P (a>>s) |] ==> P x";
-be sfinite.induct 1;
-ba 1;
+by (etac sfinite.induct 1);
+by (assume_tac 1);
 by (def_tac 1);
 by (asm_full_simp_tac (!simpset addsimps [Cons_def]) 1);
 qed"Seq_Finite_ind"; 
@@ -442,10 +442,10 @@
 
 goal thy "Finite(x@@y) = (Finite (x::'a Seq) & Finite y)";
 by (rtac iffI 1);
-be (FiniteConc_2 RS spec RS spec RS mp) 1;
-br refl 1;
-br (FiniteConc_1 RS mp) 1;
-auto();
+by (etac (FiniteConc_2 RS spec RS spec RS mp) 1);
+by (rtac refl 1);
+by (rtac (FiniteConc_1 RS mp) 1);
+by (Auto_tac());
 qed"FiniteConc";
 
 Addsimps [FiniteConc];
@@ -461,16 +461,16 @@
 by (Seq_case_simp_tac "t" 1);
 by (Asm_full_simp_tac 1);
 (* main case *)
-auto();
+by (Auto_tac());
 by (Seq_case_simp_tac "t" 1);
 by (Asm_full_simp_tac 1);
 qed"FiniteMap2";
 
 goal thy "Finite (Map f`s) = Finite s";
-auto();
-be (FiniteMap2 RS spec RS mp) 1;
-br refl 1;
-be FiniteMap1 1;
+by (Auto_tac());
+by (etac (FiniteMap2 RS spec RS mp) 1);
+by (rtac refl 1);
+by (etac FiniteMap1 1);
 qed"Map2Finite";
 
 
@@ -492,27 +492,27 @@
 goal thy "!! (x:: 'a Seq). Finite x ==> !y. Finite (y:: 'a Seq) & x<<y --> x=y";
 by (Seq_Finite_induct_tac 1);
 by (strip_tac 1);
-be conjE 1;
-be nil_less_is_nil 1;
+by (etac conjE 1);
+by (etac nil_less_is_nil 1);
 (* main case *)
-auto();
+by (Auto_tac());
 by (Seq_case_simp_tac "y" 1);
-auto();
+by (Auto_tac());
 qed_spec_mp"Finite_flat";
 
 
 goal thy "adm(%(x:: 'a Seq).Finite x)";
-br admI 1;
+by (rtac admI 1);
 by (eres_inst_tac [("x","0")] allE 1);
 back();
-be exE 1;
+by (etac exE 1);
 by (REPEAT (etac conjE 1));
 by (res_inst_tac [("x","0")] allE 1);
-ba 1;
+by (assume_tac 1);
 by (eres_inst_tac [("x","j")] allE 1);
 by (cut_inst_tac [("x","Y 0"),("y","Y j")] Finite_flat 1);
 (* Generates a contradiction in subgoal 3 *)
-auto();
+by (Auto_tac());
 qed"adm_Finite";
 
 Addsimps [adm_Finite];
@@ -543,12 +543,12 @@
 (* FIX: should be same as nil_is_Conc2 when all nils are turned to right side !! *)
 goal thy "(nil = x @@ y) = ((x::'a Seq)= nil & y = nil)";
 by (Seq_case_simp_tac "x" 1);
-auto();
+by (Auto_tac());
 qed"nil_is_Conc";
 
 goal thy "(x @@ y = nil) = ((x::'a Seq)= nil & y = nil)";
 by (Seq_case_simp_tac "x" 1);
-auto();
+by (Auto_tac());
 qed"nil_is_Conc2";
 
 
@@ -655,14 +655,14 @@
 by (strip_tac 1); 
 by (Seq_case_simp_tac "sa" 1);
 by (Asm_full_simp_tac 1);
-auto();
+by (Auto_tac());
 qed"Forall_prefix";
  
 bind_thm ("Forall_prefixclosed",Forall_prefix RS spec RS mp RS mp);
 
 
 goal thy "!! h. [| Finite h; Forall P s; s= h @@ t |] ==> Forall P t";
-auto();
+by (Auto_tac());
 qed"Forall_postfixclosed";
 
 
@@ -715,7 +715,7 @@
 by (res_inst_tac[("x","ys")] Seq_induct 1);
 (* adm *)
 (* FIX: not admissible, search other proof!! *)
-br adm_all 1;
+by (rtac adm_all 1);
 (* base cases *)
 by (Simp_tac 1);
 by (Simp_tac 1);
@@ -741,23 +741,23 @@
 \                (Forall (%x. ~P x) ys  & ~Finite ys)";
 by (rtac conjI 1);
 by (cut_inst_tac [] (FilterUU_nFinite_lemma2 RS mp COMP rev_contrapos) 1);
-auto();
+by (Auto_tac());
 by (blast_tac (!claset addSDs [FilterUU_nFinite_lemma1]) 1);
 qed"FilternPUUForallP";
 
 
 goal thy  "!! Q P.[| Forall Q ys; Finite ys; !!x. Q x ==> ~P x|] \
 \   ==> Filter P`ys = nil";
-be ForallnPFilterPnil 1;
-be ForallPForallQ 1;
-auto();
+by (etac ForallnPFilterPnil 1);
+by (etac ForallPForallQ 1);
+by (Auto_tac());
 qed"ForallQFilterPnil";
 
 goal thy "!! Q P. [| ~Finite ys; Forall Q ys;  !!x. Q x ==> ~P x|] \
 \   ==> Filter P`ys = UU ";
-be ForallnPFilterPUU 1;
-be ForallPForallQ 1;
-auto();
+by (etac ForallnPFilterPUU 1);
+by (etac ForallPForallQ 1);
+by (Auto_tac());
 qed"ForallQFilterPUU";
 
 
@@ -773,26 +773,26 @@
 
 
 goal thy"!! P. [| !!x. Q x==> P x |] ==> Forall P (Takewhile Q`x)";
-br ForallPForallQ 1;
-br ForallPTakewhileP 1;
-auto();
+by (rtac ForallPForallQ 1);
+by (rtac ForallPTakewhileP 1);
+by (Auto_tac());
 qed"ForallPTakewhileQ";
 
 
 goal thy  "!! Q P.[| Finite (Takewhile Q`ys); !!x. Q x ==> ~P x |] \
 \   ==> Filter P`(Takewhile Q`ys) = nil";
-be ForallnPFilterPnil 1;
-br ForallPForallQ 1;
-br ForallPTakewhileP 1;
-auto();
+by (etac ForallnPFilterPnil 1);
+by (rtac ForallPForallQ 1);
+by (rtac ForallPTakewhileP 1);
+by (Auto_tac());
 qed"FilterPTakewhileQnil";
 
 goal thy "!! Q P. [| !!x. Q x ==> P x |] ==> \
 \            Filter P`(Takewhile Q`ys) = (Takewhile Q`ys)";
-br ForallPFilterPid 1;
-br ForallPForallQ 1;
-br ForallPTakewhileP 1;
-auto();
+by (rtac ForallPFilterPid 1);
+by (rtac ForallPForallQ 1);
+by (rtac ForallPTakewhileP 1);
+by (Auto_tac());
 qed"FilterPTakewhileQid";
 
 Addsimps [ForallPTakewhileP,ForallPTakewhileQ,
@@ -840,26 +840,26 @@
 (* FIX: pay attention: is only admissible with chain-finite package to be added to 
         adm test *)
 by (Seq_induct_tac "y" [] 1);
-br adm_all 1;
+by (rtac adm_all 1);
 by (Asm_full_simp_tac 1); 
 by (case_tac "P a" 1);
 by (Asm_full_simp_tac 1); 
-br impI 1;
+by (rtac impI 1);
 by (hyp_subst_tac 1);
 by (Asm_full_simp_tac 1); 
 (* ~ P a *)
 by (Asm_full_simp_tac 1); 
-br impI 1;
+by (rtac impI 1);
 by (rotate_tac ~1 1);
 by (Asm_full_simp_tac 1); 
 by (REPEAT (etac conjE 1));
-ba 1;
+by (assume_tac 1);
 qed"divide_Seq_lemma";
 
 goal thy "!! x. (x>>xs) << Filter P`y  \
 \   ==> y = ((Takewhile (%a. ~ P a)`y) @@ (x >> TL`(Dropwhile (%a.~P a)`y))) \
 \      & Finite (Takewhile (%a. ~ P a)`y)  & P x";
-br (divide_Seq_lemma RS mp) 1;
+by (rtac (divide_Seq_lemma RS mp) 1);
 by (dres_inst_tac [("fo","HD"),("xa","x>>xs")]  monofun_cfun_arg 1);
 by (Asm_full_simp_tac 1); 
 qed"divide_Seq";
@@ -869,7 +869,7 @@
 (* FIX: pay attention: is only admissible with chain-finite package to be added to 
         adm test *)
 by (Seq_induct_tac "y" [] 1);
-br adm_all 1;
+by (rtac adm_all 1);
 by (case_tac "P a" 1);
 by (Asm_full_simp_tac 1); 
 by (Asm_full_simp_tac 1); 
@@ -879,18 +879,18 @@
 goal thy "!!y. ~Forall P y  \
 \  ==> ? x. y= (Takewhile P`y @@ (x >> TL`(Dropwhile P`y))) & \
 \      Finite (Takewhile P`y) & (~ P x)";
-bd (nForall_HDFilter RS mp) 1;
+by (dtac (nForall_HDFilter RS mp) 1);
 by (safe_tac set_cs);
 by (res_inst_tac [("x","x")] exI 1);
 by (cut_inst_tac [("P1","%x. ~ P x")] (divide_Seq_lemma RS mp) 1);
-auto();
+by (Auto_tac());
 qed"divide_Seq2";
 
 
 goal thy  "!! y. ~Forall P y \
 \  ==> ? x bs rs. y= (bs @@ (x>>rs)) & Finite bs & Forall P bs & (~ P x)";
 by (cut_inst_tac [] divide_Seq2 1);
-auto();
+by (Auto_tac());
 qed"divide_Seq3";
 
 Addsimps [FilterPQ,FilterConc,Conc_cong];
@@ -903,8 +903,8 @@
 
 goal thy "(!n. seq_take n`x = seq_take n`x') = (x = x')";
 by (rtac iffI 1);
-br seq.take_lemma 1;
-auto();
+by (rtac seq.take_lemma 1);
+by (Auto_tac());
 qed"seq_take_lemma";
 
 goal thy 
@@ -913,9 +913,9 @@
 by (Seq_induct_tac "x" [] 1);
 by (strip_tac 1);
 by (res_inst_tac [("n","n")] natE 1);
-auto();
+by (Auto_tac());
 by (res_inst_tac [("n","n")] natE 1);
-auto();
+by (Auto_tac());
 qed"take_reduction1";
 
 
@@ -935,9 +935,9 @@
 by (Seq_induct_tac "x" [] 1);
 by (strip_tac 1);
 by (res_inst_tac [("n","n")] natE 1);
-auto();
+by (Auto_tac());
 by (res_inst_tac [("n","n")] natE 1);
-auto();
+by (Auto_tac());
 qed"take_reduction_less1";
 
 
@@ -953,9 +953,9 @@
 by (res_inst_tac [("t","s1")] (seq.reach RS subst)  1);
 by (res_inst_tac [("t","s2")] (seq.reach RS subst)  1);
 by (rtac (fix_def2 RS ssubst ) 1);
-by (rtac (contlub_cfun_fun RS ssubst) 1);
+by (stac contlub_cfun_fun 1);
 by (rtac is_chain_iterate 1);
-by (rtac (contlub_cfun_fun RS ssubst) 1);
+by (stac contlub_cfun_fun 1);
 by (rtac is_chain_iterate 1);
 by (rtac lub_mono 1);
 by (rtac (is_chain_iterate RS ch2ch_fappL) 1);
@@ -967,9 +967,9 @@
 
 goal thy "(!n. seq_take n`x << seq_take n`x') = (x << x')";
 by (rtac iffI 1);
-br take_lemma_less1 1;
-auto();
-be monofun_cfun_arg 1;
+by (rtac take_lemma_less1 1);
+by (Auto_tac());
+by (etac monofun_cfun_arg 1);
 qed"take_lemma_less";
 
 (* ------------------------------------------------------------------
@@ -991,8 +991,8 @@
 \              ==> A x --> (f x)=(g x)";
 by (case_tac "Forall Q x" 1);
 by (auto_tac (!claset addSDs [divide_Seq3],!simpset));
-br seq.take_lemma 1;
-auto();
+by (rtac seq.take_lemma 1);
+by (Auto_tac());
 qed"take_lemma_principle2";
 
 
@@ -1011,14 +1011,14 @@
 \                         ==>   seq_take (Suc n)`(f (s1 @@ y>>s2)) \
 \                             = seq_take (Suc n)`(g (s1 @@ y>>s2)) |] \
 \              ==> A x --> (f x)=(g x)";
-br impI 1;
-br seq.take_lemma 1;
-br mp 1;
-ba 2;
+by (rtac impI 1);
+by (rtac seq.take_lemma 1);
+by (rtac mp 1);
+by (assume_tac 2);
 by (res_inst_tac [("x","x")] spec 1);
-br nat_induct 1;
+by (rtac nat_induct 1);
 by (Simp_tac 1);
-br allI 1;
+by (rtac allI 1);
 by (case_tac "Forall Q xa" 1);
 by (SELECT_GOAL (auto_tac (!claset addSIs [seq_take_lemma RS iffD2 RS spec],
                            !simpset)) 1);
@@ -1033,13 +1033,13 @@
 \                         ==>   seq_take n`(f (s1 @@ y>>s2)) \
 \                             = seq_take n`(g (s1 @@ y>>s2)) |] \
 \              ==> A x --> (f x)=(g x)";
-br impI 1;
-br seq.take_lemma 1;
-br mp 1;
-ba 2;
+by (rtac impI 1);
+by (rtac seq.take_lemma 1);
+by (rtac mp 1);
+by (assume_tac 2);
 by (res_inst_tac [("x","x")] spec 1);
-br less_induct 1;
-br allI 1;
+by (rtac less_induct 1);
+by (rtac allI 1);
 by (case_tac "Forall Q xa" 1);
 by (SELECT_GOAL (auto_tac (!claset addSIs [seq_take_lemma RS iffD2 RS spec],
                            !simpset)) 1);
@@ -1057,14 +1057,14 @@
 \                             = seq_take n`(g (s1 @@ y>>s2) h1 h2) |] \
 \              ==> ! h1 h2. (A x h1 h2) --> (f x h1 h2)=(g x h1 h2)";
 by (strip_tac 1);
-br seq.take_lemma 1;
-br mp 1;
-ba 2;
+by (rtac seq.take_lemma 1);
+by (rtac mp 1);
+by (assume_tac 2);
 by (res_inst_tac [("x","h2a")] spec 1);
 by (res_inst_tac [("x","h1a")] spec 1);
 by (res_inst_tac [("x","x")] spec 1);
-br less_induct 1;
-br allI 1;
+by (rtac less_induct 1);
+by (rtac allI 1);
 by (case_tac "Forall Q xa" 1);
 by (SELECT_GOAL (auto_tac (!claset addSIs [seq_take_lemma RS iffD2 RS spec],
                            !simpset)) 1);
@@ -1083,15 +1083,15 @@
 
 by (res_inst_tac [("t","f x = g x"),
                   ("s","!n. seq_take n`(f x) = seq_take n`(g x)")] subst 1);
-br seq_take_lemma 1;
+by (rtac seq_take_lemma 1);
 
 wie ziehe ich n durch P, d.h. evtl. ns in P muessen umbenannt werden.....
 
 
 FIX
 
-br less_induct 1;
-br allI 1;
+by (rtac less_induct 1);
+by (rtac allI 1);
 by (case_tac "Forall Q xa" 1);
 by (SELECT_GOAL (auto_tac (!claset addSIs [seq_take_lemma RS iffD2 RS spec],
                            !simpset)) 1);
@@ -1110,14 +1110,14 @@
 \                    ==>   seq_take (Suc n)`(f (y>>s)) \
 \                        = seq_take (Suc n)`(g (y>>s)) |] \
 \              ==> A x --> (f x)=(g x)";
-br impI 1;
-br seq.take_lemma 1;
-br mp 1;
-ba 2;
+by (rtac impI 1);
+by (rtac seq.take_lemma 1);
+by (rtac mp 1);
+by (assume_tac 2);
 by (res_inst_tac [("x","x")] spec 1);
-br nat_induct 1;
+by (rtac nat_induct 1);
 by (Simp_tac 1);
-br allI 1;
+by (rtac allI 1);
 by (Seq_case_simp_tac "xa" 1);
 qed"take_lemma_in_eq_out";
 
@@ -1181,7 +1181,7 @@
 
 goal thy "Map f`(x@@y) = (Map f`x) @@ (Map f`y)";
 by (res_inst_tac [("A1","%x.True"),("x1","x")] (take_lemma_in_eq_out RS mp) 1);
-auto();
+by (Auto_tac());
 qed"MapConc_takelemma";
 
 
diff -r fdb1768ebd3e -r a8ab7c64817c src/HOLCF/IOA/meta_theory/ShortExecutions.ML
--- a/src/HOLCF/IOA/meta_theory/ShortExecutions.ML	Mon Jun 23 10:35:49 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/ShortExecutions.ML	Mon Jun 23 10:42:03 1997 +0200
@@ -47,7 +47,7 @@
 goal thy "oraclebuild P`s`(x>>t) = \
 \         (Takewhile (%a.~ P a)`s)   \
 \          @@ (x>>(oraclebuild P`(TL`(Dropwhile (%a.~ P a)`s))`t))";     
-br trans 1;
+by (rtac trans 1);
 by (stac oraclebuild_unfold 1);
 by (asm_full_simp_tac (!simpset addsimps [Cons_def]) 1);
 by (simp_tac (!simpset addsimps [Cons_def]) 1);
@@ -65,7 +65,7 @@
 \           ==> Cut P s =nil";
 by (subgoal_tac "Filter P`s = nil" 1);
 by (asm_simp_tac (!simpset addsimps [oraclebuild_nil]) 1);
-br ForallQFilterPnil 1;
+by (rtac ForallQFilterPnil 1);
 by (REPEAT (atac 1));
 qed"Cut_nil";
 
@@ -74,7 +74,7 @@
 \           ==> Cut P s =UU";
 by (subgoal_tac "Filter P`s= UU" 1);
 by (asm_simp_tac (!simpset addsimps [oraclebuild_UU]) 1);
-br ForallQFilterPUU 1;
+by (rtac ForallQFilterPUU 1);
 by (REPEAT (atac 1));
 qed"Cut_UU";
 
@@ -106,7 +106,7 @@
              ForallQFilterPUU]) 1);
 (* main case *)
 by (asm_full_simp_tac (!simpset addsimps [Cut_Cons,ForallQFilterPnil]) 1);
-auto();
+by (Auto_tac());
 qed"FilterCut";
 
 
@@ -123,8 +123,8 @@
              ForallQFilterPUU]) 1);
 (* main case *)
 by (asm_full_simp_tac (!simpset addsimps [Cut_Cons,ForallQFilterPnil]) 1);
-br take_reduction 1;
-auto();
+by (rtac take_reduction 1);
+by (Auto_tac());
 qed"Cut_idemp";
 
 
@@ -136,45 +136,45 @@
 by (Fast_tac 3);
 by (case_tac "Finite s" 1);
 by (asm_full_simp_tac (!simpset addsimps [Cut_nil]) 1); 
-br (Cut_nil RS sym) 1;
+by (rtac (Cut_nil RS sym) 1);
 by (asm_full_simp_tac (!simpset addsimps [ForallMap,o_def]) 1); 
 by (asm_full_simp_tac (!simpset addsimps [Map2Finite]) 1);
 (* csae ~ Finite s *)
 by (asm_full_simp_tac (!simpset addsimps [Cut_UU]) 1);
-br (Cut_UU RS sym) 1;
+by (rtac (Cut_UU RS sym) 1);
 by (asm_full_simp_tac (!simpset addsimps [ForallMap,o_def]) 1); 
 by (asm_full_simp_tac (!simpset addsimps [Map2Finite]) 1);
 (* main case *)
 by (asm_full_simp_tac (!simpset addsimps [Cut_Cons,MapConc,
           ForallMap,FiniteMap1,o_def]) 1);
-br take_reduction 1;
-auto();
+by (rtac take_reduction 1);
+by (Auto_tac());
 qed"MapCut";
 
 
 goal thy "~Finite s --> Cut P s << s";
 by (strip_tac 1);
-br (take_lemma_less RS iffD1) 1;
+by (rtac (take_lemma_less RS iffD1) 1);
 by (strip_tac 1);
-br mp 1;
-ba 2;
+by (rtac mp 1);
+by (assume_tac 2);
 by (thin_tac' 1 1);
 by (res_inst_tac [("x","s")] spec 1);
-br less_induct 1;
+by (rtac less_induct 1);
 by (strip_tac 1);
 ren "na n s" 1;
 by (case_tac "Forall (%x. ~ P x) s" 1);
-br (take_lemma_less RS iffD2 RS spec) 1;
+by (rtac (take_lemma_less RS iffD2 RS spec) 1);
 by (asm_full_simp_tac (!simpset addsimps [Cut_UU]) 1);
 (* main case *)
-bd divide_Seq3 1;
+by (dtac divide_Seq3 1);
 by (REPEAT (etac exE 1));
 by (REPEAT (etac conjE 1));
 by (hyp_subst_tac 1);
 by (asm_full_simp_tac (!simpset addsimps [Cut_Cons]) 1);
-br take_reduction_less 1;
+by (rtac take_reduction_less 1);
 (* auto makes also reasoning about Finiteness of parts of s ! *)
-auto();
+by (Auto_tac());
 qed_spec_mp"Cut_prefixcl_nFinite";
 
 
@@ -184,24 +184,24 @@
 goal thy "Finite s --> (? y. s = Cut P s @@ y)";
 by (strip_tac 1);
 by (rtac exI 1);
-br seq.take_lemma 1;
-br mp 1;
-ba 2;
+by (rtac seq.take_lemma 1);
+by (rtac mp 1);
+by (assume_tac 2);
 by (thin_tac' 1 1);
 by (res_inst_tac [("x","s")] spec 1);
-br less_induct 1;
+by (rtac less_induct 1);
 by (strip_tac 1);
 ren "na n s" 1;
 by (case_tac "Forall (%x. ~ P x) s" 1);
-br (seq_take_lemma RS iffD2 RS spec) 1;
+by (rtac (seq_take_lemma RS iffD2 RS spec) 1);
 by (asm_full_simp_tac (!simpset addsimps [Cut_nil]) 1);
 (* main case *)
-bd divide_Seq3 1;
+by (dtac divide_Seq3 1);
 by (REPEAT (etac exE 1));
 by (REPEAT (etac conjE 1));
 by (hyp_subst_tac 1);
 by (asm_full_simp_tac (!simpset addsimps [Cut_Cons,Conc_assoc]) 1);
-br take_reduction 1;
+by (rtac take_reduction 1);
 
 qed_spec_mp"Cut_prefixcl_Finite";
 
@@ -212,13 +212,13 @@
 goal thy "!!ex .is_exec_frag A (s,ex) ==> is_exec_frag A (s,Cut P ex)";
 by (case_tac "Finite ex" 1);
 by (cut_inst_tac [("s","ex"),("P","P")] Cut_prefixcl_Finite 1);
-ba 1;
-be exE 1;
-br exec_prefix2closed 1;
+by (assume_tac 1);
+by (etac exE 1);
+by (rtac exec_prefix2closed 1);
 by (eres_inst_tac [("s","ex"),("t","Cut P ex @@ y")] subst 1);
-ba 1;
-be exec_prefixclosed 1;
-be Cut_prefixcl_nFinite 1;
+by (assume_tac 1);
+by (etac exec_prefixclosed 1);
+by (etac Cut_prefixcl_nFinite 1);
 qed"execThruCut";
 
 
@@ -251,14 +251,14 @@
 
 by (simp_tac (!simpset addsimps [filter_act_def]) 1);
 by (subgoal_tac "Map fst`(Cut (%a.fst a: ext A) y)= Cut (%a.a:ext A) (Map fst`y)" 1);
-br (rewrite_rule [o_def] MapCut) 2;
+by (rtac (rewrite_rule [o_def] MapCut) 2);
 by (asm_full_simp_tac (!simpset addsimps [FilterCut RS sym]) 1);
 
 (* Subgoal 3: Lemma: Cut idempotent  *)
 
 by (simp_tac (!simpset addsimps [LastActExtsch_def,filter_act_def]) 1);
 by (subgoal_tac "Map fst`(Cut (%a.fst a: ext A) y)= Cut (%a.a:ext A) (Map fst`y)" 1);
-br (rewrite_rule [o_def] MapCut) 2;
+by (rtac (rewrite_rule [o_def] MapCut) 2);
 by (asm_full_simp_tac (!simpset addsimps [Cut_idemp]) 1);
 qed"exists_LastActExtsch";
 
@@ -270,19 +270,19 @@
 goalw  thy [LastActExtsch_def]
   "!! A. [| LastActExtsch A sch; Filter (%x.x:ext A)`sch = nil |] \
 \   ==> sch=nil";
-bd FilternPnilForallP 1;
-be conjE 1;
-bd Cut_nil 1;
-ba 1;
+by (dtac FilternPnilForallP 1);
+by (etac conjE 1);
+by (dtac Cut_nil 1);
+by (assume_tac 1);
 by (Asm_full_simp_tac 1);
 qed"LastActExtimplnil";
 
 goalw  thy [LastActExtsch_def]
   "!! A. [| LastActExtsch A sch; Filter (%x.x:ext A)`sch = UU |] \
 \   ==> sch=UU";
-bd FilternPUUForallP 1;
-be conjE 1;
-bd Cut_UU 1;
-ba 1;
+by (dtac FilternPUUForallP 1);
+by (etac conjE 1);
+by (dtac Cut_UU 1);
+by (assume_tac 1);
 by (Asm_full_simp_tac 1);
 qed"LastActExtimplUU";
diff -r fdb1768ebd3e -r a8ab7c64817c src/HOLCF/IOA/meta_theory/Traces.ML
--- a/src/HOLCF/IOA/meta_theory/Traces.ML	Mon Jun 23 10:35:49 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/Traces.ML	Mon Jun 23 10:42:03 1997 +0200
@@ -71,9 +71,9 @@
 \             `x) \
 \   ))";
 by (rtac trans 1);
-br fix_eq2 1;
-br is_exec_fragC_def 1;
-br beta_cfun 1;
+by (rtac fix_eq2 1);
+by (rtac is_exec_fragC_def 1);
+by (rtac beta_cfun 1);
 by (simp_tac (!simpset addsimps [flift1_def]) 1);
 qed"is_exec_fragC_unfold";
 
@@ -90,7 +90,7 @@
 goal thy "(is_exec_fragC A`(pr>>xs)) s = \
 \                        (Def ((s,pr):trans_of A) \
 \                andalso (is_exec_fragC A`xs)(snd pr))";
-br trans 1;
+by (rtac trans 1);
 by (stac is_exec_fragC_unfold 1);
 by (asm_full_simp_tac (!simpset addsimps [Cons_def,flift1_def]) 1);
 by (Simp_tac 1);
@@ -178,8 +178,8 @@
 
 by (asm_full_simp_tac (!simpset addsimps [executions_def]) 1);
 by (pair_tac "x" 1);
-br (execfrag_in_sig RS spec RS mp) 1;
-auto();
+by (rtac (execfrag_in_sig RS spec RS mp) 1);
+by (Auto_tac());
 qed"exec_in_sig";
 
 goalw thy [schedules_def,has_schedule_def]
@@ -200,7 +200,7 @@
 by (strip_tac 1);
 by (Seq_case_simp_tac "xa" 1);
 by (pair_tac "a" 1);
-auto();
+by (Auto_tac());
 qed"execfrag_prefixclosed";
 
 bind_thm ("exec_prefixclosed",conjI RS (execfrag_prefixclosed RS spec RS spec RS mp));
@@ -213,6 +213,6 @@
 by (strip_tac 1);
 by (Seq_case_simp_tac "s" 1);
 by (pair_tac "a" 1);
-auto();
+by (Auto_tac());
 qed_spec_mp"exec_prefix2closed";
 
diff -r fdb1768ebd3e -r a8ab7c64817c src/HOLCF/Lift.ML
--- a/src/HOLCF/Lift.ML	Mon Jun 23 10:35:49 1997 +0200
+++ b/src/HOLCF/Lift.ML	Mon Jun 23 10:42:03 1997 +0200
@@ -8,7 +8,7 @@
 
 (* flift1 is continuous in its argument itself*)
 goal thy "cont (lift_case UU f)"; 
-br flatdom_strict2cont 1;
+by (rtac flatdom_strict2cont 1);
 by (Simp_tac 1);
 qed"cont_flift1_arg";
 
@@ -17,7 +17,7 @@
 
 goal thy "!!f. [| !! a.cont (%y. (f y) a) |] ==> \
 \          cont (%y. lift_case UU (f y))";
-br cont2cont_CF1L_rev 1;
+by (rtac cont2cont_CF1L_rev 1);
 by (strip_tac 1);
 by (res_inst_tac [("x","y")] Lift_cases 1);
 by (Asm_simp_tac 1);
@@ -29,18 +29,18 @@
 
 goal thy "!!f. [| !! a.cont (%y. (f y) a); cont g|] ==> \
 \   cont (%y. lift_case UU (f y) (g y))";
-br cont2cont_app 1;
+by (rtac cont2cont_app 1);
 back();
 by (safe_tac set_cs);
-br cont_flift1_not_arg 1;
-auto();
-br cont_flift1_arg 1;
+by (rtac cont_flift1_not_arg 1);
+by (Auto_tac());
+by (rtac cont_flift1_arg 1);
 qed"cont_flift1_arg_and_not_arg";
 
 (* flift2 is continuous in its argument itself *)
 
 goal thy "cont (lift_case UU (%y. Def (f y)))";
-br flatdom_strict2cont 1;
+by (rtac flatdom_strict2cont 1);
 by (Simp_tac 1);
 qed"cont_flift2_arg";
 
diff -r fdb1768ebd3e -r a8ab7c64817c src/HOLCF/Lift3.ML
--- a/src/HOLCF/Lift3.ML	Mon Jun 23 10:35:49 1997 +0200
+++ b/src/HOLCF/Lift3.ML	Mon Jun 23 10:42:03 1997 +0200
@@ -71,7 +71,7 @@
 (* --------------------------------------------------------*)
 
 goal thy "(x::'a lift) << y = (x=y | x=UU)";
-br (inst_lift_po RS ssubst) 1;
+by (stac inst_lift_po 1);
 by (Simp_tac 1);
 qed"less_lift";
 
@@ -96,13 +96,13 @@
 
 goal thy
   "P(lift_case a b x) = ((x=UU --> P a) & (!y. x = Def y --> P(b y)))";
-by(lift.induct_tac "x" 1);
-by(ALLGOALS Asm_simp_tac);
+by (lift.induct_tac "x" 1);
+by (ALLGOALS Asm_simp_tac);
 qed "expand_lift_case";
 
 goal thy "(x~=UU)=(? y.x=Def y)";
-br iffI 1;
-br Lift_cases 1;
+by (rtac iffI 1);
+by (rtac Lift_cases 1);
 by (REPEAT (fast_tac (HOL_cs addSIs lift.distinct) 1));
 qed"not_Undef_is_Def";
 
@@ -126,7 +126,7 @@
 back();
 by (rtac iffI 1);
 by (asm_full_simp_tac (!simpset addsimps [inst_lift_po] ) 1);
-be (antisym_less_inverse RS conjunct1) 1;
+by (etac (antisym_less_inverse RS conjunct1) 1);
 qed"Def_inject_less_eq";
 
 goal thy "Def x << y = (Def x = y)";
@@ -146,15 +146,15 @@
 (* Two specific lemmas for the combination of LCF and HOL terms *)
 
 goal thy "!!f.[|cont g; cont f|] ==> cont(%x. ((f x)`(g x)) s)";
-br cont2cont_CF1L 1;
+by (rtac cont2cont_CF1L 1);
 by (REPEAT (resolve_tac cont_lemmas1 1));
-auto();
+by (Auto_tac());
 qed"cont_fapp_app";
 
 goal thy "!!f.[|cont g; cont f|] ==> cont(%x. ((f x)`(g x)) s t)";
-br cont2cont_CF1L 1;
-be cont_fapp_app 1;
-ba 1;
+by (rtac cont2cont_CF1L 1);
+by (etac cont_fapp_app 1);
+by (assume_tac 1);
 qed"cont_fapp_app_app";