# HG changeset patch
# User wenzelm
# Date 900236957 -7200
# Node ID 24f992a25adcc43c2b552faf67a054f648a59893
# Parent  dd4ac220b8b47ec49480d380f9568edd91c3dada
isatool expandshort;

diff -r dd4ac220b8b4 -r 24f992a25adc src/HOL/IOA/IOA.ML
--- a/src/HOL/IOA/IOA.ML	Fri Jul 10 15:24:22 1998 +0200
+++ b/src/HOL/IOA/IOA.ML	Sun Jul 12 11:49:17 1998 +0200
@@ -56,7 +56,7 @@
 "!!A. [| reachable A s; (s,a,t) : trans_of(A) |] ==> reachable A t";
   by (asm_full_simp_tac (simpset() delsimps bex_simps) 1);
   by (split_all_tac 1);
-  by (Safe_tac);
+  by Safe_tac;
   by (rename_tac "ex1 ex2 n" 1);
   by (res_inst_tac [("x","(%i. if i<n then ex1 i                    \
 \                            else (if i=n then Some a else None),    \
@@ -79,7 +79,7 @@
 \     !!s t a. [|reachable A s; P(s)|] ==> (s,a,t): trans_of(A) --> P(t) |] \
 \  ==> invariant A P";
   by (rewrite_goals_tac(reachable_def::Let_def::exec_rws));
-  by (Safe_tac);
+  by Safe_tac;
   by (rename_tac "ex1 ex2 n" 1);
   by (res_inst_tac [("Q","reachable A (ex2 n)")] conjunct1 1);
   by (Asm_full_simp_tac 1);
diff -r dd4ac220b8b4 -r 24f992a25adc src/HOL/IOA/Solve.ML
--- a/src/HOL/IOA/Solve.ML	Fri Jul 10 15:24:22 1998 +0200
+++ b/src/HOL/IOA/Solve.ML	Sun Jul 12 11:49:17 1998 +0200
@@ -15,7 +15,7 @@
 \          is_weak_pmap f C A |] ==> traces(C) <= traces(A)";
 
   by (simp_tac(simpset() addsimps [has_trace_def])1);
-  by (Safe_tac);
+  by Safe_tac;
   by (rename_tac "ex1 ex2" 1);
 
   (* choose same trace, therefore same NF *)
diff -r dd4ac220b8b4 -r 24f992a25adc src/HOL/Lex/AutoMaxChop.ML
--- a/src/HOL/Lex/AutoMaxChop.ML	Fri Jul 10 15:24:22 1998 +0200
+++ b/src/HOL/Lex/AutoMaxChop.ML	Sun Jul 12 11:49:17 1998 +0200
@@ -5,33 +5,33 @@
 *)
 
 Goal "delta A (xs@[y]) q = next A y (delta A xs q)";
-by(Simp_tac 1);
+by (Simp_tac 1);
 qed "delta_snoc";
 
 Goal
  "!q ps res. auto_split A (delta A ps q) res ps xs = \
 \            maxsplit (%ys. fin A (delta A ys q)) res ps xs";
-by(induct_tac "xs" 1);
-by(Simp_tac 1);
-by(asm_simp_tac (simpset() addsimps [delta_snoc RS sym]
+by (induct_tac "xs" 1);
+by (Simp_tac 1);
+by (asm_simp_tac (simpset() addsimps [delta_snoc RS sym]
                            delsimps [delta_append]) 1);
 qed_spec_mp "auto_split_lemma";
 
 Goalw [accepts_def]
  "auto_split A (start A) res [] xs = maxsplit (accepts A) res [] xs";
-by(stac ((read_instantiate [("s","start A")] delta_Nil) RS sym) 1);
-by(stac auto_split_lemma 1);
-by(Simp_tac 1);
+by (stac ((read_instantiate [("s","start A")] delta_Nil) RS sym) 1);
+by (stac auto_split_lemma 1);
+by (Simp_tac 1);
 qed_spec_mp "auto_split_is_maxsplit";
 
 Goal
  "is_maxsplitter (accepts A) (%xs. auto_split A (start A) ([],xs) [] xs)";
-by(simp_tac (simpset() addsimps
+by (simp_tac (simpset() addsimps
         [auto_split_is_maxsplit,is_maxsplitter_maxsplit]) 1);
 qed "is_maxsplitter_auto_split";
 
 Goalw [auto_chop_def]
  "is_maxchopper (accepts A) (auto_chop A)";
-br is_maxchopper_chop 1;
-br is_maxsplitter_auto_split 1;
+by (rtac is_maxchopper_chop 1);
+by (rtac is_maxsplitter_auto_split 1);
 qed "is_maxchopper_auto_chop";
diff -r dd4ac220b8b4 -r 24f992a25adc src/HOL/Lex/AutoProj.ML
--- a/src/HOL/Lex/AutoProj.ML	Fri Jul 10 15:24:22 1998 +0200
+++ b/src/HOL/Lex/AutoProj.ML	Sun Jul 12 11:49:17 1998 +0200
@@ -5,15 +5,15 @@
 *)
 
 Goalw [start_def] "start(q,d,f) = q";
-by(Simp_tac 1);
+by (Simp_tac 1);
 qed "start_conv";
 
 Goalw [next_def] "next(q,d,f) = d";
-by(Simp_tac 1);
+by (Simp_tac 1);
 qed "next_conv";
 
 Goalw [fin_def] "fin(q,d,f) = f";
-by(Simp_tac 1);
+by (Simp_tac 1);
 qed "fin_conv";
 
 Addsimps [start_conv,next_conv,fin_conv];
diff -r dd4ac220b8b4 -r 24f992a25adc src/HOL/Lex/Automata.ML
--- a/src/HOL/Lex/Automata.ML	Fri Jul 10 15:24:22 1998 +0200
+++ b/src/HOL/Lex/Automata.ML	Sun Jul 12 11:49:17 1998 +0200
@@ -8,35 +8,35 @@
 
 Goalw [na2da_def]
  "!Q. DA.delta (na2da A) w Q = Union(NA.delta A w `` Q)";
-by(induct_tac "w" 1);
- by(ALLGOALS Asm_simp_tac);
- by(ALLGOALS Blast_tac);
+by (induct_tac "w" 1);
+ by (ALLGOALS Asm_simp_tac);
+ by (ALLGOALS Blast_tac);
 qed_spec_mp "DA_delta_is_lift_NA_delta";
 
 Goalw [DA.accepts_def,NA.accepts_def]
   "NA.accepts A w = DA.accepts (na2da A) w";
-by(simp_tac (simpset() addsimps [DA_delta_is_lift_NA_delta]) 1);
-by(simp_tac (simpset() addsimps [na2da_def]) 1);
+by (simp_tac (simpset() addsimps [DA_delta_is_lift_NA_delta]) 1);
+by (simp_tac (simpset() addsimps [na2da_def]) 1);
 qed "NA_DA_equiv";
 
 (*** Direct equivalence of NAe and DA ***)
 
 Goalw [nae2da_def]
  "!Q. (eps A)^* ^^ (DA.delta (nae2da A) w Q) = steps A w ^^ Q";
-by(induct_tac "w" 1);
+by (induct_tac "w" 1);
  by (Simp_tac 1);
-by(asm_full_simp_tac (simpset() addsimps [step_def]) 1);
-by(Blast_tac 1);
+by (asm_full_simp_tac (simpset() addsimps [step_def]) 1);
+by (Blast_tac 1);
 qed_spec_mp "espclosure_DA_delta_is_steps";
 
 Goalw [nae2da_def]
  "fin (nae2da A) Q = (? q : (eps A)^* ^^ Q. fin A q)";
-by(Simp_tac 1);
+by (Simp_tac 1);
 val lemma = result();
 
 Goalw [NAe.accepts_def,DA.accepts_def]
   "DA.accepts (nae2da A) w = NAe.accepts A w";
-by(simp_tac (simpset() addsimps [lemma,espclosure_DA_delta_is_steps]) 1);
-by(simp_tac (simpset() addsimps [nae2da_def]) 1);
-by(Blast_tac 1);
+by (simp_tac (simpset() addsimps [lemma,espclosure_DA_delta_is_steps]) 1);
+by (simp_tac (simpset() addsimps [nae2da_def]) 1);
+by (Blast_tac 1);
 qed "NAe_DA_equiv";
diff -r dd4ac220b8b4 -r 24f992a25adc src/HOL/Lex/DA.ML
--- a/src/HOL/Lex/DA.ML	Fri Jul 10 15:24:22 1998 +0200
+++ b/src/HOL/Lex/DA.ML	Sun Jul 12 11:49:17 1998 +0200
@@ -5,27 +5,27 @@
 *)
 
 Goalw [foldl2_def] "foldl2 f [] a = a";
-by(Simp_tac 1);
+by (Simp_tac 1);
 qed "foldl2_Nil";
 
 Goalw [foldl2_def] "foldl2 f (x#xs) a = foldl2 f xs (f x a)";
-by(Simp_tac 1);
+by (Simp_tac 1);
 qed "foldl2_Cons";
 
 Addsimps [foldl2_Nil,foldl2_Cons];
 
 Goalw [delta_def] "delta A [] s = s";
-by(Simp_tac 1);
+by (Simp_tac 1);
 qed "delta_Nil";
 
 Goalw [delta_def] "delta A (a#w) s = delta A w (next A a s)";
-by(Simp_tac 1);
+by (Simp_tac 1);
 qed "delta_Cons";
 
 Addsimps [delta_Nil,delta_Cons];
 
 Goal "!q ys. delta A (xs@ys) q = delta A ys (delta A xs q)";
-by(induct_tac "xs" 1);
+by (induct_tac "xs" 1);
 by (ALLGOALS Asm_simp_tac);
 qed "delta_append";
 Addsimps [delta_append];
diff -r dd4ac220b8b4 -r 24f992a25adc src/HOL/Lex/MaxChop.ML
--- a/src/HOL/Lex/MaxChop.ML	Fri Jul 10 15:24:22 1998 +0200
+++ b/src/HOL/Lex/MaxChop.ML	Sun Jul 12 11:49:17 1998 +0200
@@ -7,12 +7,12 @@
 (* Termination of chop *)
 
 Goalw [reducing_def] "reducing(%qs. maxsplit P ([],qs) [] qs)";
-by(asm_full_simp_tac (simpset() addsimps [maxsplit_eq]) 1);
+by (asm_full_simp_tac (simpset() addsimps [maxsplit_eq]) 1);
 qed "reducing_maxsplit";
 
 val [tc] = chopr.tcs;
 goalw_cterm [reducing_def] (cterm_of (sign_of thy) (HOLogic.mk_Trueprop tc));
-by(blast_tac (claset() addDs [sym]) 1);
+by (blast_tac (claset() addDs [sym]) 1);
 val lemma = result();
 
 val chopr_rule = let val [chopr_rule] = chopr.rules in lemma RS chopr_rule end;
@@ -22,85 +22,85 @@
 \                   in if pre=[] then ([],xs) \
 \                      else let (xss,zs) = chop splitf post \
 \                             in (pre#xss,zs))";
-by(asm_simp_tac (simpset() addsimps [chopr_rule] addcongs [if_weak_cong]) 1);
-by(simp_tac (simpset() addsimps [Let_def] addsplits [split_split]) 1);
+by (asm_simp_tac (simpset() addsimps [chopr_rule] addcongs [if_weak_cong]) 1);
+by (simp_tac (simpset() addsimps [Let_def] addsplits [split_split]) 1);
 qed "chop_rule";
 
 Goalw [is_maxsplitter_def,reducing_def]
  "is_maxsplitter P splitf ==> reducing splitf";
-by(Asm_full_simp_tac 1);
+by (Asm_full_simp_tac 1);
 qed "is_maxsplitter_reducing";
 
 Goal "is_maxsplitter P splitf ==> \
 \ !yss zs. chop splitf xs = (yss,zs) --> xs = concat yss @ zs";
-by(res_inst_tac [("xs","xs")] length_induct 1);
-by(asm_simp_tac (simpset() delsplits [split_if]
+by (res_inst_tac [("xs","xs")] length_induct 1);
+by (asm_simp_tac (simpset() delsplits [split_if]
                            addsimps [chop_rule,is_maxsplitter_reducing]
                            addcongs [if_weak_cong]) 1);
-by(asm_full_simp_tac (simpset() addsimps [Let_def,is_maxsplitter_def]
+by (asm_full_simp_tac (simpset() addsimps [Let_def,is_maxsplitter_def]
                                 addsplits [split_split]) 1);
 qed_spec_mp "chop_concat";
 
 Goal "is_maxsplitter P splitf ==> \
 \ !yss zs. chop splitf xs = (yss,zs) --> (!ys : set yss. ys ~= [])";
-by(res_inst_tac [("xs","xs")] length_induct 1);
-by(asm_simp_tac (simpset() addsimps [chop_rule,is_maxsplitter_reducing]
+by (res_inst_tac [("xs","xs")] length_induct 1);
+by (asm_simp_tac (simpset() addsimps [chop_rule,is_maxsplitter_reducing]
                            addcongs [if_weak_cong]) 1);
-by(asm_full_simp_tac (simpset() addsimps [Let_def,is_maxsplitter_def]
+by (asm_full_simp_tac (simpset() addsimps [Let_def,is_maxsplitter_def]
                                 addsplits [split_split]) 1);
-by(simp_tac (simpset() addsimps [Let_def,maxsplit_eq]
+by (simp_tac (simpset() addsimps [Let_def,maxsplit_eq]
                        addsplits [split_split]) 1);
-be thin_rl 1;
-by(strip_tac 1);
-br ballI 1;
-be exE 1;
-be allE 1;
-auto();
+by (etac thin_rl 1);
+by (strip_tac 1);
+by (rtac ballI 1);
+by (etac exE 1);
+by (etac allE 1);
+by Auto_tac;
 qed_spec_mp "chop_nonempty";
 
 val [prem] = goalw thy [is_maxchopper_def]
  "is_maxsplitter P splitf ==> is_maxchopper P (chop splitf)";
-by(Clarify_tac 1);
-br iffI 1;
- br conjI 1;
-  be (prem RS chop_concat) 1;
- br conjI 1;
-  be (prem RS chop_nonempty) 1;
- be rev_mp 1;
- by(stac (prem RS is_maxsplitter_reducing RS chop_rule) 1);
- by(simp_tac (simpset() addsimps [Let_def,rewrite_rule[is_maxsplitter_def]prem]
+by (Clarify_tac 1);
+by (rtac iffI 1);
+ by (rtac conjI 1);
+  by (etac (prem RS chop_concat) 1);
+ by (rtac conjI 1);
+  by (etac (prem RS chop_nonempty) 1);
+ by (etac rev_mp 1);
+ by (stac (prem RS is_maxsplitter_reducing RS chop_rule) 1);
+ by (simp_tac (simpset() addsimps [Let_def,rewrite_rule[is_maxsplitter_def]prem]
                         addsplits [split_split]) 1);
- by(Clarify_tac 1);
- br conjI 1;
-  by(Clarify_tac 1);
-  by(Asm_full_simp_tac 1);
- by(Clarify_tac 1);
- by(Asm_full_simp_tac 1);
- by(forward_tac [prem RS chop_concat] 1);
- by(Clarify_tac 1);
- ba 1;
-by(stac (prem RS is_maxsplitter_reducing RS chop_rule) 1);
- by(simp_tac (simpset() addsimps [Let_def,rewrite_rule[is_maxsplitter_def]prem]
+ by (Clarify_tac 1);
+ by (rtac conjI 1);
+  by (Clarify_tac 1);
+  by (Asm_full_simp_tac 1);
+ by (Clarify_tac 1);
+ by (Asm_full_simp_tac 1);
+ by (forward_tac [prem RS chop_concat] 1);
+ by (Clarify_tac 1);
+ by (assume_tac 1);
+by (stac (prem RS is_maxsplitter_reducing RS chop_rule) 1);
+ by (simp_tac (simpset() addsimps [Let_def,rewrite_rule[is_maxsplitter_def]prem]
                         addsplits [split_split]) 1);
-by(Clarify_tac 1);
-br conjI 1;
- by(Clarify_tac 1);
- by(exhaust_tac "yss" 1);
-  by(Asm_simp_tac 1);
- by(Asm_full_simp_tac 1);
- by(full_simp_tac (simpset() addsimps [is_maxpref_def]) 1);
- by(blast_tac (claset() addIs [prefix_append RS iffD2]) 1);
-by(exhaust_tac "yss" 1);
- by(Asm_full_simp_tac 1);
- by(full_simp_tac (simpset() addsimps [is_maxpref_def]) 1);
- by(blast_tac (claset() addIs [prefix_append RS iffD2]) 1);
-by(Clarify_tac 1);
-by(Asm_full_simp_tac 1);
-by(subgoal_tac "x=a" 1);
- by(Clarify_tac 1);
- by(Asm_full_simp_tac 1);
-by(rotate_tac ~2 1);
-by(Asm_full_simp_tac 1);
-by(full_simp_tac (simpset() addsimps [is_maxpref_def]) 1);
-by(blast_tac (claset() addIs [prefix_append RS iffD2,prefix_antisym]) 1);
+by (Clarify_tac 1);
+by (rtac conjI 1);
+ by (Clarify_tac 1);
+ by (exhaust_tac "yss" 1);
+  by (Asm_simp_tac 1);
+ by (Asm_full_simp_tac 1);
+ by (full_simp_tac (simpset() addsimps [is_maxpref_def]) 1);
+ by (blast_tac (claset() addIs [prefix_append RS iffD2]) 1);
+by (exhaust_tac "yss" 1);
+ by (Asm_full_simp_tac 1);
+ by (full_simp_tac (simpset() addsimps [is_maxpref_def]) 1);
+ by (blast_tac (claset() addIs [prefix_append RS iffD2]) 1);
+by (Clarify_tac 1);
+by (Asm_full_simp_tac 1);
+by (subgoal_tac "x=a" 1);
+ by (Clarify_tac 1);
+ by (Asm_full_simp_tac 1);
+by (rotate_tac ~2 1);
+by (Asm_full_simp_tac 1);
+by (full_simp_tac (simpset() addsimps [is_maxpref_def]) 1);
+by (blast_tac (claset() addIs [prefix_append RS iffD2,prefix_antisym]) 1);
 qed "is_maxchopper_chop";
diff -r dd4ac220b8b4 -r 24f992a25adc src/HOL/Lex/MaxPrefix.ML
--- a/src/HOL/Lex/MaxPrefix.ML	Fri Jul 10 15:24:22 1998 +0200
+++ b/src/HOL/Lex/MaxPrefix.ML	Sun Jul 12 11:49:17 1998 +0200
@@ -9,56 +9,56 @@
 \ (maxsplit P res ps qs = (xs,ys)) = \
 \ (if ? us. us <= qs & P(ps@us) then xs@ys=ps@qs & is_maxpref P xs (ps@qs) \
 \  else (xs,ys)=res)";
-by(induct_tac "qs" 1);
- by(simp_tac (simpset() addsplits [split_if]) 1);
- by(Blast_tac 1);
-by(Asm_simp_tac 1);
-be thin_rl 1;
-by(Clarify_tac 1);
-by(case_tac "? us. us <= list & P (ps @ a # us)" 1);
- by(Asm_simp_tac 1);
- by(subgoal_tac "? us. us <= a # list & P (ps @ us)" 1);
-  by(Asm_simp_tac 1);
- by(blast_tac (claset() addIs [prefix_Cons RS iffD2]) 1);
-by(subgoal_tac "~P(ps@[a])" 1);
- by(Blast_tac 2);
-by(Asm_simp_tac 1);
-by(case_tac "? us. us <= a#list & P (ps @ us)" 1);
- by(Asm_simp_tac 1);
- by(Clarify_tac 1);
- by(exhaust_tac "us" 1);
-  br iffI 1;
-   by(asm_full_simp_tac (simpset() addsimps [prefix_Cons,prefix_append]) 1);
-   by(Blast_tac 1);
-  by(asm_full_simp_tac (simpset() addsimps [prefix_Cons,prefix_append]) 1);
-  by(Clarify_tac 1);
-  be disjE 1;
-   by(fast_tac (claset() addDs [prefix_antisym]) 1);
-  by(Clarify_tac 1);
-  be disjE 1;
-   by(Clarify_tac 1);
-   by(Asm_full_simp_tac 1);
-  be disjE 1;
-   by(Clarify_tac 1);
-   by(Asm_full_simp_tac 1);
-  by(Blast_tac 1);
- by(Asm_full_simp_tac 1);
-by(subgoal_tac "~P(ps)" 1);
-by(Asm_simp_tac 1);
-by(fast_tac (claset() addss simpset()) 1);
+by (induct_tac "qs" 1);
+ by (simp_tac (simpset() addsplits [split_if]) 1);
+ by (Blast_tac 1);
+by (Asm_simp_tac 1);
+by (etac thin_rl 1);
+by (Clarify_tac 1);
+by (case_tac "? us. us <= list & P (ps @ a # us)" 1);
+ by (Asm_simp_tac 1);
+ by (subgoal_tac "? us. us <= a # list & P (ps @ us)" 1);
+  by (Asm_simp_tac 1);
+ by (blast_tac (claset() addIs [prefix_Cons RS iffD2]) 1);
+by (subgoal_tac "~P(ps@[a])" 1);
+ by (Blast_tac 2);
+by (Asm_simp_tac 1);
+by (case_tac "? us. us <= a#list & P (ps @ us)" 1);
+ by (Asm_simp_tac 1);
+ by (Clarify_tac 1);
+ by (exhaust_tac "us" 1);
+  by (rtac iffI 1);
+   by (asm_full_simp_tac (simpset() addsimps [prefix_Cons,prefix_append]) 1);
+   by (Blast_tac 1);
+  by (asm_full_simp_tac (simpset() addsimps [prefix_Cons,prefix_append]) 1);
+  by (Clarify_tac 1);
+  by (etac disjE 1);
+   by (fast_tac (claset() addDs [prefix_antisym]) 1);
+  by (Clarify_tac 1);
+  by (etac disjE 1);
+   by (Clarify_tac 1);
+   by (Asm_full_simp_tac 1);
+  by (etac disjE 1);
+   by (Clarify_tac 1);
+   by (Asm_full_simp_tac 1);
+  by (Blast_tac 1);
+ by (Asm_full_simp_tac 1);
+by (subgoal_tac "~P(ps)" 1);
+by (Asm_simp_tac 1);
+by (fast_tac (claset() addss simpset()) 1);
 qed_spec_mp "maxsplit_lemma";
 Addsplits [split_if];
 
 Goalw [is_maxpref_def]
  "~(? us. us<=xs & P us) ==> is_maxpref P ps xs = (ps = [])";
-by(Blast_tac 1);
+by (Blast_tac 1);
 qed "is_maxpref_Nil";
 Addsimps [is_maxpref_Nil];
 
 Goalw [is_maxsplitter_def]
  "is_maxsplitter P (%xs. maxsplit P ([],xs) [] xs)";
-by(simp_tac (simpset() addsimps [maxsplit_lemma]) 1);
-by(fast_tac (claset() addss simpset()) 1);
+by (simp_tac (simpset() addsimps [maxsplit_lemma]) 1);
+by (fast_tac (claset() addss simpset()) 1);
 qed "is_maxsplitter_maxsplit";
 
 val maxsplit_eq = rewrite_rule [is_maxsplitter_def] is_maxsplitter_maxsplit;
diff -r dd4ac220b8b4 -r 24f992a25adc src/HOL/Lex/NAe.ML
--- a/src/HOL/Lex/NAe.ML	Fri Jul 10 15:24:22 1998 +0200
+++ b/src/HOL/Lex/NAe.ML	Sun Jul 12 11:49:17 1998 +0200
@@ -6,13 +6,13 @@
 
 Goal "steps A w O (eps A)^* = steps A w";
 by (exhaust_tac "w" 1);
-by(ALLGOALS(asm_simp_tac (simpset() addsimps [O_assoc])));
+by (ALLGOALS(asm_simp_tac (simpset() addsimps [O_assoc])));
 qed_spec_mp "steps_epsclosure";
 Addsimps [steps_epsclosure];
 
 Goal "[| (p,q) : (eps A)^*; (q,r) : steps A w |] ==> (p,r) : steps A w";
-by(rtac (steps_epsclosure RS equalityE) 1);
-by(Blast_tac 1);
+by (rtac (steps_epsclosure RS equalityE) 1);
+by (Blast_tac 1);
 qed "in_steps_epsclosure";
 
 Goal "(eps A)^* O steps A w = steps A w";
@@ -22,19 +22,19 @@
 qed "epsclosure_steps";
 
 Goal "[| (p,q) : steps A w; (q,r) : (eps A)^* |] ==> (p,r) : steps A w";
-by(rtac (epsclosure_steps RS equalityE) 1);
-by(Blast_tac 1);
+by (rtac (epsclosure_steps RS equalityE) 1);
+by (Blast_tac 1);
 qed "in_epsclosure_steps";
 
 Goal "steps A (v@w) = steps A w  O  steps A v";
 by (induct_tac "v" 1);
-by(ALLGOALS(asm_simp_tac (simpset() addsimps [O_assoc])));
+by (ALLGOALS(asm_simp_tac (simpset() addsimps [O_assoc])));
 qed "steps_append";
 Addsimps [steps_append];
 
 Goal "(p,r) : steps A (v@w) = ((p,r) : (steps A w O steps A v))";
-by(rtac (steps_append RS equalityE) 1);
-by(Blast_tac 1);
+by (rtac (steps_append RS equalityE) 1);
+by (Blast_tac 1);
 qed "in_steps_append";
 AddIffs [in_steps_append];
 
@@ -44,6 +44,6 @@
 by (induct_tac "w" 1);
  by (Simp_tac 1);
 by (asm_simp_tac (simpset() addsimps [comp_def,step_def]) 1);
-by(Blast_tac 1);
+by (Blast_tac 1);
 qed_spec_mp "steps_equiv_delta";
 *)
diff -r dd4ac220b8b4 -r 24f992a25adc src/HOL/Lex/Prefix.ML
--- a/src/HOL/Lex/Prefix.ML	Fri Jul 10 15:24:22 1998 +0200
+++ b/src/HOL/Lex/Prefix.ML	Sun Jul 12 11:49:17 1998 +0200
@@ -15,18 +15,18 @@
 (** <= is a partial order: **)
 
 Goalw [prefix_def] "xs <= (xs::'a list)";
-by(Simp_tac 1);
+by (Simp_tac 1);
 qed "prefix_refl";
 AddIffs[prefix_refl];
 
 Goalw [prefix_def] "!!xs::'a list. [| xs <= ys; ys <= zs |] ==> xs <= zs";
-by(Clarify_tac 1);
-by(Simp_tac 1);
+by (Clarify_tac 1);
+by (Simp_tac 1);
 qed "prefix_trans";
 
 Goalw [prefix_def] "!!xs::'a list. [| xs <= ys; ys <= xs |] ==> xs = ys";
-by(Clarify_tac 1);
-by(Asm_full_simp_tac 1);
+by (Clarify_tac 1);
+by (Asm_full_simp_tac 1);
 qed "prefix_antisym";
 
 (** recursion equations **)
@@ -44,17 +44,17 @@
 Addsimps [prefix_Nil];
 
 Goalw [prefix_def] "(xs <= ys@[y]) = (xs = ys@[y] | xs <= ys)";
-br iffI 1;
- be exE 1;
- by(rename_tac "zs" 1);
- by(res_inst_tac [("xs","zs")] rev_exhaust 1);
-  by(Asm_full_simp_tac 1);
- by(hyp_subst_tac 1);
- by(asm_full_simp_tac (simpset() delsimps [append_assoc]
+by (rtac iffI 1);
+ by (etac exE 1);
+ by (rename_tac "zs" 1);
+ by (res_inst_tac [("xs","zs")] rev_exhaust 1);
+  by (Asm_full_simp_tac 1);
+ by (hyp_subst_tac 1);
+ by (asm_full_simp_tac (simpset() delsimps [append_assoc]
                                  addsimps [append_assoc RS sym])1);
-be disjE 1;
- by(Asm_simp_tac 1);
-by(Clarify_tac 1);
+by (etac disjE 1);
+ by (Asm_simp_tac 1);
+by (Clarify_tac 1);
 by (Simp_tac 1);
 qed "prefix_snoc";
 Addsimps [prefix_snoc];
@@ -67,7 +67,7 @@
 
 Goal "(xs@ys <= xs@zs) = (ys <= zs)";
 by (induct_tac "xs" 1);
-by(ALLGOALS Asm_simp_tac);
+by (ALLGOALS Asm_simp_tac);
 qed "same_prefix_prefix";
 Addsimps [same_prefix_prefix];
 
@@ -75,7 +75,7 @@
  [simplify (simpset()) (read_instantiate [("zs","[]")] same_prefix_prefix)];
 
 Goalw [prefix_def] "xs <= ys ==> xs <= ys@zs";
-by(Clarify_tac 1);
+by (Clarify_tac 1);
 by (Simp_tac 1);
 qed "prefix_prefix";
 Addsimps [prefix_prefix];
@@ -90,11 +90,11 @@
 qed "prefix_Cons";
 
 Goal "(xs <= ys@zs) = (xs <= ys | (? us. xs = ys@us & us <= zs))";
-by(res_inst_tac [("xs","zs")] rev_induct 1);
- by(Simp_tac 1);
- by(Blast_tac 1);
-by(asm_full_simp_tac (simpset() delsimps [append_assoc]
+by (res_inst_tac [("xs","zs")] rev_induct 1);
+ by (Simp_tac 1);
+ by (Blast_tac 1);
+by (asm_full_simp_tac (simpset() delsimps [append_assoc]
                                 addsimps [append_assoc RS sym])1);
-by(Simp_tac 1);
-by(Blast_tac 1);
+by (Simp_tac 1);
+by (Blast_tac 1);
 qed "prefix_append";
diff -r dd4ac220b8b4 -r 24f992a25adc src/HOL/Lex/RegExp2NAe.ML
--- a/src/HOL/Lex/RegExp2NAe.ML	Fri Jul 10 15:24:22 1998 +0200
+++ b/src/HOL/Lex/RegExp2NAe.ML	Sun Jul 12 11:49:17 1998 +0200
@@ -9,43 +9,43 @@
 (******************************************************)
 
 Goalw [atom_def] "(fin (atom a) q) = (q = [False])";
-by(Simp_tac 1);
+by (Simp_tac 1);
 qed "fin_atom";
 
 Goalw [atom_def] "start (atom a) = [True]";
-by(Simp_tac 1);
+by (Simp_tac 1);
 qed "start_atom";
 
 (* Use {x. False} = {}? *)
 
 Goalw [atom_def,step_def]
  "eps(atom a) = {}";
-by(Simp_tac 1);
+by (Simp_tac 1);
 by (Blast_tac 1);
 qed "eps_atom";
 Addsimps [eps_atom];
 
 Goalw [atom_def,step_def]
  "(p,q) : step (atom a) (Some b) = (p=[True] & q=[False] & b=a)";
-by(Simp_tac 1);
+by (Simp_tac 1);
 qed "in_step_atom_Some";
 Addsimps [in_step_atom_Some];
 
 Goal "([False],[False]) : steps (atom a) w = (w = [])";
 by (induct_tac "w" 1);
- by(Simp_tac 1);
-by(asm_simp_tac (simpset() addsimps [comp_def]) 1);
+ by (Simp_tac 1);
+by (asm_simp_tac (simpset() addsimps [comp_def]) 1);
 qed "False_False_in_steps_atom";
 
 Goal "(start (atom a), [False]) : steps (atom a) w = (w = [a])";
 by (induct_tac "w" 1);
- by(asm_simp_tac (simpset() addsimps [start_atom,rtrancl_empty]) 1);
-by(asm_full_simp_tac (simpset()
+ by (asm_simp_tac (simpset() addsimps [start_atom,rtrancl_empty]) 1);
+by (asm_full_simp_tac (simpset()
      addsimps [False_False_in_steps_atom,comp_def,start_atom]) 1);
 qed "start_fin_in_steps_atom";
 
 Goal "accepts (atom a) w = (w = [a])";
-by(simp_tac(simpset() addsimps
+by (simp_tac(simpset() addsimps
        [accepts_def,start_fin_in_steps_atom,fin_atom]) 1);
 qed "accepts_atom";
 
@@ -73,13 +73,13 @@
 Goalw [union_def,step_def]
 "!L R. (True#p,q) : step (union L R) a = (? r. q = True#r & (p,r) : step L a)";
 by (Simp_tac 1);
-by(Blast_tac 1);
+by (Blast_tac 1);
 qed_spec_mp "True_in_step_union";
 
 Goalw [union_def,step_def]
 "!L R. (False#p,q) : step (union L R) a = (? r. q = False#r & (p,r) : step R a)";
 by (Simp_tac 1);
-by(Blast_tac 1);
+by (Blast_tac 1);
 qed_spec_mp "False_in_step_union";
 
 AddIffs [True_in_step_union,False_in_step_union];
@@ -89,45 +89,45 @@
 Goal
  "(tp,tq) : (eps(union L R))^* ==> \
 \ !p. tp = True#p --> (? q. (p,q) : (eps L)^* & tq = True#q)";
-be rtrancl_induct 1;
- by(Blast_tac 1);
-by(Clarify_tac 1);
-by(Asm_full_simp_tac 1);
-by(blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
+by (etac rtrancl_induct 1);
+ by (Blast_tac 1);
+by (Clarify_tac 1);
+by (Asm_full_simp_tac 1);
+by (blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
 val lemma1a = result();
 
 Goal
  "(tp,tq) : (eps(union L R))^* ==> \
 \ !p. tp = False#p --> (? q. (p,q) : (eps R)^* & tq = False#q)";
-be rtrancl_induct 1;
- by(Blast_tac 1);
-by(Clarify_tac 1);
-by(Asm_full_simp_tac 1);
-by(blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
+by (etac rtrancl_induct 1);
+ by (Blast_tac 1);
+by (Clarify_tac 1);
+by (Asm_full_simp_tac 1);
+by (blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
 val lemma1b = result();
 
 Goal
  "(p,q) : (eps L)^*  ==> (True#p, True#q) : (eps(union L R))^*";
-be rtrancl_induct 1;
- by(Blast_tac 1);
-by(blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
+by (etac rtrancl_induct 1);
+ by (Blast_tac 1);
+by (blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
 val lemma2a = result();
 
 Goal
  "(p,q) : (eps R)^*  ==> (False#p, False#q) : (eps(union L R))^*";
-be rtrancl_induct 1;
- by(Blast_tac 1);
-by(blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
+by (etac rtrancl_induct 1);
+ by (Blast_tac 1);
+by (blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
 val lemma2b = result();
 
 Goal
  "(True#p,q) : (eps(union L R))^* = (? r. q = True#r & (p,r) : (eps L)^*)";
-by(blast_tac (claset() addDs [lemma1a,lemma2a]) 1);
+by (blast_tac (claset() addDs [lemma1a,lemma2a]) 1);
 qed "True_epsclosure_union";
 
 Goal
  "(False#p,q) : (eps(union L R))^* = (? r. q = False#r & (p,r) : (eps R)^*)";
-by(blast_tac (claset() addDs [lemma1b,lemma2b]) 1);
+by (blast_tac (claset() addDs [lemma1b,lemma2b]) 1);
 qed "False_epsclosure_union";
 
 AddIffs [True_epsclosure_union,False_epsclosure_union];
@@ -139,7 +139,7 @@
 by (induct_tac "w" 1);
 by (ALLGOALS Asm_simp_tac);
 (* Blast_tac produces PROOF FAILED for depth 8 *)
-by(Fast_tac 1);
+by (Fast_tac 1);
 qed_spec_mp "lift_True_over_steps_union";
 
 Goal 
@@ -147,7 +147,7 @@
 by (induct_tac "w" 1);
 by (ALLGOALS Asm_simp_tac);
 (* Blast_tac produces PROOF FAILED for depth 8 *)
-by(Fast_tac 1);
+by (Fast_tac 1);
 qed_spec_mp "lift_False_over_steps_union";
 
 AddIffs [lift_True_over_steps_union,lift_False_over_steps_union];
@@ -157,19 +157,19 @@
 
 Goal
  "R^* = id Un (R^* O R)";
-by(rtac set_ext 1);
-by(split_all_tac 1);
-by(rtac iffI 1);
- be rtrancl_induct 1;
-  by(Blast_tac 1);
- by(blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
-by(blast_tac (claset() addIs [rtrancl_into_rtrancl2]) 1);
+by (rtac set_ext 1);
+by (split_all_tac 1);
+by (rtac iffI 1);
+ by (etac rtrancl_induct 1);
+  by (Blast_tac 1);
+ by (blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
+by (blast_tac (claset() addIs [rtrancl_into_rtrancl2]) 1);
 qed "unfold_rtrancl2";
 
 Goal
  "(p,q) : R^* = (q = p | (? r. (p,r) : R & (r,q) : R^*))";
-by(rtac (unfold_rtrancl2 RS equalityE) 1);
-by(Blast_tac 1);
+by (rtac (unfold_rtrancl2 RS equalityE) 1);
+by (Blast_tac 1);
 qed "in_unfold_rtrancl2";
 
 val epsclosure_start_step_union =
@@ -179,13 +179,13 @@
 Goalw [union_def,step_def]
  "!L R. (start(union L R),q) : eps(union L R) = \
 \       (q = True#start L | q = False#start R)";
-by(Simp_tac 1);
+by (Simp_tac 1);
 qed_spec_mp "start_eps_union";
 AddIffs [start_eps_union];
 
 Goalw [union_def,step_def]
  "!L R. (start(union L R),q) ~: step (union L R) (Some a)";
-by(Simp_tac 1);
+by (Simp_tac 1);
 qed_spec_mp "not_start_step_union_Some";
 AddIffs [not_start_step_union_Some];
 
@@ -197,54 +197,54 @@
 by (exhaust_tac "w" 1);
  by (Asm_simp_tac 1);
  (* Blast_tac produces PROOF FAILED! *)
- by(Fast_tac 1);
+ by (Fast_tac 1);
 by (Asm_simp_tac 1);
 (* The goal is now completely dual to the first one.
    Fast/Best_tac don't return. Blast_tac produces PROOF FAILED!
    The lemmas used in the explicit proof are part of the claset already!
 *)
-br iffI 1;
- by(Blast_tac 1);
-by(Clarify_tac 1);
-be disjE 1;
- by(Blast_tac 1);
-by(Clarify_tac 1);
-br compI 1;
-br compI 1;
-br (epsclosure_start_step_union RS iffD2) 1;
-br disjI2 1;
-br exI 1;
-br conjI 1;
-br (start_eps_union RS iffD2) 1;
-br disjI2 1;
-br refl 1;
-by(Clarify_tac 1);
-br exI 1;
-br conjI 1;
-br refl 1;
-ba 1;
-by(Clarify_tac 1);
-br exI 1;
-br conjI 1;
-br refl 1;
-ba 1;
-by(Clarify_tac 1);
-br exI 1;
-br conjI 1;
-br refl 1;
-ba 1;
+by (rtac iffI 1);
+ by (Blast_tac 1);
+by (Clarify_tac 1);
+by (etac disjE 1);
+ by (Blast_tac 1);
+by (Clarify_tac 1);
+by (rtac compI 1);
+by (rtac compI 1);
+by (rtac (epsclosure_start_step_union RS iffD2) 1);
+by (rtac disjI2 1);
+by (rtac exI 1);
+by (rtac conjI 1);
+by (rtac (start_eps_union RS iffD2) 1);
+by (rtac disjI2 1);
+by (rtac refl 1);
+by (Clarify_tac 1);
+by (rtac exI 1);
+by (rtac conjI 1);
+by (rtac refl 1);
+by (assume_tac 1);
+by (Clarify_tac 1);
+by (rtac exI 1);
+by (rtac conjI 1);
+by (rtac refl 1);
+by (assume_tac 1);
+by (Clarify_tac 1);
+by (rtac exI 1);
+by (rtac conjI 1);
+by (rtac refl 1);
+by (assume_tac 1);
 qed "steps_union";
 
 Goalw [union_def]
  "!L R. ~ fin (union L R) (start(union L R))";
-by(Simp_tac 1);
+by (Simp_tac 1);
 qed_spec_mp "start_union_not_final";
 AddIffs [start_union_not_final];
 
 Goalw [accepts_def]
  "accepts (union L R) w = (accepts L w | accepts R w)";
 by (simp_tac (simpset() addsimps [steps_union]) 1);
-auto();
+by Auto_tac;
 qed "accepts_union";
 
 
@@ -273,14 +273,14 @@
 \       ((? r. q=True#r & (p,r): step L a) | \
 \        (fin L p & a=None & q=False#start R))";
 by (Simp_tac 1);
-by(Blast_tac 1);
+by (Blast_tac 1);
 qed_spec_mp "True_step_conc";
 
 Goalw [conc_def,step_def]
  "!L R. (False#p,q) : step (conc L R) a = \
 \       (? r. q = False#r & (p,r) : step R a)";
 by (Simp_tac 1);
-by(Blast_tac 1);
+by (Blast_tac 1);
 qed_spec_mp "False_step_conc";
 
 AddIffs [True_step_conc, False_step_conc];
@@ -290,24 +290,24 @@
 Goal
  "(tp,tq) : (eps(conc L R))^* ==> \
 \ !p. tp = False#p --> (? q. (p,q) : (eps R)^* & tq = False#q)";
-by(etac rtrancl_induct 1);
- by(Blast_tac 1);
-by(blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
+by (etac rtrancl_induct 1);
+ by (Blast_tac 1);
+by (blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
 qed "lemma1b";
 
 Goal
  "(p,q) : (eps R)^* ==> (False#p, False#q) : (eps(conc L R))^*";
-by(etac rtrancl_induct 1);
- by(Blast_tac 1);
-by(blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
+by (etac rtrancl_induct 1);
+ by (Blast_tac 1);
+by (blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
 val lemma2b = result();
 
 Goal
  "((False # p, q) : (eps (conc L R))^*) = \
 \ (? r. q = False # r & (p, r) : (eps R)^*)";
 by (rtac iffI 1);
- by(blast_tac (claset() addDs [lemma1b]) 1);
-by(blast_tac (claset() addDs [lemma2b]) 1);
+ by (blast_tac (claset() addDs [lemma1b]) 1);
+by (blast_tac (claset() addDs [lemma2b]) 1);
 qed "False_epsclosure_conc";
 AddIffs [False_epsclosure_conc];
 
@@ -319,7 +319,7 @@
  by (Simp_tac 1);
 by (Simp_tac 1);
 (* Blast_tac produces PROOF FAILED for depth 8 *)
-by(Fast_tac 1);
+by (Fast_tac 1);
 qed_spec_mp "False_steps_conc";
 AddIffs [False_steps_conc];
 
@@ -327,17 +327,17 @@
 
 Goal
  "(p,q): (eps L)^* ==> (True#p,True#q) : (eps(conc L R))^*";
-be rtrancl_induct 1;
- by(Blast_tac 1);
-by(blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
+by (etac rtrancl_induct 1);
+ by (Blast_tac 1);
+by (blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
 qed "True_True_eps_concI";
 
 Goal
  "!p. (p,q) : steps L w --> (True#p,True#q) : steps (conc L R) w";
-by(induct_tac "w" 1);
+by (induct_tac "w" 1);
  by (simp_tac (simpset() addsimps [True_True_eps_concI]) 1);
 by (Simp_tac 1);
-by(blast_tac (claset() addIs [True_True_eps_concI]) 1);
+by (blast_tac (claset() addIs [True_True_eps_concI]) 1);
 qed_spec_mp "True_True_steps_concI";
 
 Goal
@@ -345,36 +345,36 @@
 \ !p. tp = True#p --> \
 \ (? q. tq = True#q & (p,q) : (eps L)^*) | \
 \ (? q r. tq = False#q & (p,r):(eps L)^* & fin L r & (start R,q) : (eps R)^*)";
-by(etac rtrancl_induct 1);
- by(Blast_tac 1);
-by(blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
+by (etac rtrancl_induct 1);
+ by (Blast_tac 1);
+by (blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
 val lemma1a = result();
 
 Goal
  "(p, q) : (eps L)^* ==> (True#p, True#q) : (eps(conc L R))^*";
-by(etac rtrancl_induct 1);
- by(Blast_tac 1);
-by(blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
+by (etac rtrancl_induct 1);
+ by (Blast_tac 1);
+by (blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
 val lemma2a = result();
 
 Goalw [conc_def,step_def]
  "!!L R. (p,q) : step R None ==> (False#p, False#q) : step (conc L R) None";
-by(split_all_tac 1);
+by (split_all_tac 1);
 by (Asm_full_simp_tac 1);
 val lemma = result();
 
 Goal
  "(p,q) : (eps R)^* ==> (False#p, False#q) : (eps(conc L R))^*";
-by(etac rtrancl_induct 1);
- by(Blast_tac 1);
+by (etac rtrancl_induct 1);
+ by (Blast_tac 1);
 by (dtac lemma 1);
-by(blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
+by (blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
 val lemma2b = result();
 
 Goalw [conc_def,step_def]
  "!!L R. fin L p ==> (True#p, False#start R) : eps(conc L R)";
-by(split_all_tac 1);
-by(Asm_full_simp_tac 1);
+by (split_all_tac 1);
+by (Asm_full_simp_tac 1);
 qed "True_False_eps_concI";
 
 Goal
@@ -382,16 +382,16 @@
 \ ((? r. (p,r) : (eps L)^* & q = True#r) | \
 \  (? r. (p,r) : (eps L)^* & fin L r & \
 \        (? s. (start R, s) : (eps R)^* & q = False#s)))";
-by(rtac iffI 1);
- by(blast_tac (claset() addDs [lemma1a]) 1);
-be disjE 1;
- by(blast_tac (claset() addIs [lemma2a]) 1);
-by(Clarify_tac 1);
-br (rtrancl_trans) 1;
-be lemma2a 1;
-br (rtrancl_into_rtrancl2) 1;
-be True_False_eps_concI 1;
-be lemma2b 1;
+by (rtac iffI 1);
+ by (blast_tac (claset() addDs [lemma1a]) 1);
+by (etac disjE 1);
+ by (blast_tac (claset() addIs [lemma2a]) 1);
+by (Clarify_tac 1);
+by (rtac (rtrancl_trans) 1);
+by (etac lemma2a 1);
+by (rtac (rtrancl_into_rtrancl2) 1);
+by (etac True_False_eps_concI 1);
+by (etac lemma2b 1);
 qed "True_epsclosure_conc";
 AddIffs [True_epsclosure_conc];
 
@@ -402,29 +402,29 @@
 \     ((? r. (p,r) : steps L w & q = True#r)  | \
 \      (? u v. w = u@v & (? r. (p,r) : steps L u & fin L r & \
 \              (? s. (start R,s) : steps R v & q = False#s))))";
-by(induct_tac "w" 1);
- by(Simp_tac 1);
-by(Simp_tac 1);
-by(clarify_tac (claset() delrules [disjCI]) 1);
- be disjE 1;
- by(clarify_tac (claset() delrules [disjCI]) 1);
- be disjE 1;
-  by(clarify_tac (claset() delrules [disjCI]) 1);
-  by(etac allE 1 THEN mp_tac 1);
-  be disjE 1;
+by (induct_tac "w" 1);
+ by (Simp_tac 1);
+by (Simp_tac 1);
+by (clarify_tac (claset() delrules [disjCI]) 1);
+ by (etac disjE 1);
+ by (clarify_tac (claset() delrules [disjCI]) 1);
+ by (etac disjE 1);
+  by (clarify_tac (claset() delrules [disjCI]) 1);
+  by (etac allE 1 THEN mp_tac 1);
+  by (etac disjE 1);
    by (Blast_tac 1);
-  br disjI2 1;
+  by (rtac disjI2 1);
   by (Clarify_tac 1);
-  by(Simp_tac 1);
-  by(res_inst_tac[("x","a#u")] exI 1);
-  by(Simp_tac 1);
+  by (Simp_tac 1);
+  by (res_inst_tac[("x","a#u")] exI 1);
+  by (Simp_tac 1);
   by (Blast_tac 1);
  by (Blast_tac 1);
-br disjI2 1;
+by (rtac disjI2 1);
 by (Clarify_tac 1);
-by(Simp_tac 1);
-by(res_inst_tac[("x","[]")] exI 1);
-by(Simp_tac 1);
+by (Simp_tac 1);
+by (res_inst_tac[("x","[]")] exI 1);
+by (Simp_tac 1);
 by (Blast_tac 1);
 qed_spec_mp "True_steps_concD";
 
@@ -433,7 +433,7 @@
 \ ((? r. (p,r) : steps L w & q = True#r)  | \
 \  (? u v. w = u@v & (? r. (p,r) : steps L u & fin L r & \
 \          (? s. (start R,s) : steps R v & q = False#s))))";
-by(blast_tac (claset() addDs [True_steps_concD]
+by (blast_tac (claset() addDs [True_steps_concD]
      addIs [True_True_steps_concI,in_steps_epsclosure,r_into_rtrancl]) 1);
 qed "True_steps_conc";
 
@@ -441,7 +441,7 @@
 
 Goalw [conc_def]
   "!L R. start(conc L R) = True#start L";
-by(Simp_tac 1);
+by (Simp_tac 1);
 qed_spec_mp "start_conc";
 
 Goalw [conc_def]
@@ -453,7 +453,7 @@
  "accepts (conc L R) w = (? u v. w = u@v & accepts L u & accepts R v)";
 by (simp_tac (simpset() addsimps
      [accepts_def,True_steps_conc,final_conc,start_conc]) 1);
-by(Blast_tac 1);
+by (Blast_tac 1);
 qed "accepts_conc";
 
 (******************************************************)
@@ -463,26 +463,26 @@
 Goalw [star_def,step_def]
  "!A. (True#p,q) : eps(star A) = \
 \     ( (? r. q = True#r & (p,r) : eps A) | (fin A p & q = True#start A) )";
-by(Simp_tac 1);
-by(Blast_tac 1);
+by (Simp_tac 1);
+by (Blast_tac 1);
 qed_spec_mp "True_in_eps_star";
 AddIffs [True_in_eps_star];
 
 Goalw [star_def,step_def]
   "!A. (p,q) : step A a --> (True#p, True#q) : step (star A) a";
-by(Simp_tac 1);
+by (Simp_tac 1);
 qed_spec_mp "True_True_step_starI";
 
 Goal
   "(p,r) : (eps A)^* ==> (True#p, True#r) : (eps(star A))^*";
-be rtrancl_induct 1;
- by(Blast_tac 1);
-by(blast_tac (claset() addIs [True_True_step_starI,rtrancl_into_rtrancl]) 1);
+by (etac rtrancl_induct 1);
+ by (Blast_tac 1);
+by (blast_tac (claset() addIs [True_True_step_starI,rtrancl_into_rtrancl]) 1);
 qed_spec_mp "True_True_eps_starI";
 
 Goalw [star_def,step_def]
  "!A. fin A p --> (True#p,True#start A) : eps(star A)";
-by(Simp_tac 1);
+by (Simp_tac 1);
 qed_spec_mp "True_start_eps_starI";
 
 Goal
@@ -490,11 +490,11 @@
 \ (? r. ((p,r) : (eps A)^* | \
 \        (? q. (p,q) : (eps A)^* & fin A q & (start A,r) : (eps A)^*)) & \
 \       s = True#r))";
-be rtrancl_induct 1;
- by(Simp_tac 1);
+by (etac rtrancl_induct 1);
+ by (Simp_tac 1);
 by (Clarify_tac 1);
 by (Asm_full_simp_tac 1);
-by(blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
+by (blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
 val lemma = result();
 
 Goal
@@ -502,20 +502,20 @@
 \ (? r. ((p,r) : (eps A)^* | \
 \        (? q. (p,q) : (eps A)^* & fin A q & (start A,r) : (eps A)^*)) & \
 \       s = True#r)";
-br iffI 1;
- bd lemma 1;
- by(Blast_tac 1);
+by (rtac iffI 1);
+ by (dtac lemma 1);
+ by (Blast_tac 1);
 (* Why can't blast_tac do the rest? *)
 by (Clarify_tac 1);
-be disjE 1;
-be True_True_eps_starI 1;
+by (etac disjE 1);
+by (etac True_True_eps_starI 1);
 by (Clarify_tac 1);
-br rtrancl_trans 1;
-be True_True_eps_starI 1;
-br rtrancl_trans 1;
-br r_into_rtrancl 1;
-be True_start_eps_starI 1;
-be True_True_eps_starI 1;
+by (rtac rtrancl_trans 1);
+by (etac True_True_eps_starI 1);
+by (rtac rtrancl_trans 1);
+by (rtac r_into_rtrancl 1);
+by (etac True_start_eps_starI 1);
+by (etac True_True_eps_starI 1);
 qed "True_eps_star";
 AddIffs [True_eps_star];
 
@@ -524,8 +524,8 @@
 Goalw [star_def,step_def]
  "!A. (True#p,r): step (star A) (Some a) = \
 \     (? q. (p,q): step A (Some a) & r=True#q)";
-by(Simp_tac 1);
-by(Blast_tac 1);
+by (Simp_tac 1);
+by (Blast_tac 1);
 qed_spec_mp "True_step_star";
 AddIffs [True_step_star];
 
@@ -538,44 +538,44 @@
 \ (? us v. w = concat us @ v & \
 \             (!u:set us. accepts A u) & \
 \             (? r. (start A,r) : steps A v & rr = True#r))";
-by(res_inst_tac [("xs","w")] rev_induct 1);
+by (res_inst_tac [("xs","w")] rev_induct 1);
  by (Asm_full_simp_tac 1);
  by (Clarify_tac 1);
- by(res_inst_tac [("x","[]")] exI 1);
- be disjE 1;
+ by (res_inst_tac [("x","[]")] exI 1);
+ by (etac disjE 1);
   by (Asm_simp_tac 1);
  by (Clarify_tac 1);
  by (Asm_simp_tac 1);
-by(simp_tac (simpset() addsimps [O_assoc,epsclosure_steps]) 1);
+by (simp_tac (simpset() addsimps [O_assoc,epsclosure_steps]) 1);
 by (Clarify_tac 1);
-by(etac allE 1 THEN mp_tac 1);
+by (etac allE 1 THEN mp_tac 1);
 by (Clarify_tac 1);
-be disjE 1;
- by(res_inst_tac [("x","us")] exI 1);
- by(res_inst_tac [("x","v@[x]")] exI 1);
- by(asm_simp_tac (simpset() addsimps [O_assoc,epsclosure_steps]) 1);
- by(Blast_tac 1);
+by (etac disjE 1);
+ by (res_inst_tac [("x","us")] exI 1);
+ by (res_inst_tac [("x","v@[x]")] exI 1);
+ by (asm_simp_tac (simpset() addsimps [O_assoc,epsclosure_steps]) 1);
+ by (Blast_tac 1);
 by (Clarify_tac 1);
-by(res_inst_tac [("x","us@[v@[x]]")] exI 1);
-by(res_inst_tac [("x","[]")] exI 1);
-by(asm_full_simp_tac (simpset() addsimps [accepts_def]) 1);
-by(Blast_tac 1);
+by (res_inst_tac [("x","us@[v@[x]]")] exI 1);
+by (res_inst_tac [("x","[]")] exI 1);
+by (asm_full_simp_tac (simpset() addsimps [accepts_def]) 1);
+by (Blast_tac 1);
 qed_spec_mp "True_start_steps_starD";
 
 Goal "!p. (p,q) : steps A w --> (True#p,True#q) : steps (star A) w";
-by(induct_tac "w" 1);
- by(Simp_tac 1);
-by(Simp_tac 1);
-by(blast_tac (claset() addIs [True_True_eps_starI,True_True_step_starI]) 1);
+by (induct_tac "w" 1);
+ by (Simp_tac 1);
+by (Simp_tac 1);
+by (blast_tac (claset() addIs [True_True_eps_starI,True_True_step_starI]) 1);
 qed_spec_mp "True_True_steps_starI";
 
 Goalw [accepts_def]
  "(!u : set us. accepts A u) --> \
 \ (True#start A,True#start A) : steps (star A) (concat us)";
-by(induct_tac "us" 1);
- by(Simp_tac 1);
-by(Simp_tac 1);
-by(blast_tac (claset() addIs [True_True_steps_starI,True_start_eps_starI,r_into_rtrancl,in_epsclosure_steps]) 1);
+by (induct_tac "us" 1);
+ by (Simp_tac 1);
+by (Simp_tac 1);
+by (blast_tac (claset() addIs [True_True_steps_starI,True_start_eps_starI,r_into_rtrancl,in_epsclosure_steps]) 1);
 qed_spec_mp "steps_star_cycle";
 
 (* Better stated directly with start(star A)? Loop in star A back to start(star A)?*)
@@ -584,18 +584,18 @@
 \ (? us v. w = concat us @ v & \
 \             (!u:set us. accepts A u) & \
 \             (? r. (start A,r) : steps A v & rr = True#r))";
-br iffI 1;
- be True_start_steps_starD 1;
+by (rtac iffI 1);
+ by (etac True_start_steps_starD 1);
 by (Clarify_tac 1);
-by(Asm_simp_tac 1);
-by(blast_tac (claset() addIs [True_True_steps_starI,steps_star_cycle]) 1);
+by (Asm_simp_tac 1);
+by (blast_tac (claset() addIs [True_True_steps_starI,steps_star_cycle]) 1);
 qed "True_start_steps_star";
 
 (** the start state **)
 
 Goalw [star_def,step_def]
   "!A. (start(star A),r) : step (star A) a = (a=None & r = True#start A)";
-by(Simp_tac 1);
+by (Simp_tac 1);
 qed_spec_mp "start_step_star";
 AddIffs [start_step_star];
 
@@ -605,27 +605,27 @@
 Goal
  "(start(star A),r) : steps (star A) w = \
 \ ((w=[] & r= start(star A)) | (True#start A,r) : steps (star A) w)";
-br iffI 1;
- by(exhaust_tac "w" 1);
-  by(asm_full_simp_tac (simpset() addsimps
+by (rtac iffI 1);
+ by (exhaust_tac "w" 1);
+  by (asm_full_simp_tac (simpset() addsimps
     [epsclosure_start_step_star]) 1);
- by(Asm_full_simp_tac 1);
+ by (Asm_full_simp_tac 1);
  by (Clarify_tac 1);
- by(asm_full_simp_tac (simpset() addsimps
+ by (asm_full_simp_tac (simpset() addsimps
     [epsclosure_start_step_star]) 1);
- by(Blast_tac 1);
-be disjE 1;
- by(Asm_simp_tac 1);
-by(blast_tac (claset() addIs [in_steps_epsclosure,r_into_rtrancl]) 1);
+ by (Blast_tac 1);
+by (etac disjE 1);
+ by (Asm_simp_tac 1);
+by (blast_tac (claset() addIs [in_steps_epsclosure,r_into_rtrancl]) 1);
 qed "start_steps_star";
 
 Goalw [star_def] "!A. fin (star A) (True#p) = fin A p";
-by(Simp_tac 1);
+by (Simp_tac 1);
 qed_spec_mp "fin_star_True";
 AddIffs [fin_star_True];
 
 Goalw [star_def] "!A. fin (star A) (start(star A))";
-by(Simp_tac 1);
+by (Simp_tac 1);
 qed_spec_mp "fin_star_start";
 AddIffs [fin_star_start];
 
@@ -633,25 +633,25 @@
 Goalw [accepts_def]
  "accepts (star A) w = \
 \ (? us. (!u : set(us). accepts A u) & (w = concat us) )";
-by(simp_tac (simpset() addsimps [start_steps_star,True_start_steps_star]) 1);
-br iffI 1;
+by (simp_tac (simpset() addsimps [start_steps_star,True_start_steps_star]) 1);
+by (rtac iffI 1);
  by (Clarify_tac 1);
- be disjE 1;
+ by (etac disjE 1);
   by (Clarify_tac 1);
-  by(Simp_tac 1);
-  by(res_inst_tac [("x","[]")] exI 1);
-  by(Simp_tac 1);
+  by (Simp_tac 1);
+  by (res_inst_tac [("x","[]")] exI 1);
+  by (Simp_tac 1);
  by (Clarify_tac 1);
- by(res_inst_tac [("x","us@[v]")] exI 1);
- by(asm_full_simp_tac (simpset() addsimps [accepts_def]) 1);
- by(Blast_tac 1);
+ by (res_inst_tac [("x","us@[v]")] exI 1);
+ by (asm_full_simp_tac (simpset() addsimps [accepts_def]) 1);
+ by (Blast_tac 1);
 by (Clarify_tac 1);
-by(res_inst_tac [("xs","us")] rev_exhaust 1);
- by(Asm_simp_tac 1);
- by(Blast_tac 1);
+by (res_inst_tac [("xs","us")] rev_exhaust 1);
+ by (Asm_simp_tac 1);
+ by (Blast_tac 1);
 by (Clarify_tac 1);
-by(asm_full_simp_tac (simpset() addsimps [accepts_def]) 1);
-by(Blast_tac 1);
+by (asm_full_simp_tac (simpset() addsimps [accepts_def]) 1);
+by (Blast_tac 1);
 qed "accepts_star";
 
 
@@ -659,10 +659,10 @@
 
 Goal
  "!w. accepts (rexp2nae r) w = (w : lang r)";
-by(induct_tac "r" 1);
-    by(simp_tac (simpset() addsimps [accepts_def]) 1);
-   by(simp_tac(simpset() addsimps [accepts_atom]) 1);
-  by(asm_simp_tac (simpset() addsimps [accepts_union]) 1);
- by(asm_simp_tac (simpset() addsimps [accepts_conc,RegSet.conc_def]) 1);
-by(asm_simp_tac (simpset() addsimps [accepts_star,in_star]) 1);
+by (induct_tac "r" 1);
+    by (simp_tac (simpset() addsimps [accepts_def]) 1);
+   by (simp_tac(simpset() addsimps [accepts_atom]) 1);
+  by (asm_simp_tac (simpset() addsimps [accepts_union]) 1);
+ by (asm_simp_tac (simpset() addsimps [accepts_conc,RegSet.conc_def]) 1);
+by (asm_simp_tac (simpset() addsimps [accepts_star,in_star]) 1);
 qed "accepts_rexp2nae";
diff -r dd4ac220b8b4 -r 24f992a25adc src/HOL/Lex/RegSet.ML
--- a/src/HOL/Lex/RegSet.ML	Fri Jul 10 15:24:22 1998 +0200
+++ b/src/HOL/Lex/RegSet.ML	Sun Jul 12 11:49:17 1998 +0200
@@ -15,7 +15,7 @@
 
 Goal
  "w : star U = (? us. (!u : set(us). u : U) & (w = concat us))";
-br iffI 1;
+by (rtac iffI 1);
  be star.induct 1;
   by (res_inst_tac [("x","[]")] exI 1);
   by (Simp_tac 1);
diff -r dd4ac220b8b4 -r 24f992a25adc src/HOL/Lex/RegSet_of_nat_DA.ML
--- a/src/HOL/Lex/RegSet_of_nat_DA.ML	Fri Jul 10 15:24:22 1998 +0200
+++ b/src/HOL/Lex/RegSet_of_nat_DA.ML	Sun Jul 12 11:49:17 1998 +0200
@@ -210,6 +210,6 @@
 Goalw [regset_of_DA_def]
  "[| bounded (next A) k; start A < k; j < k |] ==> \
 \ w : regset_of_DA A k = accepts A w";
-by(asm_simp_tac (simpset() addcongs [conj_cong] addsimps
+by (asm_simp_tac (simpset() addcongs [conj_cong] addsimps
  [regset_below,deltas_below,accepts_def,delta_def]) 1);
 qed "regset_DA_equiv";
diff -r dd4ac220b8b4 -r 24f992a25adc src/HOL/Lex/Scanner.ML
--- a/src/HOL/Lex/Scanner.ML	Fri Jul 10 15:24:22 1998 +0200
+++ b/src/HOL/Lex/Scanner.ML	Sun Jul 12 11:49:17 1998 +0200
@@ -6,5 +6,5 @@
 
 Goal
  "DA.accepts (nae2da(rexp2nae r)) w = (w : lang r)";
-by(simp_tac (simpset() addsimps [NAe_DA_equiv,accepts_rexp2nae]) 1);
+by (simp_tac (simpset() addsimps [NAe_DA_equiv,accepts_rexp2nae]) 1);
 qed "accepts_nae2da_rexp2nae";
diff -r dd4ac220b8b4 -r 24f992a25adc src/HOL/List.ML
--- a/src/HOL/List.ML	Fri Jul 10 15:24:22 1998 +0200
+++ b/src/HOL/List.ML	Sun Jul 12 11:49:17 1998 +0200
@@ -21,7 +21,7 @@
 (* Induction over the length of a list: *)
 val [prem] = Goal
   "(!!xs. (!ys. length ys < length xs --> P ys) ==> P xs) ==> P(xs)";
-by(rtac measure_induct 1 THEN etac prem 1);
+by (rtac measure_induct 1 THEN etac prem 1);
 qed "length_induct";
 
 
@@ -184,14 +184,14 @@
  [same_append_eq RS iffD1, append1_eq_conv RS iffD1, append_same_eq RS iffD1];
 
 Goal "(xs @ ys = ys) = (xs=[])";
-by(cut_inst_tac [("zs","[]")] append_same_eq 1);
+by (cut_inst_tac [("zs","[]")] append_same_eq 1);
 by (Auto_tac);
 qed "append_self_conv2";
 
 Goal "(ys = xs @ ys) = (xs=[])";
-by(simp_tac (simpset() addsimps
+by (simp_tac (simpset() addsimps
      [simplify (simpset()) (read_instantiate[("ys","[]")]append_same_eq)]) 1);
-by(Blast_tac 1);
+by (Blast_tac 1);
 qed "self_append_conv2";
 AddIffs [append_self_conv2,self_append_conv2];
 
@@ -309,16 +309,16 @@
 AddIffs [Nil_is_rev_conv];
 
 val prems = Goal "[| P []; !!x xs. P xs ==> P(xs@[x]) |] ==> P xs";
-by(stac (rev_rev_ident RS sym) 1);
+by (stac (rev_rev_ident RS sym) 1);
 br(read_instantiate [("P","%xs. ?P(rev xs)")]list.induct)1;
-by(ALLGOALS Simp_tac);
-brs prems 1;
-bes prems 1;
+by (ALLGOALS Simp_tac);
+by (resolve_tac prems 1);
+by (eresolve_tac prems 1);
 qed "rev_induct";
 
 Goal  "(xs = [] --> P) -->  (!ys y. xs = ys@[y] --> P) --> P";
-by(res_inst_tac [("xs","xs")] rev_induct 1);
-by(Auto_tac);
+by (res_inst_tac [("xs","xs")] rev_induct 1);
+by (Auto_tac);
 bind_thm ("rev_exhaust",
   impI RSN (2,allI RSN (2,allI RSN (2,impI RS (result() RS mp RS mp)))));
 
diff -r dd4ac220b8b4 -r 24f992a25adc src/HOL/NatDef.ML
--- a/src/HOL/NatDef.ML	Fri Jul 10 15:24:22 1998 +0200
+++ b/src/HOL/NatDef.ML	Sun Jul 12 11:49:17 1998 +0200
@@ -601,7 +601,7 @@
 Goal "(m::nat) <= n | n <= m";
 by (simp_tac (simpset() addsimps [le_eq_less_or_eq]) 1);
 by (cut_facts_tac [less_linear] 1);
-by(Blast_tac 1);
+by (Blast_tac 1);
 qed "nat_le_linear";
 
 
diff -r dd4ac220b8b4 -r 24f992a25adc src/HOL/Ord.ML
--- a/src/HOL/Ord.ML	Fri Jul 10 15:24:22 1998 +0200
+++ b/src/HOL/Ord.ML	Sun Jul 12 11:49:17 1998 +0200
@@ -58,31 +58,31 @@
 
 Goal "!!x::'a::linorder. x<y | x=y | y<x";
 by (simp_tac (simpset() addsimps [order_less_le]) 1);
-by(cut_facts_tac [linorder_linear] 1);
+by (cut_facts_tac [linorder_linear] 1);
 by (Blast_tac 1);
 qed "linorder_less_linear";
 
 Goalw [max_def] "!!z::'a::linorder. (z <= max x y) = (z <= x | z <= y)";
 by (Simp_tac 1);
-by(cut_facts_tac [linorder_linear] 1);
+by (cut_facts_tac [linorder_linear] 1);
 by (blast_tac (claset() addIs [order_trans]) 1);
 qed "le_max_iff_disj";
 
 Goalw [max_def] "!!z::'a::linorder. (max x y <= z) = (x <= z & y <= z)";
 by (Simp_tac 1);
-by(cut_facts_tac [linorder_linear] 1);
+by (cut_facts_tac [linorder_linear] 1);
 by (blast_tac (claset() addIs [order_trans]) 1);
 qed "max_le_iff_conj";
 
 Goalw [min_def] "!!z::'a::linorder. (z <= min x y) = (z <= x & z <= y)";
 by (Simp_tac 1);
-by(cut_facts_tac [linorder_linear] 1);
+by (cut_facts_tac [linorder_linear] 1);
 by (blast_tac (claset() addIs [order_trans]) 1);
 qed "le_min_iff_conj";
 
 Goalw [min_def] "!!z::'a::linorder. (min x y <= z) = (x <= z | y <= z)";
 by (Simp_tac 1);
-by(cut_facts_tac [linorder_linear] 1);
+by (cut_facts_tac [linorder_linear] 1);
 by (blast_tac (claset() addIs [order_trans]) 1);
 qed "min_le_iff_disj";
 
diff -r dd4ac220b8b4 -r 24f992a25adc src/HOL/Prod.ML
--- a/src/HOL/Prod.ML	Fri Jul 10 15:24:22 1998 +0200
+++ b/src/HOL/Prod.ML	Sun Jul 12 11:49:17 1998 +0200
@@ -156,7 +156,7 @@
 Addsimps split_etas; (* pragmatic solution *)
 
 Goal "(%(x,y,z).f(x,y,z)) = t";
-by(simp_tac (simpset() addsimps [cond_split_eta]) 1);
+by (simp_tac (simpset() addsimps [cond_split_eta]) 1);
 
 qed_goal "split_beta" Prod.thy "(%(x,y). P x y) z = P (fst z) (snd z)"
 	(K [stac surjective_pairing 1, stac split 1, rtac refl 1]);
diff -r dd4ac220b8b4 -r 24f992a25adc src/HOL/Trancl.ML
--- a/src/HOL/Trancl.ML	Fri Jul 10 15:24:22 1998 +0200
+++ b/src/HOL/Trancl.ML	Sun Jul 12 11:49:17 1998 +0200
@@ -114,9 +114,9 @@
 Addsimps [rtrancl_idemp];
 
 Goal "R^* O R^* = R^*";
-br set_ext 1;
-by(split_all_tac 1);
-by(blast_tac (claset() addIs [rtrancl_trans]) 1);
+by (rtac set_ext 1);
+by (split_all_tac 1);
+by (blast_tac (claset() addIs [rtrancl_trans]) 1);
 qed "rtrancl_idemp_self_comp";
 Addsimps [rtrancl_idemp_self_comp];
 
@@ -341,7 +341,7 @@
 by (etac rtranclE 1);
 by  (Auto_tac );
 by (etac rtrancl_into_trancl1 1);
-ba 1;
+by (assume_tac 1);
 qed "reflcl_trancl";
 Addsimps[reflcl_trancl];
 
diff -r dd4ac220b8b4 -r 24f992a25adc src/HOL/UNITY/Traces.ML
--- a/src/HOL/UNITY/Traces.ML	Fri Jul 10 15:24:22 1998 +0200
+++ b/src/HOL/UNITY/Traces.ML	Sun Jul 12 11:49:17 1998 +0200
@@ -53,7 +53,7 @@
 \        ==> P s' |] \
 \  ==> P za";
 by (cut_facts_tac [major] 1);
-auto();
+by Auto_tac;
 be traces.induct 1;
 by (ALLGOALS (blast_tac (claset() addIs prems)));
 qed "reachable_induct";
diff -r dd4ac220b8b4 -r 24f992a25adc src/HOL/WF.ML
--- a/src/HOL/WF.ML	Fri Jul 10 15:24:22 1998 +0200
+++ b/src/HOL/WF.ML	Sun Jul 12 11:49:17 1998 +0200
@@ -232,7 +232,7 @@
 by (simp_tac (HOL_ss addsimps [cuts_eq]) 1);
 by (Clarify_tac 1);
 by (stac cut_apply 1);
- by(fast_tac (claset() addDs [transD]) 1);
+ by (fast_tac (claset() addDs [transD]) 1);
 by (rtac (refl RSN (2,H_cong)) 1);
 by (fold_tac [is_recfun_def]);
 by (asm_simp_tac (wf_super_ss addsimps[is_recfun_cut]) 1);
diff -r dd4ac220b8b4 -r 24f992a25adc src/HOL/arith_data.ML
--- a/src/HOL/arith_data.ML	Fri Jul 10 15:24:22 1998 +0200
+++ b/src/HOL/arith_data.ML	Sun Jul 12 11:49:17 1998 +0200
@@ -226,7 +226,7 @@
 by (induct_tac "l" 1);
 by (Simp_tac 1);
 by (Clarify_tac 1);
-be less_SucE 1;
+by (etac less_SucE 1);
 by (asm_simp_tac (simpset() addsimps [diff_Suc_le_Suc_diff RS le_less_trans,
 				      Suc_diff_n]) 1);
 by (Clarify_tac 1);
diff -r dd4ac220b8b4 -r 24f992a25adc src/HOLCF/IOA/NTP/Multiset.ML
--- a/src/HOLCF/IOA/NTP/Multiset.ML	Fri Jul 10 15:24:22 1998 +0200
+++ b/src/HOLCF/IOA/NTP/Multiset.ML	Sun Jul 12 11:49:17 1998 +0200
@@ -38,7 +38,7 @@
 by (res_inst_tac [("M","M")] Multiset.induction 1);
  by (simp_tac (simpset() addsimps [Multiset.countm_empty_def]) 1);
 by (simp_tac (simpset() addsimps[Multiset.countm_nonempty_def]) 1);
-auto();
+by Auto_tac;
 qed "countm_props";
 
 Goal "!!P. ~P(obj) ==> countm M P = countm (delm M obj) P";
diff -r dd4ac220b8b4 -r 24f992a25adc src/HOLCF/IOA/meta_theory/Abstraction.ML
--- a/src/HOLCF/IOA/meta_theory/Abstraction.ML	Fri Jul 10 15:24:22 1998 +0200
+++ b/src/HOLCF/IOA/meta_theory/Abstraction.ML	Sun Jul 12 11:49:17 1998 +0200
@@ -39,13 +39,13 @@
 Goal "temp_weakening Q P h = (! ex. (ex |== P) --> (cex_abs h ex |== Q))";
 by (simp_tac (simpset() addsimps [temp_weakening_def,temp_strengthening_def,
      NOT_def,temp_sat_def,satisfies_def]) 1);
-auto();
+by Auto_tac;
 qed"temp_weakening_def2";
 
 Goal "state_weakening Q P h = (! s t a. P (s,a,t) --> Q (h(s),a,h(t)))";
 by (simp_tac (simpset() addsimps [state_weakening_def,state_strengthening_def,
      NOT_def]) 1);
-auto();
+by Auto_tac;
 qed"state_weakening_def2";
 
 
@@ -74,7 +74,7 @@
 
 Goal "!!A. is_abstraction h C A ==> weakeningIOA A C h";
 by (asm_full_simp_tac (simpset() addsimps [weakeningIOA_def])1);
-auto();
+by Auto_tac;
 by (asm_full_simp_tac (simpset() addsimps [executions_def]) 1);
 (* start state *) 
 by (rtac conjI 1);
@@ -87,7 +87,7 @@
 
 Goal "!!A. [|is_abstraction h C A; validIOA A Q; temp_strengthening Q P h |] \
 \         ==> validIOA C P";
-bd abs_is_weakening 1;
+by (dtac abs_is_weakening 1);
 by (asm_full_simp_tac (simpset() addsimps [weakeningIOA_def, 
     validIOA_def, temp_strengthening_def])1);
 by (safe_tac set_cs);
@@ -120,8 +120,8 @@
    "!!A. [|is_live_abstraction h (C,L) (A,M); \
 \         validLIOA (A,M) Q;  temp_strengthening Q P h |] \
 \         ==> validLIOA (C,L) P";
-auto();
-bd abs_is_weakening 1;
+by Auto_tac;
+by (dtac abs_is_weakening 1);
 by (asm_full_simp_tac (simpset() addsimps [weakeningIOA_def, temp_weakening_def2,
     validLIOA_def, validIOA_def, temp_strengthening_def])1);
 by (safe_tac set_cs);
@@ -134,8 +134,8 @@
 \         validLIOA (A,M) (H1 .--> Q);  temp_strengthening Q P h; \
 \         temp_weakening H1 H2 h; validLIOA (C,L) H2 |] \
 \         ==> validLIOA (C,L) P";
-auto();
-bd abs_is_weakening 1;
+by Auto_tac;
+by (dtac abs_is_weakening 1);
 by (asm_full_simp_tac (simpset() addsimps [weakeningIOA_def, temp_weakening_def2,
     validLIOA_def, validIOA_def, temp_strengthening_def])1);
 by (safe_tac set_cs);
@@ -162,10 +162,10 @@
 \                  is_abstraction h C A |] \
 \               ==> C =<| A";
 by (asm_full_simp_tac (simpset() addsimps [ioa_implements_def]) 1);
-br trace_inclusion 1;
+by (rtac trace_inclusion 1);
 by (simp_tac (simpset() addsimps [externals_def])1);
 by (SELECT_GOAL (auto_tac (claset(),simpset()))1);
-be abstraction_is_ref_map 1;
+by (etac abstraction_is_ref_map 1);
 qed"abs_safety";
 
 
@@ -244,7 +244,7 @@
 
 Goalw [ioa_implements_def] 
 "!! A. [| A =<| B; B =<| C|] ==> A =<| C"; 
-auto();
+by Auto_tac;
 qed"implements_trans";
 
 
@@ -260,13 +260,13 @@
 \                  A =<| Q ; \
 \                  is_abstraction h2 Q P |] \
 \               ==> C =<| P";   
-bd abs_safety 1;
+by (dtac abs_safety 1);
 by (REPEAT (atac 1));
-bd abs_safety 1;
+by (dtac abs_safety 1);
 by (REPEAT (atac 1));
-be implements_trans 1;
-be implements_trans 1;
-ba 1;
+by (etac implements_trans 1);
+by (etac implements_trans 1);
+by (assume_tac 1);
 qed"AbsRuleA1";
 
 
@@ -276,13 +276,13 @@
 \                  live_implements (A,LA) (Q,LQ) ; \
 \                  is_live_abstraction h2 (Q,LQ) (P,LP) |] \
 \               ==> live_implements (C,LC) (P,LP)";   
-bd abs_liveness 1;
+by (dtac abs_liveness 1);
 by (REPEAT (atac 1));
-bd abs_liveness 1;
+by (dtac abs_liveness 1);
 by (REPEAT (atac 1));
-be live_implements_trans 1;
-be live_implements_trans 1;
-ba 1;
+by (etac live_implements_trans 1);
+by (etac live_implements_trans 1);
+by (assume_tac 1);
 qed"AbsRuleA2";
 
 
@@ -299,21 +299,21 @@
 "!! h. [| temp_strengthening P1 Q1 h; \
 \         temp_strengthening P2 Q2 h |] \
 \      ==> temp_strengthening (P1 .& P2) (Q1 .& Q2) h";
-auto();
+by Auto_tac;
 qed"strength_AND";
 
 Goalw [temp_strengthening_def]
 "!! h. [| temp_strengthening P1 Q1 h; \
 \         temp_strengthening P2 Q2 h |] \
 \      ==> temp_strengthening (P1 .| P2) (Q1 .| Q2) h";
-auto();
+by Auto_tac;
 qed"strength_OR";
 
 Goalw [temp_strengthening_def]
 "!! h. [| temp_weakening P Q h |] \
 \      ==> temp_strengthening (.~ P) (.~ Q) h";
 by (asm_full_simp_tac (simpset() addsimps [temp_weakening_def2])1);
-auto();
+by Auto_tac;
 qed"strength_NOT";
 
 Goalw [temp_strengthening_def]
@@ -347,7 +347,7 @@
 "!! h. [| temp_strengthening P Q h |] \
 \      ==> temp_weakening (.~ P) (.~ Q) h";
 by (asm_full_simp_tac (simpset() addsimps [temp_weakening_def2])1);
-auto();
+by Auto_tac;
 qed"weak_NOT";
 
 Goalw [temp_strengthening_def]
@@ -387,16 +387,16 @@
 by (asm_full_simp_tac (simpset() addsimps [nil_is_Conc])1);
 (* cons case *)
 by (pair_tac "aa" 1);
-auto();
+by Auto_tac;
 qed_spec_mp"ex2seqConc";
 
 (* important property of ex2seq: can be shiftet, as defined "pointwise" *)
 
 Goalw [tsuffix_def,suffix_def]
 "!!s. tsuffix s (ex2seq ex) ==> ? ex'. s = (ex2seq ex')";
-auto();
-bd ex2seqConc 1;
-auto();
+by Auto_tac;
+by (dtac ex2seqConc 1);
+by Auto_tac;
 qed"ex2seq_tsuffix";
 
 
@@ -414,7 +414,7 @@
 
 Goalw [tsuffix_def,suffix_def,cex_absSeq_def]
 "!! s. tsuffix s t ==> tsuffix (cex_absSeq h s) (cex_absSeq h t)";
-auto();
+by Auto_tac;
 by (asm_full_simp_tac (simpset() addsimps [Mapnil])1);
 by (asm_full_simp_tac (simpset() addsimps [MapUU])1);
 by (res_inst_tac [("x","Map (%(s,a,t). (h s,a, h t))`s1")] exI 1);
@@ -486,7 +486,7 @@
 by (pair_tac "ex" 1);
 by (Seq_case_simp_tac "y" 1);
 by (pair_tac "a" 1);
-auto();
+by Auto_tac;
 qed"TLex2seq";
 
 
@@ -520,9 +520,9 @@
 (* cons case *)
 by (asm_full_simp_tac (simpset() addsimps [TL_ex2seq_nil,TL_ex2seq_UU,
         ex2seq_abs_cex,cex_absSeq_TL RS sym, ex2seqUUTL,ex2seqnilTL])1);
-bd TLex2seq 1;
-ba 1;
-auto();
+by (dtac TLex2seq 1);
+by (assume_tac 1);
+by Auto_tac;
 qed"strength_Next";
 
 
@@ -572,18 +572,18 @@
 Goalw [Diamond_def]
 "!! h. [| temp_strengthening P Q h |]\
 \      ==> temp_strengthening (<> P) (<> Q) h";
-br strength_NOT 1;
-br weak_Box 1;
-be weak_NOT 1;
+by (rtac strength_NOT 1);
+by (rtac weak_Box 1);
+by (etac weak_NOT 1);
 qed"strength_Diamond";
 
 Goalw [Leadsto_def]
 "!! h. [| temp_weakening P1 P2 h;\
 \         temp_strengthening Q1 Q2 h |]\
 \      ==> temp_strengthening (P1 ~> Q1) (P2 ~> Q2) h";
-br strength_Box 1;
-be strength_IMPLIES 1;
-be strength_Diamond 1;
+by (rtac strength_Box 1);
+by (etac strength_IMPLIES 1);
+by (etac strength_Diamond 1);
 qed"strength_Leadsto";
 
 
@@ -595,30 +595,30 @@
 Goalw [Diamond_def]
 "!! h. [| temp_weakening P Q h |]\
 \      ==> temp_weakening (<> P) (<> Q) h";
-br weak_NOT 1;
-br strength_Box 1;
-be strength_NOT 1;
+by (rtac weak_NOT 1);
+by (rtac strength_Box 1);
+by (etac strength_NOT 1);
 qed"weak_Diamond";
 
 Goalw [Leadsto_def]
 "!! h. [| temp_strengthening P1 P2 h;\
 \         temp_weakening Q1 Q2 h |]\
 \      ==> temp_weakening (P1 ~> Q1) (P2 ~> Q2) h";
-br weak_Box 1;
-be weak_IMPLIES 1;
-be weak_Diamond 1;
+by (rtac weak_Box 1);
+by (etac weak_IMPLIES 1);
+by (etac weak_Diamond 1);
 qed"weak_Leadsto";
 
 Goalw [WF_def]
   " !!A. [| !! s. Enabled A acts (h s) ==> Enabled C acts s|] \ 
 \   ==> temp_weakening (WF A acts) (WF C acts) h";
-br weak_IMPLIES 1;
-br strength_Diamond 1;
-br strength_Box 1;
-br strength_Init 1;
-br weak_Box 2;
-br weak_Diamond 2;
-br weak_Init 2;
+by (rtac weak_IMPLIES 1);
+by (rtac strength_Diamond 1);
+by (rtac strength_Box 1);
+by (rtac strength_Init 1);
+by (rtac weak_Box 2);
+by (rtac weak_Diamond 2);
+by (rtac weak_Init 2);
 by (auto_tac (claset(),
               simpset() addsimps [state_weakening_def,state_strengthening_def,
                              xt2_def,plift_def,option_lift_def,NOT_def]));
@@ -627,13 +627,13 @@
 Goalw [SF_def]
   " !!A. [| !! s. Enabled A acts (h s) ==> Enabled C acts s|] \ 
 \   ==> temp_weakening (SF A acts) (SF C acts) h";
-br weak_IMPLIES 1;
-br strength_Box 1;
-br strength_Diamond 1;
-br strength_Init 1;
-br weak_Box 2;
-br weak_Diamond 2;
-br weak_Init 2;
+by (rtac weak_IMPLIES 1);
+by (rtac strength_Box 1);
+by (rtac strength_Diamond 1);
+by (rtac strength_Init 1);
+by (rtac weak_Box 2);
+by (rtac weak_Diamond 2);
+by (rtac weak_Init 2);
 by (auto_tac (claset(),
               simpset() addsimps [state_weakening_def,state_strengthening_def,
                              xt2_def,plift_def,option_lift_def,NOT_def]));
diff -r dd4ac220b8b4 -r 24f992a25adc src/HOLCF/IOA/meta_theory/Deadlock.ML
--- a/src/HOLCF/IOA/meta_theory/Deadlock.ML	Fri Jul 10 15:24:22 1998 +0200
+++ b/src/HOLCF/IOA/meta_theory/Deadlock.ML	Sun Jul 12 11:49:17 1998 +0200
@@ -59,7 +59,7 @@
 by (rtac conjI 1);
 (* a : act (A||B) *)
 by (asm_full_simp_tac (simpset() addsimps [actions_of_par]) 2);
-by(blast_tac (claset() addDs [int_is_act,out_is_act]) 2);
+by (blast_tac (claset() addDs [int_is_act,out_is_act]) 2);
 
 (* Filter B (sch@@[a]) : schedules B *)
 
diff -r dd4ac220b8b4 -r 24f992a25adc src/HOLCF/IOA/meta_theory/LiveIOA.ML
--- a/src/HOLCF/IOA/meta_theory/LiveIOA.ML	Fri Jul 10 15:24:22 1998 +0200
+++ b/src/HOLCF/IOA/meta_theory/LiveIOA.ML	Sun Jul 12 11:49:17 1998 +0200
@@ -12,7 +12,7 @@
 Goalw [live_implements_def] 
 "!! A. [| live_implements (A,LA) (B,LB); live_implements (B,LB) (C,LC) |] \
 \     ==> live_implements (A,LA) (C,LC)"; 
-auto();
+by Auto_tac;
 qed"live_implements_trans";
 
 
@@ -51,7 +51,7 @@
   by (asm_full_simp_tac (simpset() addsimps [reachable.reachable_0]) 1);
 
  (* Liveness *)
-auto();
+by Auto_tac;
 qed"live_implements";
 
 
diff -r dd4ac220b8b4 -r 24f992a25adc src/HOLCF/IOA/meta_theory/RefCorrectness.ML
--- a/src/HOLCF/IOA/meta_theory/RefCorrectness.ML	Fri Jul 10 15:24:22 1998 +0200
+++ b/src/HOLCF/IOA/meta_theory/RefCorrectness.ML	Sun Jul 12 11:49:17 1998 +0200
@@ -256,7 +256,7 @@
 
 
 Goalw [fin_often_def] "(~inf_often P s) = fin_often P s";
-auto();
+by Auto_tac;
 qed"fininf";
 
 
@@ -264,17 +264,17 @@
 "is_wfair A W (s,ex) = \
 \ (fin_often (%x. ~Enabled A W (snd x)) ex --> inf_often (%x. fst x :W) ex)";
 by (asm_full_simp_tac (simpset() addsimps [is_wfair_def,fin_often_def])1);
-auto();
+by Auto_tac;
 qed"WF_alt";
 
 Goal  
 "!! ex. [|is_wfair A W (s,ex); inf_often (%x. Enabled A W (snd x)) ex; \
 \         en_persistent A W|] \
 \   ==> inf_often (%x. fst x :W) ex";
-bd persistent 1;
-ba 1;
+by (dtac persistent 1);
+by (assume_tac 1);
 by (asm_full_simp_tac (simpset() addsimps [WF_alt])1);
-auto();
+by Auto_tac;
 qed"WF_persistent";
 
 
@@ -305,7 +305,7 @@
   by (asm_full_simp_tac (simpset() addsimps [reachable.reachable_0]) 1);
 
  (* Fairness *)
-auto();
+by Auto_tac;
 qed"fair_trace_inclusion";
 
 Goal "!! C A. \
@@ -335,7 +335,7 @@
   by (asm_full_simp_tac (simpset() addsimps [reachable.reachable_0]) 1);
 
  (* Fairness *)
-auto();
+by Auto_tac;
 qed"fair_trace_inclusion2";
 
 
diff -r dd4ac220b8b4 -r 24f992a25adc src/HOLCF/IOA/meta_theory/SimCorrectness.ML
--- a/src/HOLCF/IOA/meta_theory/SimCorrectness.ML	Fri Jul 10 15:24:22 1998 +0200
+++ b/src/HOLCF/IOA/meta_theory/SimCorrectness.ML	Sun Jul 12 11:49:17 1998 +0200
@@ -27,9 +27,9 @@
 \                              @@ ((corresp_ex_simC A R `xs) T'))   \
 \                        `x) ))";
 by (rtac trans 1);
-br fix_eq2 1;
-br corresp_ex_simC_def 1;
-br beta_cfun 1;
+by (rtac fix_eq2 1);
+by (rtac corresp_ex_simC_def 1);
+by (rtac beta_cfun 1);
 by (simp_tac (simpset() addsimps [flift1_def]) 1);
 qed"corresp_ex_simC_unfold";
 
@@ -48,7 +48,7 @@
 \           in  \
 \            (@cex. move A cex s a T')  \ 
 \             @@ ((corresp_ex_simC A R`xs) T'))";
-br trans 1;
+by (rtac trans 1);
 by (stac corresp_ex_simC_unfold 1);
 by (asm_full_simp_tac (simpset() addsimps [Cons_def,flift1_def]) 1);
 by (Simp_tac 1);
@@ -84,15 +84,15 @@
 by (eres_inst_tac [("x","a")] allE 2);
 by (Asm_full_simp_tac 2); 
 (* Go on as usual *)
-be exE 1;
+by (etac exE 1);
 by (dres_inst_tac [("x","t'"),
          ("P","%t'. ? ex.(t,t'):R & move A ex s' a t'")] selectI 1);
-be exE 1;
-be conjE 1;
+by (etac exE 1);
+by (etac conjE 1);
 by (asm_full_simp_tac (simpset() addsimps [Let_def]) 1);
 by (res_inst_tac [("x","ex")] selectI 1);
-be conjE 1;
-ba 1;
+by (etac conjE 1);
+by (assume_tac 1);
 qed"move_is_move_sim";
 
 
@@ -168,7 +168,7 @@
 ren "ex a t s s'" 1;
 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","t")] allE 1);
 by (eres_inst_tac [("x",
                     "@t'. ? ex1. (t,t'):R & move A ex1 s' a t'")] 
@@ -202,12 +202,12 @@
     lemma_2_1 1);
 
 (* Finite *)
-be (rewrite_rule [Let_def] move_subprop2_sim) 1;
+by (etac (rewrite_rule [Let_def] move_subprop2_sim) 1);
 by (REPEAT (atac 1));
 by (rtac conjI 1);
 
 (* is_exec_frag *)
-be  (rewrite_rule [Let_def] move_subprop1_sim) 1;
+by (etac (rewrite_rule [Let_def] move_subprop1_sim) 1);
 by (REPEAT (atac 1));
 by (rtac conjI 1);
 
@@ -219,11 +219,11 @@
      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 (simpset() addsimps 
             [rewrite_rule [Let_def] move_subprop5_sim]) 1);
 (* laststate *)
-be ((rewrite_rule [Let_def] move_subprop3_sim) RS sym) 1;
+by (etac ((rewrite_rule [Let_def] move_subprop3_sim) RS sym) 1);
 by (REPEAT (atac 1));
 qed_spec_mp"correspsim_is_execution";
 
@@ -246,11 +246,11 @@
   by (asm_full_simp_tac (simpset() addsimps [is_simulation_def,
          corresp_ex_sim_def, Int_non_empty,Image_def]) 1);
   by (REPEAT (etac conjE 1));
-  be ballE 1;
+  by (etac ballE 1);
   by (Blast_tac 2);
-  be exE 1;
-  br selectI2 1;
-  ba 1;
+  by (etac exE 1);
+  by (rtac selectI2 1);
+  by (assume_tac 1);
   by (Blast_tac 1);
 qed"simulation_starts";
 
@@ -290,7 +290,7 @@
   (* is-execution-fragment *)
   by (asm_full_simp_tac (simpset() addsimps [corresp_ex_sim_def]) 1);
   by (res_inst_tac [("s","s")] correspsim_is_execution 1);
-  ba 1;
+  by (assume_tac 1);
   by (asm_full_simp_tac (simpset() addsimps [reachable.reachable_0,sim_starts1]) 1);
 qed"trace_inclusion_for_simulations"; 
 
diff -r dd4ac220b8b4 -r 24f992a25adc src/HOLCF/IOA/meta_theory/Simulations.ML
--- a/src/HOLCF/IOA/meta_theory/Simulations.ML	Fri Jul 10 15:24:22 1998 +0200
+++ b/src/HOLCF/IOA/meta_theory/Simulations.ML	Sun Jul 12 11:49:17 1998 +0200
@@ -10,7 +10,7 @@
 
 Goal "(A~={}) = (? x. x:A)";
 by (safe_tac set_cs);
-auto();
+by Auto_tac;
 qed"set_non_empty";
 
 Goal "(A Int B ~= {}) = (? x. x: A & x:B)";
diff -r dd4ac220b8b4 -r 24f992a25adc src/HOLCF/IOA/meta_theory/TL.ML
--- a/src/HOLCF/IOA/meta_theory/TL.ML	Fri Jul 10 15:24:22 1998 +0200
+++ b/src/HOLCF/IOA/meta_theory/TL.ML	Sun Jul 12 11:49:17 1998 +0200
@@ -8,9 +8,9 @@
 
 
 Goal "[] <> (.~ P) = (.~ <> [] P)";
-br ext 1;
+by (rtac ext 1);
 by (simp_tac (simpset() addsimps [Diamond_def,NOT_def,Box_def])1);
-auto();
+by Auto_tac;
 qed"simple_try";
 
 Goal "nil |= [] P";
@@ -39,7 +39,7 @@
 Goal "suffix s s";
 by (simp_tac (simpset() addsimps [suffix_def])1);
 by (res_inst_tac [("x","nil")] exI 1);
-auto();
+by Auto_tac;
 qed"suffix_refl";
 
 Goal "s~=UU & s~=nil --> (s |= [] F .--> F)";
@@ -52,19 +52,19 @@
 
 Goal "!!x. [| suffix y x ; suffix z y |]  ==> suffix z x";
 by (asm_full_simp_tac (simpset() addsimps [suffix_def])1);
-auto();
+by Auto_tac;
 by (res_inst_tac [("x","s1 @@ s1a")] exI 1);
-auto();
+by Auto_tac;
 by (simp_tac (simpset() addsimps [Conc_assoc]) 1); 
 qed"suffix_trans";
 
 Goal "s |= [] F .--> [] [] F";
 by (simp_tac (simpset() addsimps [satisfies_def,IMPLIES_def,Box_def,tsuffix_def])1);
-auto();
-bd suffix_trans 1;
-ba 1;
+by Auto_tac;
+by (dtac suffix_trans 1);
+by (assume_tac 1);
 by (eres_inst_tac [("x","s2a")] allE 1);
-auto();
+by Auto_tac;
 qed"transT";
 
 
@@ -76,13 +76,13 @@
 (*
 Goal "s |= <> F .& <> G .--> (<> (F .& <> G) .| <> (G .& <> F))";
 by (simp_tac (simpset() addsimps [satisfies_def,IMPLIES_def,AND_def,OR_def,Diamond_def2])1);
-br impI 1;
-be conjE 1;
-be exE 1;
-be exE 1;
+by (rtac impI 1);
+by (etac conjE 1);
+by (etac exE 1);
+by (etac exE 1);
 
 
-br disjI1 1;
+by (rtac disjI1 1);
 
 Goal "!!s. [| tsuffix s1 s ; tsuffix s2 s|] ==> tsuffix s2 s1 | tsuffix s1 s2";
 by (asm_full_simp_tac (simpset() addsimps [tsuffix_def,suffix_def])1);
@@ -109,8 +109,8 @@
 qed"STL1b";
 
 Goal "!! P. valid P ==> validT ([] (Init P))";
-br STL1a 1;
-be STL1b 1;
+by (rtac STL1a 1);
+by (etac STL1b 1);
 qed"STL1";
 
 
@@ -130,10 +130,10 @@
 
 Goalw [tsuffix_def,suffix_def]
 "s~=UU & s~=nil --> tsuffix s2 (TL`s) --> tsuffix s2 s";
-auto();
+by Auto_tac;
 by (Seq_case_simp_tac "s" 1);
 by (res_inst_tac [("x","a>>s1")] exI 1);
-auto();
+by Auto_tac;
 qed_spec_mp"tsuffix_TL";
 
 val tsuffix_TL2 = conjI RS tsuffix_TL;
@@ -141,16 +141,16 @@
 Delsplits[split_if];
 Goalw [Next_def,satisfies_def,NOT_def,IMPLIES_def,AND_def,Box_def] 
    "s~=UU & s~=nil --> (s |= [] F .--> (F .& (Next ([] F))))";
-auto();
+by Auto_tac;
 (* []F .--> F *)
 by (eres_inst_tac [("x","s")] allE 1);
 by (asm_full_simp_tac (simpset() addsimps [tsuffix_def,suffix_refl])1);
 (* []F .--> Next [] F *)
 by (asm_full_simp_tac (simpset() addsplits [split_if]) 1);
-auto();
-bd tsuffix_TL2 1;
+by Auto_tac;
+by (dtac tsuffix_TL2 1);
 by (REPEAT (atac 1));
-auto();
+by Auto_tac;
 qed"LTL1";
 Addsplits[split_if];
 
@@ -173,11 +173,11 @@
 Goalw [Next_def,satisfies_def,Box_def,NOT_def,IMPLIES_def] 
  "s |= [] (F .--> Next F) .--> F .--> []F";
 by (Asm_full_simp_tac 1);
-auto();
+by Auto_tac;
 
 
 by (asm_full_simp_tac (simpset() addsimps [tsuffix_def,suffix_def])1);
-auto();
+by Auto_tac;
 
 
 
diff -r dd4ac220b8b4 -r 24f992a25adc src/HOLCF/IOA/meta_theory/TrivEx.ML
--- a/src/HOLCF/IOA/meta_theory/TrivEx.ML	Fri Jul 10 15:24:22 1998 +0200
+++ b/src/HOLCF/IOA/meta_theory/TrivEx.ML	Sun Jul 12 11:49:17 1998 +0200
@@ -7,7 +7,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";
 
 
@@ -24,14 +24,14 @@
         C_ioa_def,A_ioa_def,C_trans_def,A_trans_def])1);
 by (simp_tac (simpset() addsimps [h_abs_def]) 1);
 by (action.induct_tac "a" 1);
-auto();
+by Auto_tac;
 qed"h_abs_is_abstraction";
 
 
 Goal "validIOA C_ioa (<>[] <%(n,a,m). n~=0>)";
-br AbsRuleT1 1;
-br h_abs_is_abstraction 1;
-br MC_result 1;
+by (rtac AbsRuleT1 1);
+by (rtac h_abs_is_abstraction 1);
+by (rtac MC_result 1);
 by (abstraction_tac 1);
 by (asm_full_simp_tac (simpset() addsimps [h_abs_def]) 1);
 qed"TrivEx_abstraction";
diff -r dd4ac220b8b4 -r 24f992a25adc src/HOLCF/IOA/meta_theory/TrivEx2.ML
--- a/src/HOLCF/IOA/meta_theory/TrivEx2.ML	Fri Jul 10 15:24:22 1998 +0200
+++ b/src/HOLCF/IOA/meta_theory/TrivEx2.ML	Sun Jul 12 11:49:17 1998 +0200
@@ -7,7 +7,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";
 
 
@@ -24,7 +24,7 @@
         C_ioa_def,A_ioa_def,C_trans_def,A_trans_def])1);
 by (simp_tac (simpset() addsimps [h_abs_def]) 1);
 by (action.induct_tac "a" 1);
-auto();
+by Auto_tac;
 qed"h_abs_is_abstraction";
 
 
@@ -39,26 +39,26 @@
 Goalw [Enabled_def, enabled_def, h_abs_def,A_ioa_def,C_ioa_def,A_trans_def,
            C_trans_def,trans_of_def] 
 "!!s. Enabled A_ioa {INC} (h_abs s) ==> Enabled C_ioa {INC} s";
-auto();
+by Auto_tac;
 qed"Enabled_implication";
 
 
 Goalw [is_live_abstraction_def]
 "is_live_abstraction h_abs (C_ioa, WF C_ioa {INC}) (A_ioa, WF A_ioa {INC})";
-auto();
+by Auto_tac;
 (* is_abstraction *)
-br h_abs_is_abstraction 1;
+by (rtac h_abs_is_abstraction 1);
 (* temp_weakening *)
 by (abstraction_tac 1);
-be Enabled_implication 1;
+by (etac Enabled_implication 1);
 qed"h_abs_is_liveabstraction";
 
 
 Goalw [C_live_ioa_def]
 "validLIOA C_live_ioa (<>[] <%(n,a,m). n~=0>)";
-br AbsRuleT2 1;
-br h_abs_is_liveabstraction 1;
-br MC_result 1;
+by (rtac AbsRuleT2 1);
+by (rtac h_abs_is_liveabstraction 1);
+by (rtac MC_result 1);
 by (abstraction_tac 1);
 by (asm_full_simp_tac (simpset() addsimps [h_abs_def]) 1);
 qed"TrivEx2_abstraction";