isatool expandshort;
authorwenzelm
Sun Jul 12 11:49:17 1998 +0200 (1998-07-12)
changeset 513224f992a25adc
parent 5131 dd4ac220b8b4
child 5133 42a7fe39a63a
isatool expandshort;
src/HOL/IOA/IOA.ML
src/HOL/IOA/Solve.ML
src/HOL/Lex/AutoMaxChop.ML
src/HOL/Lex/AutoProj.ML
src/HOL/Lex/Automata.ML
src/HOL/Lex/DA.ML
src/HOL/Lex/MaxChop.ML
src/HOL/Lex/MaxPrefix.ML
src/HOL/Lex/NAe.ML
src/HOL/Lex/Prefix.ML
src/HOL/Lex/RegExp2NAe.ML
src/HOL/Lex/RegSet.ML
src/HOL/Lex/RegSet_of_nat_DA.ML
src/HOL/Lex/Scanner.ML
src/HOL/List.ML
src/HOL/NatDef.ML
src/HOL/Ord.ML
src/HOL/Prod.ML
src/HOL/Trancl.ML
src/HOL/UNITY/Traces.ML
src/HOL/WF.ML
src/HOL/arith_data.ML
src/HOLCF/IOA/NTP/Multiset.ML
src/HOLCF/IOA/meta_theory/Abstraction.ML
src/HOLCF/IOA/meta_theory/Deadlock.ML
src/HOLCF/IOA/meta_theory/LiveIOA.ML
src/HOLCF/IOA/meta_theory/RefCorrectness.ML
src/HOLCF/IOA/meta_theory/SimCorrectness.ML
src/HOLCF/IOA/meta_theory/Simulations.ML
src/HOLCF/IOA/meta_theory/TL.ML
src/HOLCF/IOA/meta_theory/TrivEx.ML
src/HOLCF/IOA/meta_theory/TrivEx2.ML
     1.1 --- a/src/HOL/IOA/IOA.ML	Fri Jul 10 15:24:22 1998 +0200
     1.2 +++ b/src/HOL/IOA/IOA.ML	Sun Jul 12 11:49:17 1998 +0200
     1.3 @@ -56,7 +56,7 @@
     1.4  "!!A. [| reachable A s; (s,a,t) : trans_of(A) |] ==> reachable A t";
     1.5    by (asm_full_simp_tac (simpset() delsimps bex_simps) 1);
     1.6    by (split_all_tac 1);
     1.7 -  by (Safe_tac);
     1.8 +  by Safe_tac;
     1.9    by (rename_tac "ex1 ex2 n" 1);
    1.10    by (res_inst_tac [("x","(%i. if i<n then ex1 i                    \
    1.11  \                            else (if i=n then Some a else None),    \
    1.12 @@ -79,7 +79,7 @@
    1.13  \     !!s t a. [|reachable A s; P(s)|] ==> (s,a,t): trans_of(A) --> P(t) |] \
    1.14  \  ==> invariant A P";
    1.15    by (rewrite_goals_tac(reachable_def::Let_def::exec_rws));
    1.16 -  by (Safe_tac);
    1.17 +  by Safe_tac;
    1.18    by (rename_tac "ex1 ex2 n" 1);
    1.19    by (res_inst_tac [("Q","reachable A (ex2 n)")] conjunct1 1);
    1.20    by (Asm_full_simp_tac 1);
     2.1 --- a/src/HOL/IOA/Solve.ML	Fri Jul 10 15:24:22 1998 +0200
     2.2 +++ b/src/HOL/IOA/Solve.ML	Sun Jul 12 11:49:17 1998 +0200
     2.3 @@ -15,7 +15,7 @@
     2.4  \          is_weak_pmap f C A |] ==> traces(C) <= traces(A)";
     2.5  
     2.6    by (simp_tac(simpset() addsimps [has_trace_def])1);
     2.7 -  by (Safe_tac);
     2.8 +  by Safe_tac;
     2.9    by (rename_tac "ex1 ex2" 1);
    2.10  
    2.11    (* choose same trace, therefore same NF *)
     3.1 --- a/src/HOL/Lex/AutoMaxChop.ML	Fri Jul 10 15:24:22 1998 +0200
     3.2 +++ b/src/HOL/Lex/AutoMaxChop.ML	Sun Jul 12 11:49:17 1998 +0200
     3.3 @@ -5,33 +5,33 @@
     3.4  *)
     3.5  
     3.6  Goal "delta A (xs@[y]) q = next A y (delta A xs q)";
     3.7 -by(Simp_tac 1);
     3.8 +by (Simp_tac 1);
     3.9  qed "delta_snoc";
    3.10  
    3.11  Goal
    3.12   "!q ps res. auto_split A (delta A ps q) res ps xs = \
    3.13  \            maxsplit (%ys. fin A (delta A ys q)) res ps xs";
    3.14 -by(induct_tac "xs" 1);
    3.15 -by(Simp_tac 1);
    3.16 -by(asm_simp_tac (simpset() addsimps [delta_snoc RS sym]
    3.17 +by (induct_tac "xs" 1);
    3.18 +by (Simp_tac 1);
    3.19 +by (asm_simp_tac (simpset() addsimps [delta_snoc RS sym]
    3.20                             delsimps [delta_append]) 1);
    3.21  qed_spec_mp "auto_split_lemma";
    3.22  
    3.23  Goalw [accepts_def]
    3.24   "auto_split A (start A) res [] xs = maxsplit (accepts A) res [] xs";
    3.25 -by(stac ((read_instantiate [("s","start A")] delta_Nil) RS sym) 1);
    3.26 -by(stac auto_split_lemma 1);
    3.27 -by(Simp_tac 1);
    3.28 +by (stac ((read_instantiate [("s","start A")] delta_Nil) RS sym) 1);
    3.29 +by (stac auto_split_lemma 1);
    3.30 +by (Simp_tac 1);
    3.31  qed_spec_mp "auto_split_is_maxsplit";
    3.32  
    3.33  Goal
    3.34   "is_maxsplitter (accepts A) (%xs. auto_split A (start A) ([],xs) [] xs)";
    3.35 -by(simp_tac (simpset() addsimps
    3.36 +by (simp_tac (simpset() addsimps
    3.37          [auto_split_is_maxsplit,is_maxsplitter_maxsplit]) 1);
    3.38  qed "is_maxsplitter_auto_split";
    3.39  
    3.40  Goalw [auto_chop_def]
    3.41   "is_maxchopper (accepts A) (auto_chop A)";
    3.42 -br is_maxchopper_chop 1;
    3.43 -br is_maxsplitter_auto_split 1;
    3.44 +by (rtac is_maxchopper_chop 1);
    3.45 +by (rtac is_maxsplitter_auto_split 1);
    3.46  qed "is_maxchopper_auto_chop";
     4.1 --- a/src/HOL/Lex/AutoProj.ML	Fri Jul 10 15:24:22 1998 +0200
     4.2 +++ b/src/HOL/Lex/AutoProj.ML	Sun Jul 12 11:49:17 1998 +0200
     4.3 @@ -5,15 +5,15 @@
     4.4  *)
     4.5  
     4.6  Goalw [start_def] "start(q,d,f) = q";
     4.7 -by(Simp_tac 1);
     4.8 +by (Simp_tac 1);
     4.9  qed "start_conv";
    4.10  
    4.11  Goalw [next_def] "next(q,d,f) = d";
    4.12 -by(Simp_tac 1);
    4.13 +by (Simp_tac 1);
    4.14  qed "next_conv";
    4.15  
    4.16  Goalw [fin_def] "fin(q,d,f) = f";
    4.17 -by(Simp_tac 1);
    4.18 +by (Simp_tac 1);
    4.19  qed "fin_conv";
    4.20  
    4.21  Addsimps [start_conv,next_conv,fin_conv];
     5.1 --- a/src/HOL/Lex/Automata.ML	Fri Jul 10 15:24:22 1998 +0200
     5.2 +++ b/src/HOL/Lex/Automata.ML	Sun Jul 12 11:49:17 1998 +0200
     5.3 @@ -8,35 +8,35 @@
     5.4  
     5.5  Goalw [na2da_def]
     5.6   "!Q. DA.delta (na2da A) w Q = Union(NA.delta A w `` Q)";
     5.7 -by(induct_tac "w" 1);
     5.8 - by(ALLGOALS Asm_simp_tac);
     5.9 - by(ALLGOALS Blast_tac);
    5.10 +by (induct_tac "w" 1);
    5.11 + by (ALLGOALS Asm_simp_tac);
    5.12 + by (ALLGOALS Blast_tac);
    5.13  qed_spec_mp "DA_delta_is_lift_NA_delta";
    5.14  
    5.15  Goalw [DA.accepts_def,NA.accepts_def]
    5.16    "NA.accepts A w = DA.accepts (na2da A) w";
    5.17 -by(simp_tac (simpset() addsimps [DA_delta_is_lift_NA_delta]) 1);
    5.18 -by(simp_tac (simpset() addsimps [na2da_def]) 1);
    5.19 +by (simp_tac (simpset() addsimps [DA_delta_is_lift_NA_delta]) 1);
    5.20 +by (simp_tac (simpset() addsimps [na2da_def]) 1);
    5.21  qed "NA_DA_equiv";
    5.22  
    5.23  (*** Direct equivalence of NAe and DA ***)
    5.24  
    5.25  Goalw [nae2da_def]
    5.26   "!Q. (eps A)^* ^^ (DA.delta (nae2da A) w Q) = steps A w ^^ Q";
    5.27 -by(induct_tac "w" 1);
    5.28 +by (induct_tac "w" 1);
    5.29   by (Simp_tac 1);
    5.30 -by(asm_full_simp_tac (simpset() addsimps [step_def]) 1);
    5.31 -by(Blast_tac 1);
    5.32 +by (asm_full_simp_tac (simpset() addsimps [step_def]) 1);
    5.33 +by (Blast_tac 1);
    5.34  qed_spec_mp "espclosure_DA_delta_is_steps";
    5.35  
    5.36  Goalw [nae2da_def]
    5.37   "fin (nae2da A) Q = (? q : (eps A)^* ^^ Q. fin A q)";
    5.38 -by(Simp_tac 1);
    5.39 +by (Simp_tac 1);
    5.40  val lemma = result();
    5.41  
    5.42  Goalw [NAe.accepts_def,DA.accepts_def]
    5.43    "DA.accepts (nae2da A) w = NAe.accepts A w";
    5.44 -by(simp_tac (simpset() addsimps [lemma,espclosure_DA_delta_is_steps]) 1);
    5.45 -by(simp_tac (simpset() addsimps [nae2da_def]) 1);
    5.46 -by(Blast_tac 1);
    5.47 +by (simp_tac (simpset() addsimps [lemma,espclosure_DA_delta_is_steps]) 1);
    5.48 +by (simp_tac (simpset() addsimps [nae2da_def]) 1);
    5.49 +by (Blast_tac 1);
    5.50  qed "NAe_DA_equiv";
     6.1 --- a/src/HOL/Lex/DA.ML	Fri Jul 10 15:24:22 1998 +0200
     6.2 +++ b/src/HOL/Lex/DA.ML	Sun Jul 12 11:49:17 1998 +0200
     6.3 @@ -5,27 +5,27 @@
     6.4  *)
     6.5  
     6.6  Goalw [foldl2_def] "foldl2 f [] a = a";
     6.7 -by(Simp_tac 1);
     6.8 +by (Simp_tac 1);
     6.9  qed "foldl2_Nil";
    6.10  
    6.11  Goalw [foldl2_def] "foldl2 f (x#xs) a = foldl2 f xs (f x a)";
    6.12 -by(Simp_tac 1);
    6.13 +by (Simp_tac 1);
    6.14  qed "foldl2_Cons";
    6.15  
    6.16  Addsimps [foldl2_Nil,foldl2_Cons];
    6.17  
    6.18  Goalw [delta_def] "delta A [] s = s";
    6.19 -by(Simp_tac 1);
    6.20 +by (Simp_tac 1);
    6.21  qed "delta_Nil";
    6.22  
    6.23  Goalw [delta_def] "delta A (a#w) s = delta A w (next A a s)";
    6.24 -by(Simp_tac 1);
    6.25 +by (Simp_tac 1);
    6.26  qed "delta_Cons";
    6.27  
    6.28  Addsimps [delta_Nil,delta_Cons];
    6.29  
    6.30  Goal "!q ys. delta A (xs@ys) q = delta A ys (delta A xs q)";
    6.31 -by(induct_tac "xs" 1);
    6.32 +by (induct_tac "xs" 1);
    6.33  by (ALLGOALS Asm_simp_tac);
    6.34  qed "delta_append";
    6.35  Addsimps [delta_append];
     7.1 --- a/src/HOL/Lex/MaxChop.ML	Fri Jul 10 15:24:22 1998 +0200
     7.2 +++ b/src/HOL/Lex/MaxChop.ML	Sun Jul 12 11:49:17 1998 +0200
     7.3 @@ -7,12 +7,12 @@
     7.4  (* Termination of chop *)
     7.5  
     7.6  Goalw [reducing_def] "reducing(%qs. maxsplit P ([],qs) [] qs)";
     7.7 -by(asm_full_simp_tac (simpset() addsimps [maxsplit_eq]) 1);
     7.8 +by (asm_full_simp_tac (simpset() addsimps [maxsplit_eq]) 1);
     7.9  qed "reducing_maxsplit";
    7.10  
    7.11  val [tc] = chopr.tcs;
    7.12  goalw_cterm [reducing_def] (cterm_of (sign_of thy) (HOLogic.mk_Trueprop tc));
    7.13 -by(blast_tac (claset() addDs [sym]) 1);
    7.14 +by (blast_tac (claset() addDs [sym]) 1);
    7.15  val lemma = result();
    7.16  
    7.17  val chopr_rule = let val [chopr_rule] = chopr.rules in lemma RS chopr_rule end;
    7.18 @@ -22,85 +22,85 @@
    7.19  \                   in if pre=[] then ([],xs) \
    7.20  \                      else let (xss,zs) = chop splitf post \
    7.21  \                             in (pre#xss,zs))";
    7.22 -by(asm_simp_tac (simpset() addsimps [chopr_rule] addcongs [if_weak_cong]) 1);
    7.23 -by(simp_tac (simpset() addsimps [Let_def] addsplits [split_split]) 1);
    7.24 +by (asm_simp_tac (simpset() addsimps [chopr_rule] addcongs [if_weak_cong]) 1);
    7.25 +by (simp_tac (simpset() addsimps [Let_def] addsplits [split_split]) 1);
    7.26  qed "chop_rule";
    7.27  
    7.28  Goalw [is_maxsplitter_def,reducing_def]
    7.29   "is_maxsplitter P splitf ==> reducing splitf";
    7.30 -by(Asm_full_simp_tac 1);
    7.31 +by (Asm_full_simp_tac 1);
    7.32  qed "is_maxsplitter_reducing";
    7.33  
    7.34  Goal "is_maxsplitter P splitf ==> \
    7.35  \ !yss zs. chop splitf xs = (yss,zs) --> xs = concat yss @ zs";
    7.36 -by(res_inst_tac [("xs","xs")] length_induct 1);
    7.37 -by(asm_simp_tac (simpset() delsplits [split_if]
    7.38 +by (res_inst_tac [("xs","xs")] length_induct 1);
    7.39 +by (asm_simp_tac (simpset() delsplits [split_if]
    7.40                             addsimps [chop_rule,is_maxsplitter_reducing]
    7.41                             addcongs [if_weak_cong]) 1);
    7.42 -by(asm_full_simp_tac (simpset() addsimps [Let_def,is_maxsplitter_def]
    7.43 +by (asm_full_simp_tac (simpset() addsimps [Let_def,is_maxsplitter_def]
    7.44                                  addsplits [split_split]) 1);
    7.45  qed_spec_mp "chop_concat";
    7.46  
    7.47  Goal "is_maxsplitter P splitf ==> \
    7.48  \ !yss zs. chop splitf xs = (yss,zs) --> (!ys : set yss. ys ~= [])";
    7.49 -by(res_inst_tac [("xs","xs")] length_induct 1);
    7.50 -by(asm_simp_tac (simpset() addsimps [chop_rule,is_maxsplitter_reducing]
    7.51 +by (res_inst_tac [("xs","xs")] length_induct 1);
    7.52 +by (asm_simp_tac (simpset() addsimps [chop_rule,is_maxsplitter_reducing]
    7.53                             addcongs [if_weak_cong]) 1);
    7.54 -by(asm_full_simp_tac (simpset() addsimps [Let_def,is_maxsplitter_def]
    7.55 +by (asm_full_simp_tac (simpset() addsimps [Let_def,is_maxsplitter_def]
    7.56                                  addsplits [split_split]) 1);
    7.57 -by(simp_tac (simpset() addsimps [Let_def,maxsplit_eq]
    7.58 +by (simp_tac (simpset() addsimps [Let_def,maxsplit_eq]
    7.59                         addsplits [split_split]) 1);
    7.60 -be thin_rl 1;
    7.61 -by(strip_tac 1);
    7.62 -br ballI 1;
    7.63 -be exE 1;
    7.64 -be allE 1;
    7.65 -auto();
    7.66 +by (etac thin_rl 1);
    7.67 +by (strip_tac 1);
    7.68 +by (rtac ballI 1);
    7.69 +by (etac exE 1);
    7.70 +by (etac allE 1);
    7.71 +by Auto_tac;
    7.72  qed_spec_mp "chop_nonempty";
    7.73  
    7.74  val [prem] = goalw thy [is_maxchopper_def]
    7.75   "is_maxsplitter P splitf ==> is_maxchopper P (chop splitf)";
    7.76 -by(Clarify_tac 1);
    7.77 -br iffI 1;
    7.78 - br conjI 1;
    7.79 -  be (prem RS chop_concat) 1;
    7.80 - br conjI 1;
    7.81 -  be (prem RS chop_nonempty) 1;
    7.82 - be rev_mp 1;
    7.83 - by(stac (prem RS is_maxsplitter_reducing RS chop_rule) 1);
    7.84 - by(simp_tac (simpset() addsimps [Let_def,rewrite_rule[is_maxsplitter_def]prem]
    7.85 +by (Clarify_tac 1);
    7.86 +by (rtac iffI 1);
    7.87 + by (rtac conjI 1);
    7.88 +  by (etac (prem RS chop_concat) 1);
    7.89 + by (rtac conjI 1);
    7.90 +  by (etac (prem RS chop_nonempty) 1);
    7.91 + by (etac rev_mp 1);
    7.92 + by (stac (prem RS is_maxsplitter_reducing RS chop_rule) 1);
    7.93 + by (simp_tac (simpset() addsimps [Let_def,rewrite_rule[is_maxsplitter_def]prem]
    7.94                          addsplits [split_split]) 1);
    7.95 - by(Clarify_tac 1);
    7.96 - br conjI 1;
    7.97 -  by(Clarify_tac 1);
    7.98 -  by(Asm_full_simp_tac 1);
    7.99 - by(Clarify_tac 1);
   7.100 - by(Asm_full_simp_tac 1);
   7.101 - by(forward_tac [prem RS chop_concat] 1);
   7.102 - by(Clarify_tac 1);
   7.103 - ba 1;
   7.104 -by(stac (prem RS is_maxsplitter_reducing RS chop_rule) 1);
   7.105 - by(simp_tac (simpset() addsimps [Let_def,rewrite_rule[is_maxsplitter_def]prem]
   7.106 + by (Clarify_tac 1);
   7.107 + by (rtac conjI 1);
   7.108 +  by (Clarify_tac 1);
   7.109 +  by (Asm_full_simp_tac 1);
   7.110 + by (Clarify_tac 1);
   7.111 + by (Asm_full_simp_tac 1);
   7.112 + by (forward_tac [prem RS chop_concat] 1);
   7.113 + by (Clarify_tac 1);
   7.114 + by (assume_tac 1);
   7.115 +by (stac (prem RS is_maxsplitter_reducing RS chop_rule) 1);
   7.116 + by (simp_tac (simpset() addsimps [Let_def,rewrite_rule[is_maxsplitter_def]prem]
   7.117                          addsplits [split_split]) 1);
   7.118 -by(Clarify_tac 1);
   7.119 -br conjI 1;
   7.120 - by(Clarify_tac 1);
   7.121 - by(exhaust_tac "yss" 1);
   7.122 -  by(Asm_simp_tac 1);
   7.123 - by(Asm_full_simp_tac 1);
   7.124 - by(full_simp_tac (simpset() addsimps [is_maxpref_def]) 1);
   7.125 - by(blast_tac (claset() addIs [prefix_append RS iffD2]) 1);
   7.126 -by(exhaust_tac "yss" 1);
   7.127 - by(Asm_full_simp_tac 1);
   7.128 - by(full_simp_tac (simpset() addsimps [is_maxpref_def]) 1);
   7.129 - by(blast_tac (claset() addIs [prefix_append RS iffD2]) 1);
   7.130 -by(Clarify_tac 1);
   7.131 -by(Asm_full_simp_tac 1);
   7.132 -by(subgoal_tac "x=a" 1);
   7.133 - by(Clarify_tac 1);
   7.134 - by(Asm_full_simp_tac 1);
   7.135 -by(rotate_tac ~2 1);
   7.136 -by(Asm_full_simp_tac 1);
   7.137 -by(full_simp_tac (simpset() addsimps [is_maxpref_def]) 1);
   7.138 -by(blast_tac (claset() addIs [prefix_append RS iffD2,prefix_antisym]) 1);
   7.139 +by (Clarify_tac 1);
   7.140 +by (rtac conjI 1);
   7.141 + by (Clarify_tac 1);
   7.142 + by (exhaust_tac "yss" 1);
   7.143 +  by (Asm_simp_tac 1);
   7.144 + by (Asm_full_simp_tac 1);
   7.145 + by (full_simp_tac (simpset() addsimps [is_maxpref_def]) 1);
   7.146 + by (blast_tac (claset() addIs [prefix_append RS iffD2]) 1);
   7.147 +by (exhaust_tac "yss" 1);
   7.148 + by (Asm_full_simp_tac 1);
   7.149 + by (full_simp_tac (simpset() addsimps [is_maxpref_def]) 1);
   7.150 + by (blast_tac (claset() addIs [prefix_append RS iffD2]) 1);
   7.151 +by (Clarify_tac 1);
   7.152 +by (Asm_full_simp_tac 1);
   7.153 +by (subgoal_tac "x=a" 1);
   7.154 + by (Clarify_tac 1);
   7.155 + by (Asm_full_simp_tac 1);
   7.156 +by (rotate_tac ~2 1);
   7.157 +by (Asm_full_simp_tac 1);
   7.158 +by (full_simp_tac (simpset() addsimps [is_maxpref_def]) 1);
   7.159 +by (blast_tac (claset() addIs [prefix_append RS iffD2,prefix_antisym]) 1);
   7.160  qed "is_maxchopper_chop";
     8.1 --- a/src/HOL/Lex/MaxPrefix.ML	Fri Jul 10 15:24:22 1998 +0200
     8.2 +++ b/src/HOL/Lex/MaxPrefix.ML	Sun Jul 12 11:49:17 1998 +0200
     8.3 @@ -9,56 +9,56 @@
     8.4  \ (maxsplit P res ps qs = (xs,ys)) = \
     8.5  \ (if ? us. us <= qs & P(ps@us) then xs@ys=ps@qs & is_maxpref P xs (ps@qs) \
     8.6  \  else (xs,ys)=res)";
     8.7 -by(induct_tac "qs" 1);
     8.8 - by(simp_tac (simpset() addsplits [split_if]) 1);
     8.9 - by(Blast_tac 1);
    8.10 -by(Asm_simp_tac 1);
    8.11 -be thin_rl 1;
    8.12 -by(Clarify_tac 1);
    8.13 -by(case_tac "? us. us <= list & P (ps @ a # us)" 1);
    8.14 - by(Asm_simp_tac 1);
    8.15 - by(subgoal_tac "? us. us <= a # list & P (ps @ us)" 1);
    8.16 -  by(Asm_simp_tac 1);
    8.17 - by(blast_tac (claset() addIs [prefix_Cons RS iffD2]) 1);
    8.18 -by(subgoal_tac "~P(ps@[a])" 1);
    8.19 - by(Blast_tac 2);
    8.20 -by(Asm_simp_tac 1);
    8.21 -by(case_tac "? us. us <= a#list & P (ps @ us)" 1);
    8.22 - by(Asm_simp_tac 1);
    8.23 - by(Clarify_tac 1);
    8.24 - by(exhaust_tac "us" 1);
    8.25 -  br iffI 1;
    8.26 -   by(asm_full_simp_tac (simpset() addsimps [prefix_Cons,prefix_append]) 1);
    8.27 -   by(Blast_tac 1);
    8.28 -  by(asm_full_simp_tac (simpset() addsimps [prefix_Cons,prefix_append]) 1);
    8.29 -  by(Clarify_tac 1);
    8.30 -  be disjE 1;
    8.31 -   by(fast_tac (claset() addDs [prefix_antisym]) 1);
    8.32 -  by(Clarify_tac 1);
    8.33 -  be disjE 1;
    8.34 -   by(Clarify_tac 1);
    8.35 -   by(Asm_full_simp_tac 1);
    8.36 -  be disjE 1;
    8.37 -   by(Clarify_tac 1);
    8.38 -   by(Asm_full_simp_tac 1);
    8.39 -  by(Blast_tac 1);
    8.40 - by(Asm_full_simp_tac 1);
    8.41 -by(subgoal_tac "~P(ps)" 1);
    8.42 -by(Asm_simp_tac 1);
    8.43 -by(fast_tac (claset() addss simpset()) 1);
    8.44 +by (induct_tac "qs" 1);
    8.45 + by (simp_tac (simpset() addsplits [split_if]) 1);
    8.46 + by (Blast_tac 1);
    8.47 +by (Asm_simp_tac 1);
    8.48 +by (etac thin_rl 1);
    8.49 +by (Clarify_tac 1);
    8.50 +by (case_tac "? us. us <= list & P (ps @ a # us)" 1);
    8.51 + by (Asm_simp_tac 1);
    8.52 + by (subgoal_tac "? us. us <= a # list & P (ps @ us)" 1);
    8.53 +  by (Asm_simp_tac 1);
    8.54 + by (blast_tac (claset() addIs [prefix_Cons RS iffD2]) 1);
    8.55 +by (subgoal_tac "~P(ps@[a])" 1);
    8.56 + by (Blast_tac 2);
    8.57 +by (Asm_simp_tac 1);
    8.58 +by (case_tac "? us. us <= a#list & P (ps @ us)" 1);
    8.59 + by (Asm_simp_tac 1);
    8.60 + by (Clarify_tac 1);
    8.61 + by (exhaust_tac "us" 1);
    8.62 +  by (rtac iffI 1);
    8.63 +   by (asm_full_simp_tac (simpset() addsimps [prefix_Cons,prefix_append]) 1);
    8.64 +   by (Blast_tac 1);
    8.65 +  by (asm_full_simp_tac (simpset() addsimps [prefix_Cons,prefix_append]) 1);
    8.66 +  by (Clarify_tac 1);
    8.67 +  by (etac disjE 1);
    8.68 +   by (fast_tac (claset() addDs [prefix_antisym]) 1);
    8.69 +  by (Clarify_tac 1);
    8.70 +  by (etac disjE 1);
    8.71 +   by (Clarify_tac 1);
    8.72 +   by (Asm_full_simp_tac 1);
    8.73 +  by (etac disjE 1);
    8.74 +   by (Clarify_tac 1);
    8.75 +   by (Asm_full_simp_tac 1);
    8.76 +  by (Blast_tac 1);
    8.77 + by (Asm_full_simp_tac 1);
    8.78 +by (subgoal_tac "~P(ps)" 1);
    8.79 +by (Asm_simp_tac 1);
    8.80 +by (fast_tac (claset() addss simpset()) 1);
    8.81  qed_spec_mp "maxsplit_lemma";
    8.82  Addsplits [split_if];
    8.83  
    8.84  Goalw [is_maxpref_def]
    8.85   "~(? us. us<=xs & P us) ==> is_maxpref P ps xs = (ps = [])";
    8.86 -by(Blast_tac 1);
    8.87 +by (Blast_tac 1);
    8.88  qed "is_maxpref_Nil";
    8.89  Addsimps [is_maxpref_Nil];
    8.90  
    8.91  Goalw [is_maxsplitter_def]
    8.92   "is_maxsplitter P (%xs. maxsplit P ([],xs) [] xs)";
    8.93 -by(simp_tac (simpset() addsimps [maxsplit_lemma]) 1);
    8.94 -by(fast_tac (claset() addss simpset()) 1);
    8.95 +by (simp_tac (simpset() addsimps [maxsplit_lemma]) 1);
    8.96 +by (fast_tac (claset() addss simpset()) 1);
    8.97  qed "is_maxsplitter_maxsplit";
    8.98  
    8.99  val maxsplit_eq = rewrite_rule [is_maxsplitter_def] is_maxsplitter_maxsplit;
     9.1 --- a/src/HOL/Lex/NAe.ML	Fri Jul 10 15:24:22 1998 +0200
     9.2 +++ b/src/HOL/Lex/NAe.ML	Sun Jul 12 11:49:17 1998 +0200
     9.3 @@ -6,13 +6,13 @@
     9.4  
     9.5  Goal "steps A w O (eps A)^* = steps A w";
     9.6  by (exhaust_tac "w" 1);
     9.7 -by(ALLGOALS(asm_simp_tac (simpset() addsimps [O_assoc])));
     9.8 +by (ALLGOALS(asm_simp_tac (simpset() addsimps [O_assoc])));
     9.9  qed_spec_mp "steps_epsclosure";
    9.10  Addsimps [steps_epsclosure];
    9.11  
    9.12  Goal "[| (p,q) : (eps A)^*; (q,r) : steps A w |] ==> (p,r) : steps A w";
    9.13 -by(rtac (steps_epsclosure RS equalityE) 1);
    9.14 -by(Blast_tac 1);
    9.15 +by (rtac (steps_epsclosure RS equalityE) 1);
    9.16 +by (Blast_tac 1);
    9.17  qed "in_steps_epsclosure";
    9.18  
    9.19  Goal "(eps A)^* O steps A w = steps A w";
    9.20 @@ -22,19 +22,19 @@
    9.21  qed "epsclosure_steps";
    9.22  
    9.23  Goal "[| (p,q) : steps A w; (q,r) : (eps A)^* |] ==> (p,r) : steps A w";
    9.24 -by(rtac (epsclosure_steps RS equalityE) 1);
    9.25 -by(Blast_tac 1);
    9.26 +by (rtac (epsclosure_steps RS equalityE) 1);
    9.27 +by (Blast_tac 1);
    9.28  qed "in_epsclosure_steps";
    9.29  
    9.30  Goal "steps A (v@w) = steps A w  O  steps A v";
    9.31  by (induct_tac "v" 1);
    9.32 -by(ALLGOALS(asm_simp_tac (simpset() addsimps [O_assoc])));
    9.33 +by (ALLGOALS(asm_simp_tac (simpset() addsimps [O_assoc])));
    9.34  qed "steps_append";
    9.35  Addsimps [steps_append];
    9.36  
    9.37  Goal "(p,r) : steps A (v@w) = ((p,r) : (steps A w O steps A v))";
    9.38 -by(rtac (steps_append RS equalityE) 1);
    9.39 -by(Blast_tac 1);
    9.40 +by (rtac (steps_append RS equalityE) 1);
    9.41 +by (Blast_tac 1);
    9.42  qed "in_steps_append";
    9.43  AddIffs [in_steps_append];
    9.44  
    9.45 @@ -44,6 +44,6 @@
    9.46  by (induct_tac "w" 1);
    9.47   by (Simp_tac 1);
    9.48  by (asm_simp_tac (simpset() addsimps [comp_def,step_def]) 1);
    9.49 -by(Blast_tac 1);
    9.50 +by (Blast_tac 1);
    9.51  qed_spec_mp "steps_equiv_delta";
    9.52  *)
    10.1 --- a/src/HOL/Lex/Prefix.ML	Fri Jul 10 15:24:22 1998 +0200
    10.2 +++ b/src/HOL/Lex/Prefix.ML	Sun Jul 12 11:49:17 1998 +0200
    10.3 @@ -15,18 +15,18 @@
    10.4  (** <= is a partial order: **)
    10.5  
    10.6  Goalw [prefix_def] "xs <= (xs::'a list)";
    10.7 -by(Simp_tac 1);
    10.8 +by (Simp_tac 1);
    10.9  qed "prefix_refl";
   10.10  AddIffs[prefix_refl];
   10.11  
   10.12  Goalw [prefix_def] "!!xs::'a list. [| xs <= ys; ys <= zs |] ==> xs <= zs";
   10.13 -by(Clarify_tac 1);
   10.14 -by(Simp_tac 1);
   10.15 +by (Clarify_tac 1);
   10.16 +by (Simp_tac 1);
   10.17  qed "prefix_trans";
   10.18  
   10.19  Goalw [prefix_def] "!!xs::'a list. [| xs <= ys; ys <= xs |] ==> xs = ys";
   10.20 -by(Clarify_tac 1);
   10.21 -by(Asm_full_simp_tac 1);
   10.22 +by (Clarify_tac 1);
   10.23 +by (Asm_full_simp_tac 1);
   10.24  qed "prefix_antisym";
   10.25  
   10.26  (** recursion equations **)
   10.27 @@ -44,17 +44,17 @@
   10.28  Addsimps [prefix_Nil];
   10.29  
   10.30  Goalw [prefix_def] "(xs <= ys@[y]) = (xs = ys@[y] | xs <= ys)";
   10.31 -br iffI 1;
   10.32 - be exE 1;
   10.33 - by(rename_tac "zs" 1);
   10.34 - by(res_inst_tac [("xs","zs")] rev_exhaust 1);
   10.35 -  by(Asm_full_simp_tac 1);
   10.36 - by(hyp_subst_tac 1);
   10.37 - by(asm_full_simp_tac (simpset() delsimps [append_assoc]
   10.38 +by (rtac iffI 1);
   10.39 + by (etac exE 1);
   10.40 + by (rename_tac "zs" 1);
   10.41 + by (res_inst_tac [("xs","zs")] rev_exhaust 1);
   10.42 +  by (Asm_full_simp_tac 1);
   10.43 + by (hyp_subst_tac 1);
   10.44 + by (asm_full_simp_tac (simpset() delsimps [append_assoc]
   10.45                                   addsimps [append_assoc RS sym])1);
   10.46 -be disjE 1;
   10.47 - by(Asm_simp_tac 1);
   10.48 -by(Clarify_tac 1);
   10.49 +by (etac disjE 1);
   10.50 + by (Asm_simp_tac 1);
   10.51 +by (Clarify_tac 1);
   10.52  by (Simp_tac 1);
   10.53  qed "prefix_snoc";
   10.54  Addsimps [prefix_snoc];
   10.55 @@ -67,7 +67,7 @@
   10.56  
   10.57  Goal "(xs@ys <= xs@zs) = (ys <= zs)";
   10.58  by (induct_tac "xs" 1);
   10.59 -by(ALLGOALS Asm_simp_tac);
   10.60 +by (ALLGOALS Asm_simp_tac);
   10.61  qed "same_prefix_prefix";
   10.62  Addsimps [same_prefix_prefix];
   10.63  
   10.64 @@ -75,7 +75,7 @@
   10.65   [simplify (simpset()) (read_instantiate [("zs","[]")] same_prefix_prefix)];
   10.66  
   10.67  Goalw [prefix_def] "xs <= ys ==> xs <= ys@zs";
   10.68 -by(Clarify_tac 1);
   10.69 +by (Clarify_tac 1);
   10.70  by (Simp_tac 1);
   10.71  qed "prefix_prefix";
   10.72  Addsimps [prefix_prefix];
   10.73 @@ -90,11 +90,11 @@
   10.74  qed "prefix_Cons";
   10.75  
   10.76  Goal "(xs <= ys@zs) = (xs <= ys | (? us. xs = ys@us & us <= zs))";
   10.77 -by(res_inst_tac [("xs","zs")] rev_induct 1);
   10.78 - by(Simp_tac 1);
   10.79 - by(Blast_tac 1);
   10.80 -by(asm_full_simp_tac (simpset() delsimps [append_assoc]
   10.81 +by (res_inst_tac [("xs","zs")] rev_induct 1);
   10.82 + by (Simp_tac 1);
   10.83 + by (Blast_tac 1);
   10.84 +by (asm_full_simp_tac (simpset() delsimps [append_assoc]
   10.85                                  addsimps [append_assoc RS sym])1);
   10.86 -by(Simp_tac 1);
   10.87 -by(Blast_tac 1);
   10.88 +by (Simp_tac 1);
   10.89 +by (Blast_tac 1);
   10.90  qed "prefix_append";
    11.1 --- a/src/HOL/Lex/RegExp2NAe.ML	Fri Jul 10 15:24:22 1998 +0200
    11.2 +++ b/src/HOL/Lex/RegExp2NAe.ML	Sun Jul 12 11:49:17 1998 +0200
    11.3 @@ -9,43 +9,43 @@
    11.4  (******************************************************)
    11.5  
    11.6  Goalw [atom_def] "(fin (atom a) q) = (q = [False])";
    11.7 -by(Simp_tac 1);
    11.8 +by (Simp_tac 1);
    11.9  qed "fin_atom";
   11.10  
   11.11  Goalw [atom_def] "start (atom a) = [True]";
   11.12 -by(Simp_tac 1);
   11.13 +by (Simp_tac 1);
   11.14  qed "start_atom";
   11.15  
   11.16  (* Use {x. False} = {}? *)
   11.17  
   11.18  Goalw [atom_def,step_def]
   11.19   "eps(atom a) = {}";
   11.20 -by(Simp_tac 1);
   11.21 +by (Simp_tac 1);
   11.22  by (Blast_tac 1);
   11.23  qed "eps_atom";
   11.24  Addsimps [eps_atom];
   11.25  
   11.26  Goalw [atom_def,step_def]
   11.27   "(p,q) : step (atom a) (Some b) = (p=[True] & q=[False] & b=a)";
   11.28 -by(Simp_tac 1);
   11.29 +by (Simp_tac 1);
   11.30  qed "in_step_atom_Some";
   11.31  Addsimps [in_step_atom_Some];
   11.32  
   11.33  Goal "([False],[False]) : steps (atom a) w = (w = [])";
   11.34  by (induct_tac "w" 1);
   11.35 - by(Simp_tac 1);
   11.36 -by(asm_simp_tac (simpset() addsimps [comp_def]) 1);
   11.37 + by (Simp_tac 1);
   11.38 +by (asm_simp_tac (simpset() addsimps [comp_def]) 1);
   11.39  qed "False_False_in_steps_atom";
   11.40  
   11.41  Goal "(start (atom a), [False]) : steps (atom a) w = (w = [a])";
   11.42  by (induct_tac "w" 1);
   11.43 - by(asm_simp_tac (simpset() addsimps [start_atom,rtrancl_empty]) 1);
   11.44 -by(asm_full_simp_tac (simpset()
   11.45 + by (asm_simp_tac (simpset() addsimps [start_atom,rtrancl_empty]) 1);
   11.46 +by (asm_full_simp_tac (simpset()
   11.47       addsimps [False_False_in_steps_atom,comp_def,start_atom]) 1);
   11.48  qed "start_fin_in_steps_atom";
   11.49  
   11.50  Goal "accepts (atom a) w = (w = [a])";
   11.51 -by(simp_tac(simpset() addsimps
   11.52 +by (simp_tac(simpset() addsimps
   11.53         [accepts_def,start_fin_in_steps_atom,fin_atom]) 1);
   11.54  qed "accepts_atom";
   11.55  
   11.56 @@ -73,13 +73,13 @@
   11.57  Goalw [union_def,step_def]
   11.58  "!L R. (True#p,q) : step (union L R) a = (? r. q = True#r & (p,r) : step L a)";
   11.59  by (Simp_tac 1);
   11.60 -by(Blast_tac 1);
   11.61 +by (Blast_tac 1);
   11.62  qed_spec_mp "True_in_step_union";
   11.63  
   11.64  Goalw [union_def,step_def]
   11.65  "!L R. (False#p,q) : step (union L R) a = (? r. q = False#r & (p,r) : step R a)";
   11.66  by (Simp_tac 1);
   11.67 -by(Blast_tac 1);
   11.68 +by (Blast_tac 1);
   11.69  qed_spec_mp "False_in_step_union";
   11.70  
   11.71  AddIffs [True_in_step_union,False_in_step_union];
   11.72 @@ -89,45 +89,45 @@
   11.73  Goal
   11.74   "(tp,tq) : (eps(union L R))^* ==> \
   11.75  \ !p. tp = True#p --> (? q. (p,q) : (eps L)^* & tq = True#q)";
   11.76 -be rtrancl_induct 1;
   11.77 - by(Blast_tac 1);
   11.78 -by(Clarify_tac 1);
   11.79 -by(Asm_full_simp_tac 1);
   11.80 -by(blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
   11.81 +by (etac rtrancl_induct 1);
   11.82 + by (Blast_tac 1);
   11.83 +by (Clarify_tac 1);
   11.84 +by (Asm_full_simp_tac 1);
   11.85 +by (blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
   11.86  val lemma1a = result();
   11.87  
   11.88  Goal
   11.89   "(tp,tq) : (eps(union L R))^* ==> \
   11.90  \ !p. tp = False#p --> (? q. (p,q) : (eps R)^* & tq = False#q)";
   11.91 -be rtrancl_induct 1;
   11.92 - by(Blast_tac 1);
   11.93 -by(Clarify_tac 1);
   11.94 -by(Asm_full_simp_tac 1);
   11.95 -by(blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
   11.96 +by (etac rtrancl_induct 1);
   11.97 + by (Blast_tac 1);
   11.98 +by (Clarify_tac 1);
   11.99 +by (Asm_full_simp_tac 1);
  11.100 +by (blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
  11.101  val lemma1b = result();
  11.102  
  11.103  Goal
  11.104   "(p,q) : (eps L)^*  ==> (True#p, True#q) : (eps(union L R))^*";
  11.105 -be rtrancl_induct 1;
  11.106 - by(Blast_tac 1);
  11.107 -by(blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
  11.108 +by (etac rtrancl_induct 1);
  11.109 + by (Blast_tac 1);
  11.110 +by (blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
  11.111  val lemma2a = result();
  11.112  
  11.113  Goal
  11.114   "(p,q) : (eps R)^*  ==> (False#p, False#q) : (eps(union L R))^*";
  11.115 -be rtrancl_induct 1;
  11.116 - by(Blast_tac 1);
  11.117 -by(blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
  11.118 +by (etac rtrancl_induct 1);
  11.119 + by (Blast_tac 1);
  11.120 +by (blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
  11.121  val lemma2b = result();
  11.122  
  11.123  Goal
  11.124   "(True#p,q) : (eps(union L R))^* = (? r. q = True#r & (p,r) : (eps L)^*)";
  11.125 -by(blast_tac (claset() addDs [lemma1a,lemma2a]) 1);
  11.126 +by (blast_tac (claset() addDs [lemma1a,lemma2a]) 1);
  11.127  qed "True_epsclosure_union";
  11.128  
  11.129  Goal
  11.130   "(False#p,q) : (eps(union L R))^* = (? r. q = False#r & (p,r) : (eps R)^*)";
  11.131 -by(blast_tac (claset() addDs [lemma1b,lemma2b]) 1);
  11.132 +by (blast_tac (claset() addDs [lemma1b,lemma2b]) 1);
  11.133  qed "False_epsclosure_union";
  11.134  
  11.135  AddIffs [True_epsclosure_union,False_epsclosure_union];
  11.136 @@ -139,7 +139,7 @@
  11.137  by (induct_tac "w" 1);
  11.138  by (ALLGOALS Asm_simp_tac);
  11.139  (* Blast_tac produces PROOF FAILED for depth 8 *)
  11.140 -by(Fast_tac 1);
  11.141 +by (Fast_tac 1);
  11.142  qed_spec_mp "lift_True_over_steps_union";
  11.143  
  11.144  Goal 
  11.145 @@ -147,7 +147,7 @@
  11.146  by (induct_tac "w" 1);
  11.147  by (ALLGOALS Asm_simp_tac);
  11.148  (* Blast_tac produces PROOF FAILED for depth 8 *)
  11.149 -by(Fast_tac 1);
  11.150 +by (Fast_tac 1);
  11.151  qed_spec_mp "lift_False_over_steps_union";
  11.152  
  11.153  AddIffs [lift_True_over_steps_union,lift_False_over_steps_union];
  11.154 @@ -157,19 +157,19 @@
  11.155  
  11.156  Goal
  11.157   "R^* = id Un (R^* O R)";
  11.158 -by(rtac set_ext 1);
  11.159 -by(split_all_tac 1);
  11.160 -by(rtac iffI 1);
  11.161 - be rtrancl_induct 1;
  11.162 -  by(Blast_tac 1);
  11.163 - by(blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
  11.164 -by(blast_tac (claset() addIs [rtrancl_into_rtrancl2]) 1);
  11.165 +by (rtac set_ext 1);
  11.166 +by (split_all_tac 1);
  11.167 +by (rtac iffI 1);
  11.168 + by (etac rtrancl_induct 1);
  11.169 +  by (Blast_tac 1);
  11.170 + by (blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
  11.171 +by (blast_tac (claset() addIs [rtrancl_into_rtrancl2]) 1);
  11.172  qed "unfold_rtrancl2";
  11.173  
  11.174  Goal
  11.175   "(p,q) : R^* = (q = p | (? r. (p,r) : R & (r,q) : R^*))";
  11.176 -by(rtac (unfold_rtrancl2 RS equalityE) 1);
  11.177 -by(Blast_tac 1);
  11.178 +by (rtac (unfold_rtrancl2 RS equalityE) 1);
  11.179 +by (Blast_tac 1);
  11.180  qed "in_unfold_rtrancl2";
  11.181  
  11.182  val epsclosure_start_step_union =
  11.183 @@ -179,13 +179,13 @@
  11.184  Goalw [union_def,step_def]
  11.185   "!L R. (start(union L R),q) : eps(union L R) = \
  11.186  \       (q = True#start L | q = False#start R)";
  11.187 -by(Simp_tac 1);
  11.188 +by (Simp_tac 1);
  11.189  qed_spec_mp "start_eps_union";
  11.190  AddIffs [start_eps_union];
  11.191  
  11.192  Goalw [union_def,step_def]
  11.193   "!L R. (start(union L R),q) ~: step (union L R) (Some a)";
  11.194 -by(Simp_tac 1);
  11.195 +by (Simp_tac 1);
  11.196  qed_spec_mp "not_start_step_union_Some";
  11.197  AddIffs [not_start_step_union_Some];
  11.198  
  11.199 @@ -197,54 +197,54 @@
  11.200  by (exhaust_tac "w" 1);
  11.201   by (Asm_simp_tac 1);
  11.202   (* Blast_tac produces PROOF FAILED! *)
  11.203 - by(Fast_tac 1);
  11.204 + by (Fast_tac 1);
  11.205  by (Asm_simp_tac 1);
  11.206  (* The goal is now completely dual to the first one.
  11.207     Fast/Best_tac don't return. Blast_tac produces PROOF FAILED!
  11.208     The lemmas used in the explicit proof are part of the claset already!
  11.209  *)
  11.210 -br iffI 1;
  11.211 - by(Blast_tac 1);
  11.212 -by(Clarify_tac 1);
  11.213 -be disjE 1;
  11.214 - by(Blast_tac 1);
  11.215 -by(Clarify_tac 1);
  11.216 -br compI 1;
  11.217 -br compI 1;
  11.218 -br (epsclosure_start_step_union RS iffD2) 1;
  11.219 -br disjI2 1;
  11.220 -br exI 1;
  11.221 -br conjI 1;
  11.222 -br (start_eps_union RS iffD2) 1;
  11.223 -br disjI2 1;
  11.224 -br refl 1;
  11.225 -by(Clarify_tac 1);
  11.226 -br exI 1;
  11.227 -br conjI 1;
  11.228 -br refl 1;
  11.229 -ba 1;
  11.230 -by(Clarify_tac 1);
  11.231 -br exI 1;
  11.232 -br conjI 1;
  11.233 -br refl 1;
  11.234 -ba 1;
  11.235 -by(Clarify_tac 1);
  11.236 -br exI 1;
  11.237 -br conjI 1;
  11.238 -br refl 1;
  11.239 -ba 1;
  11.240 +by (rtac iffI 1);
  11.241 + by (Blast_tac 1);
  11.242 +by (Clarify_tac 1);
  11.243 +by (etac disjE 1);
  11.244 + by (Blast_tac 1);
  11.245 +by (Clarify_tac 1);
  11.246 +by (rtac compI 1);
  11.247 +by (rtac compI 1);
  11.248 +by (rtac (epsclosure_start_step_union RS iffD2) 1);
  11.249 +by (rtac disjI2 1);
  11.250 +by (rtac exI 1);
  11.251 +by (rtac conjI 1);
  11.252 +by (rtac (start_eps_union RS iffD2) 1);
  11.253 +by (rtac disjI2 1);
  11.254 +by (rtac refl 1);
  11.255 +by (Clarify_tac 1);
  11.256 +by (rtac exI 1);
  11.257 +by (rtac conjI 1);
  11.258 +by (rtac refl 1);
  11.259 +by (assume_tac 1);
  11.260 +by (Clarify_tac 1);
  11.261 +by (rtac exI 1);
  11.262 +by (rtac conjI 1);
  11.263 +by (rtac refl 1);
  11.264 +by (assume_tac 1);
  11.265 +by (Clarify_tac 1);
  11.266 +by (rtac exI 1);
  11.267 +by (rtac conjI 1);
  11.268 +by (rtac refl 1);
  11.269 +by (assume_tac 1);
  11.270  qed "steps_union";
  11.271  
  11.272  Goalw [union_def]
  11.273   "!L R. ~ fin (union L R) (start(union L R))";
  11.274 -by(Simp_tac 1);
  11.275 +by (Simp_tac 1);
  11.276  qed_spec_mp "start_union_not_final";
  11.277  AddIffs [start_union_not_final];
  11.278  
  11.279  Goalw [accepts_def]
  11.280   "accepts (union L R) w = (accepts L w | accepts R w)";
  11.281  by (simp_tac (simpset() addsimps [steps_union]) 1);
  11.282 -auto();
  11.283 +by Auto_tac;
  11.284  qed "accepts_union";
  11.285  
  11.286  
  11.287 @@ -273,14 +273,14 @@
  11.288  \       ((? r. q=True#r & (p,r): step L a) | \
  11.289  \        (fin L p & a=None & q=False#start R))";
  11.290  by (Simp_tac 1);
  11.291 -by(Blast_tac 1);
  11.292 +by (Blast_tac 1);
  11.293  qed_spec_mp "True_step_conc";
  11.294  
  11.295  Goalw [conc_def,step_def]
  11.296   "!L R. (False#p,q) : step (conc L R) a = \
  11.297  \       (? r. q = False#r & (p,r) : step R a)";
  11.298  by (Simp_tac 1);
  11.299 -by(Blast_tac 1);
  11.300 +by (Blast_tac 1);
  11.301  qed_spec_mp "False_step_conc";
  11.302  
  11.303  AddIffs [True_step_conc, False_step_conc];
  11.304 @@ -290,24 +290,24 @@
  11.305  Goal
  11.306   "(tp,tq) : (eps(conc L R))^* ==> \
  11.307  \ !p. tp = False#p --> (? q. (p,q) : (eps R)^* & tq = False#q)";
  11.308 -by(etac rtrancl_induct 1);
  11.309 - by(Blast_tac 1);
  11.310 -by(blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
  11.311 +by (etac rtrancl_induct 1);
  11.312 + by (Blast_tac 1);
  11.313 +by (blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
  11.314  qed "lemma1b";
  11.315  
  11.316  Goal
  11.317   "(p,q) : (eps R)^* ==> (False#p, False#q) : (eps(conc L R))^*";
  11.318 -by(etac rtrancl_induct 1);
  11.319 - by(Blast_tac 1);
  11.320 -by(blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
  11.321 +by (etac rtrancl_induct 1);
  11.322 + by (Blast_tac 1);
  11.323 +by (blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
  11.324  val lemma2b = result();
  11.325  
  11.326  Goal
  11.327   "((False # p, q) : (eps (conc L R))^*) = \
  11.328  \ (? r. q = False # r & (p, r) : (eps R)^*)";
  11.329  by (rtac iffI 1);
  11.330 - by(blast_tac (claset() addDs [lemma1b]) 1);
  11.331 -by(blast_tac (claset() addDs [lemma2b]) 1);
  11.332 + by (blast_tac (claset() addDs [lemma1b]) 1);
  11.333 +by (blast_tac (claset() addDs [lemma2b]) 1);
  11.334  qed "False_epsclosure_conc";
  11.335  AddIffs [False_epsclosure_conc];
  11.336  
  11.337 @@ -319,7 +319,7 @@
  11.338   by (Simp_tac 1);
  11.339  by (Simp_tac 1);
  11.340  (* Blast_tac produces PROOF FAILED for depth 8 *)
  11.341 -by(Fast_tac 1);
  11.342 +by (Fast_tac 1);
  11.343  qed_spec_mp "False_steps_conc";
  11.344  AddIffs [False_steps_conc];
  11.345  
  11.346 @@ -327,17 +327,17 @@
  11.347  
  11.348  Goal
  11.349   "(p,q): (eps L)^* ==> (True#p,True#q) : (eps(conc L R))^*";
  11.350 -be rtrancl_induct 1;
  11.351 - by(Blast_tac 1);
  11.352 -by(blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
  11.353 +by (etac rtrancl_induct 1);
  11.354 + by (Blast_tac 1);
  11.355 +by (blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
  11.356  qed "True_True_eps_concI";
  11.357  
  11.358  Goal
  11.359   "!p. (p,q) : steps L w --> (True#p,True#q) : steps (conc L R) w";
  11.360 -by(induct_tac "w" 1);
  11.361 +by (induct_tac "w" 1);
  11.362   by (simp_tac (simpset() addsimps [True_True_eps_concI]) 1);
  11.363  by (Simp_tac 1);
  11.364 -by(blast_tac (claset() addIs [True_True_eps_concI]) 1);
  11.365 +by (blast_tac (claset() addIs [True_True_eps_concI]) 1);
  11.366  qed_spec_mp "True_True_steps_concI";
  11.367  
  11.368  Goal
  11.369 @@ -345,36 +345,36 @@
  11.370  \ !p. tp = True#p --> \
  11.371  \ (? q. tq = True#q & (p,q) : (eps L)^*) | \
  11.372  \ (? q r. tq = False#q & (p,r):(eps L)^* & fin L r & (start R,q) : (eps R)^*)";
  11.373 -by(etac rtrancl_induct 1);
  11.374 - by(Blast_tac 1);
  11.375 -by(blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
  11.376 +by (etac rtrancl_induct 1);
  11.377 + by (Blast_tac 1);
  11.378 +by (blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
  11.379  val lemma1a = result();
  11.380  
  11.381  Goal
  11.382   "(p, q) : (eps L)^* ==> (True#p, True#q) : (eps(conc L R))^*";
  11.383 -by(etac rtrancl_induct 1);
  11.384 - by(Blast_tac 1);
  11.385 -by(blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
  11.386 +by (etac rtrancl_induct 1);
  11.387 + by (Blast_tac 1);
  11.388 +by (blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
  11.389  val lemma2a = result();
  11.390  
  11.391  Goalw [conc_def,step_def]
  11.392   "!!L R. (p,q) : step R None ==> (False#p, False#q) : step (conc L R) None";
  11.393 -by(split_all_tac 1);
  11.394 +by (split_all_tac 1);
  11.395  by (Asm_full_simp_tac 1);
  11.396  val lemma = result();
  11.397  
  11.398  Goal
  11.399   "(p,q) : (eps R)^* ==> (False#p, False#q) : (eps(conc L R))^*";
  11.400 -by(etac rtrancl_induct 1);
  11.401 - by(Blast_tac 1);
  11.402 +by (etac rtrancl_induct 1);
  11.403 + by (Blast_tac 1);
  11.404  by (dtac lemma 1);
  11.405 -by(blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
  11.406 +by (blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
  11.407  val lemma2b = result();
  11.408  
  11.409  Goalw [conc_def,step_def]
  11.410   "!!L R. fin L p ==> (True#p, False#start R) : eps(conc L R)";
  11.411 -by(split_all_tac 1);
  11.412 -by(Asm_full_simp_tac 1);
  11.413 +by (split_all_tac 1);
  11.414 +by (Asm_full_simp_tac 1);
  11.415  qed "True_False_eps_concI";
  11.416  
  11.417  Goal
  11.418 @@ -382,16 +382,16 @@
  11.419  \ ((? r. (p,r) : (eps L)^* & q = True#r) | \
  11.420  \  (? r. (p,r) : (eps L)^* & fin L r & \
  11.421  \        (? s. (start R, s) : (eps R)^* & q = False#s)))";
  11.422 -by(rtac iffI 1);
  11.423 - by(blast_tac (claset() addDs [lemma1a]) 1);
  11.424 -be disjE 1;
  11.425 - by(blast_tac (claset() addIs [lemma2a]) 1);
  11.426 -by(Clarify_tac 1);
  11.427 -br (rtrancl_trans) 1;
  11.428 -be lemma2a 1;
  11.429 -br (rtrancl_into_rtrancl2) 1;
  11.430 -be True_False_eps_concI 1;
  11.431 -be lemma2b 1;
  11.432 +by (rtac iffI 1);
  11.433 + by (blast_tac (claset() addDs [lemma1a]) 1);
  11.434 +by (etac disjE 1);
  11.435 + by (blast_tac (claset() addIs [lemma2a]) 1);
  11.436 +by (Clarify_tac 1);
  11.437 +by (rtac (rtrancl_trans) 1);
  11.438 +by (etac lemma2a 1);
  11.439 +by (rtac (rtrancl_into_rtrancl2) 1);
  11.440 +by (etac True_False_eps_concI 1);
  11.441 +by (etac lemma2b 1);
  11.442  qed "True_epsclosure_conc";
  11.443  AddIffs [True_epsclosure_conc];
  11.444  
  11.445 @@ -402,29 +402,29 @@
  11.446  \     ((? r. (p,r) : steps L w & q = True#r)  | \
  11.447  \      (? u v. w = u@v & (? r. (p,r) : steps L u & fin L r & \
  11.448  \              (? s. (start R,s) : steps R v & q = False#s))))";
  11.449 -by(induct_tac "w" 1);
  11.450 - by(Simp_tac 1);
  11.451 -by(Simp_tac 1);
  11.452 -by(clarify_tac (claset() delrules [disjCI]) 1);
  11.453 - be disjE 1;
  11.454 - by(clarify_tac (claset() delrules [disjCI]) 1);
  11.455 - be disjE 1;
  11.456 -  by(clarify_tac (claset() delrules [disjCI]) 1);
  11.457 -  by(etac allE 1 THEN mp_tac 1);
  11.458 -  be disjE 1;
  11.459 +by (induct_tac "w" 1);
  11.460 + by (Simp_tac 1);
  11.461 +by (Simp_tac 1);
  11.462 +by (clarify_tac (claset() delrules [disjCI]) 1);
  11.463 + by (etac disjE 1);
  11.464 + by (clarify_tac (claset() delrules [disjCI]) 1);
  11.465 + by (etac disjE 1);
  11.466 +  by (clarify_tac (claset() delrules [disjCI]) 1);
  11.467 +  by (etac allE 1 THEN mp_tac 1);
  11.468 +  by (etac disjE 1);
  11.469     by (Blast_tac 1);
  11.470 -  br disjI2 1;
  11.471 +  by (rtac disjI2 1);
  11.472    by (Clarify_tac 1);
  11.473 -  by(Simp_tac 1);
  11.474 -  by(res_inst_tac[("x","a#u")] exI 1);
  11.475 -  by(Simp_tac 1);
  11.476 +  by (Simp_tac 1);
  11.477 +  by (res_inst_tac[("x","a#u")] exI 1);
  11.478 +  by (Simp_tac 1);
  11.479    by (Blast_tac 1);
  11.480   by (Blast_tac 1);
  11.481 -br disjI2 1;
  11.482 +by (rtac disjI2 1);
  11.483  by (Clarify_tac 1);
  11.484 -by(Simp_tac 1);
  11.485 -by(res_inst_tac[("x","[]")] exI 1);
  11.486 -by(Simp_tac 1);
  11.487 +by (Simp_tac 1);
  11.488 +by (res_inst_tac[("x","[]")] exI 1);
  11.489 +by (Simp_tac 1);
  11.490  by (Blast_tac 1);
  11.491  qed_spec_mp "True_steps_concD";
  11.492  
  11.493 @@ -433,7 +433,7 @@
  11.494  \ ((? r. (p,r) : steps L w & q = True#r)  | \
  11.495  \  (? u v. w = u@v & (? r. (p,r) : steps L u & fin L r & \
  11.496  \          (? s. (start R,s) : steps R v & q = False#s))))";
  11.497 -by(blast_tac (claset() addDs [True_steps_concD]
  11.498 +by (blast_tac (claset() addDs [True_steps_concD]
  11.499       addIs [True_True_steps_concI,in_steps_epsclosure,r_into_rtrancl]) 1);
  11.500  qed "True_steps_conc";
  11.501  
  11.502 @@ -441,7 +441,7 @@
  11.503  
  11.504  Goalw [conc_def]
  11.505    "!L R. start(conc L R) = True#start L";
  11.506 -by(Simp_tac 1);
  11.507 +by (Simp_tac 1);
  11.508  qed_spec_mp "start_conc";
  11.509  
  11.510  Goalw [conc_def]
  11.511 @@ -453,7 +453,7 @@
  11.512   "accepts (conc L R) w = (? u v. w = u@v & accepts L u & accepts R v)";
  11.513  by (simp_tac (simpset() addsimps
  11.514       [accepts_def,True_steps_conc,final_conc,start_conc]) 1);
  11.515 -by(Blast_tac 1);
  11.516 +by (Blast_tac 1);
  11.517  qed "accepts_conc";
  11.518  
  11.519  (******************************************************)
  11.520 @@ -463,26 +463,26 @@
  11.521  Goalw [star_def,step_def]
  11.522   "!A. (True#p,q) : eps(star A) = \
  11.523  \     ( (? r. q = True#r & (p,r) : eps A) | (fin A p & q = True#start A) )";
  11.524 -by(Simp_tac 1);
  11.525 -by(Blast_tac 1);
  11.526 +by (Simp_tac 1);
  11.527 +by (Blast_tac 1);
  11.528  qed_spec_mp "True_in_eps_star";
  11.529  AddIffs [True_in_eps_star];
  11.530  
  11.531  Goalw [star_def,step_def]
  11.532    "!A. (p,q) : step A a --> (True#p, True#q) : step (star A) a";
  11.533 -by(Simp_tac 1);
  11.534 +by (Simp_tac 1);
  11.535  qed_spec_mp "True_True_step_starI";
  11.536  
  11.537  Goal
  11.538    "(p,r) : (eps A)^* ==> (True#p, True#r) : (eps(star A))^*";
  11.539 -be rtrancl_induct 1;
  11.540 - by(Blast_tac 1);
  11.541 -by(blast_tac (claset() addIs [True_True_step_starI,rtrancl_into_rtrancl]) 1);
  11.542 +by (etac rtrancl_induct 1);
  11.543 + by (Blast_tac 1);
  11.544 +by (blast_tac (claset() addIs [True_True_step_starI,rtrancl_into_rtrancl]) 1);
  11.545  qed_spec_mp "True_True_eps_starI";
  11.546  
  11.547  Goalw [star_def,step_def]
  11.548   "!A. fin A p --> (True#p,True#start A) : eps(star A)";
  11.549 -by(Simp_tac 1);
  11.550 +by (Simp_tac 1);
  11.551  qed_spec_mp "True_start_eps_starI";
  11.552  
  11.553  Goal
  11.554 @@ -490,11 +490,11 @@
  11.555  \ (? r. ((p,r) : (eps A)^* | \
  11.556  \        (? q. (p,q) : (eps A)^* & fin A q & (start A,r) : (eps A)^*)) & \
  11.557  \       s = True#r))";
  11.558 -be rtrancl_induct 1;
  11.559 - by(Simp_tac 1);
  11.560 +by (etac rtrancl_induct 1);
  11.561 + by (Simp_tac 1);
  11.562  by (Clarify_tac 1);
  11.563  by (Asm_full_simp_tac 1);
  11.564 -by(blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
  11.565 +by (blast_tac (claset() addIs [rtrancl_into_rtrancl]) 1);
  11.566  val lemma = result();
  11.567  
  11.568  Goal
  11.569 @@ -502,20 +502,20 @@
  11.570  \ (? r. ((p,r) : (eps A)^* | \
  11.571  \        (? q. (p,q) : (eps A)^* & fin A q & (start A,r) : (eps A)^*)) & \
  11.572  \       s = True#r)";
  11.573 -br iffI 1;
  11.574 - bd lemma 1;
  11.575 - by(Blast_tac 1);
  11.576 +by (rtac iffI 1);
  11.577 + by (dtac lemma 1);
  11.578 + by (Blast_tac 1);
  11.579  (* Why can't blast_tac do the rest? *)
  11.580  by (Clarify_tac 1);
  11.581 -be disjE 1;
  11.582 -be True_True_eps_starI 1;
  11.583 +by (etac disjE 1);
  11.584 +by (etac True_True_eps_starI 1);
  11.585  by (Clarify_tac 1);
  11.586 -br rtrancl_trans 1;
  11.587 -be True_True_eps_starI 1;
  11.588 -br rtrancl_trans 1;
  11.589 -br r_into_rtrancl 1;
  11.590 -be True_start_eps_starI 1;
  11.591 -be True_True_eps_starI 1;
  11.592 +by (rtac rtrancl_trans 1);
  11.593 +by (etac True_True_eps_starI 1);
  11.594 +by (rtac rtrancl_trans 1);
  11.595 +by (rtac r_into_rtrancl 1);
  11.596 +by (etac True_start_eps_starI 1);
  11.597 +by (etac True_True_eps_starI 1);
  11.598  qed "True_eps_star";
  11.599  AddIffs [True_eps_star];
  11.600  
  11.601 @@ -524,8 +524,8 @@
  11.602  Goalw [star_def,step_def]
  11.603   "!A. (True#p,r): step (star A) (Some a) = \
  11.604  \     (? q. (p,q): step A (Some a) & r=True#q)";
  11.605 -by(Simp_tac 1);
  11.606 -by(Blast_tac 1);
  11.607 +by (Simp_tac 1);
  11.608 +by (Blast_tac 1);
  11.609  qed_spec_mp "True_step_star";
  11.610  AddIffs [True_step_star];
  11.611  
  11.612 @@ -538,44 +538,44 @@
  11.613  \ (? us v. w = concat us @ v & \
  11.614  \             (!u:set us. accepts A u) & \
  11.615  \             (? r. (start A,r) : steps A v & rr = True#r))";
  11.616 -by(res_inst_tac [("xs","w")] rev_induct 1);
  11.617 +by (res_inst_tac [("xs","w")] rev_induct 1);
  11.618   by (Asm_full_simp_tac 1);
  11.619   by (Clarify_tac 1);
  11.620 - by(res_inst_tac [("x","[]")] exI 1);
  11.621 - be disjE 1;
  11.622 + by (res_inst_tac [("x","[]")] exI 1);
  11.623 + by (etac disjE 1);
  11.624    by (Asm_simp_tac 1);
  11.625   by (Clarify_tac 1);
  11.626   by (Asm_simp_tac 1);
  11.627 -by(simp_tac (simpset() addsimps [O_assoc,epsclosure_steps]) 1);
  11.628 +by (simp_tac (simpset() addsimps [O_assoc,epsclosure_steps]) 1);
  11.629  by (Clarify_tac 1);
  11.630 -by(etac allE 1 THEN mp_tac 1);
  11.631 +by (etac allE 1 THEN mp_tac 1);
  11.632  by (Clarify_tac 1);
  11.633 -be disjE 1;
  11.634 - by(res_inst_tac [("x","us")] exI 1);
  11.635 - by(res_inst_tac [("x","v@[x]")] exI 1);
  11.636 - by(asm_simp_tac (simpset() addsimps [O_assoc,epsclosure_steps]) 1);
  11.637 - by(Blast_tac 1);
  11.638 +by (etac disjE 1);
  11.639 + by (res_inst_tac [("x","us")] exI 1);
  11.640 + by (res_inst_tac [("x","v@[x]")] exI 1);
  11.641 + by (asm_simp_tac (simpset() addsimps [O_assoc,epsclosure_steps]) 1);
  11.642 + by (Blast_tac 1);
  11.643  by (Clarify_tac 1);
  11.644 -by(res_inst_tac [("x","us@[v@[x]]")] exI 1);
  11.645 -by(res_inst_tac [("x","[]")] exI 1);
  11.646 -by(asm_full_simp_tac (simpset() addsimps [accepts_def]) 1);
  11.647 -by(Blast_tac 1);
  11.648 +by (res_inst_tac [("x","us@[v@[x]]")] exI 1);
  11.649 +by (res_inst_tac [("x","[]")] exI 1);
  11.650 +by (asm_full_simp_tac (simpset() addsimps [accepts_def]) 1);
  11.651 +by (Blast_tac 1);
  11.652  qed_spec_mp "True_start_steps_starD";
  11.653  
  11.654  Goal "!p. (p,q) : steps A w --> (True#p,True#q) : steps (star A) w";
  11.655 -by(induct_tac "w" 1);
  11.656 - by(Simp_tac 1);
  11.657 -by(Simp_tac 1);
  11.658 -by(blast_tac (claset() addIs [True_True_eps_starI,True_True_step_starI]) 1);
  11.659 +by (induct_tac "w" 1);
  11.660 + by (Simp_tac 1);
  11.661 +by (Simp_tac 1);
  11.662 +by (blast_tac (claset() addIs [True_True_eps_starI,True_True_step_starI]) 1);
  11.663  qed_spec_mp "True_True_steps_starI";
  11.664  
  11.665  Goalw [accepts_def]
  11.666   "(!u : set us. accepts A u) --> \
  11.667  \ (True#start A,True#start A) : steps (star A) (concat us)";
  11.668 -by(induct_tac "us" 1);
  11.669 - by(Simp_tac 1);
  11.670 -by(Simp_tac 1);
  11.671 -by(blast_tac (claset() addIs [True_True_steps_starI,True_start_eps_starI,r_into_rtrancl,in_epsclosure_steps]) 1);
  11.672 +by (induct_tac "us" 1);
  11.673 + by (Simp_tac 1);
  11.674 +by (Simp_tac 1);
  11.675 +by (blast_tac (claset() addIs [True_True_steps_starI,True_start_eps_starI,r_into_rtrancl,in_epsclosure_steps]) 1);
  11.676  qed_spec_mp "steps_star_cycle";
  11.677  
  11.678  (* Better stated directly with start(star A)? Loop in star A back to start(star A)?*)
  11.679 @@ -584,18 +584,18 @@
  11.680  \ (? us v. w = concat us @ v & \
  11.681  \             (!u:set us. accepts A u) & \
  11.682  \             (? r. (start A,r) : steps A v & rr = True#r))";
  11.683 -br iffI 1;
  11.684 - be True_start_steps_starD 1;
  11.685 +by (rtac iffI 1);
  11.686 + by (etac True_start_steps_starD 1);
  11.687  by (Clarify_tac 1);
  11.688 -by(Asm_simp_tac 1);
  11.689 -by(blast_tac (claset() addIs [True_True_steps_starI,steps_star_cycle]) 1);
  11.690 +by (Asm_simp_tac 1);
  11.691 +by (blast_tac (claset() addIs [True_True_steps_starI,steps_star_cycle]) 1);
  11.692  qed "True_start_steps_star";
  11.693  
  11.694  (** the start state **)
  11.695  
  11.696  Goalw [star_def,step_def]
  11.697    "!A. (start(star A),r) : step (star A) a = (a=None & r = True#start A)";
  11.698 -by(Simp_tac 1);
  11.699 +by (Simp_tac 1);
  11.700  qed_spec_mp "start_step_star";
  11.701  AddIffs [start_step_star];
  11.702  
  11.703 @@ -605,27 +605,27 @@
  11.704  Goal
  11.705   "(start(star A),r) : steps (star A) w = \
  11.706  \ ((w=[] & r= start(star A)) | (True#start A,r) : steps (star A) w)";
  11.707 -br iffI 1;
  11.708 - by(exhaust_tac "w" 1);
  11.709 -  by(asm_full_simp_tac (simpset() addsimps
  11.710 +by (rtac iffI 1);
  11.711 + by (exhaust_tac "w" 1);
  11.712 +  by (asm_full_simp_tac (simpset() addsimps
  11.713      [epsclosure_start_step_star]) 1);
  11.714 - by(Asm_full_simp_tac 1);
  11.715 + by (Asm_full_simp_tac 1);
  11.716   by (Clarify_tac 1);
  11.717 - by(asm_full_simp_tac (simpset() addsimps
  11.718 + by (asm_full_simp_tac (simpset() addsimps
  11.719      [epsclosure_start_step_star]) 1);
  11.720 - by(Blast_tac 1);
  11.721 -be disjE 1;
  11.722 - by(Asm_simp_tac 1);
  11.723 -by(blast_tac (claset() addIs [in_steps_epsclosure,r_into_rtrancl]) 1);
  11.724 + by (Blast_tac 1);
  11.725 +by (etac disjE 1);
  11.726 + by (Asm_simp_tac 1);
  11.727 +by (blast_tac (claset() addIs [in_steps_epsclosure,r_into_rtrancl]) 1);
  11.728  qed "start_steps_star";
  11.729  
  11.730  Goalw [star_def] "!A. fin (star A) (True#p) = fin A p";
  11.731 -by(Simp_tac 1);
  11.732 +by (Simp_tac 1);
  11.733  qed_spec_mp "fin_star_True";
  11.734  AddIffs [fin_star_True];
  11.735  
  11.736  Goalw [star_def] "!A. fin (star A) (start(star A))";
  11.737 -by(Simp_tac 1);
  11.738 +by (Simp_tac 1);
  11.739  qed_spec_mp "fin_star_start";
  11.740  AddIffs [fin_star_start];
  11.741  
  11.742 @@ -633,25 +633,25 @@
  11.743  Goalw [accepts_def]
  11.744   "accepts (star A) w = \
  11.745  \ (? us. (!u : set(us). accepts A u) & (w = concat us) )";
  11.746 -by(simp_tac (simpset() addsimps [start_steps_star,True_start_steps_star]) 1);
  11.747 -br iffI 1;
  11.748 +by (simp_tac (simpset() addsimps [start_steps_star,True_start_steps_star]) 1);
  11.749 +by (rtac iffI 1);
  11.750   by (Clarify_tac 1);
  11.751 - be disjE 1;
  11.752 + by (etac disjE 1);
  11.753    by (Clarify_tac 1);
  11.754 -  by(Simp_tac 1);
  11.755 -  by(res_inst_tac [("x","[]")] exI 1);
  11.756 -  by(Simp_tac 1);
  11.757 +  by (Simp_tac 1);
  11.758 +  by (res_inst_tac [("x","[]")] exI 1);
  11.759 +  by (Simp_tac 1);
  11.760   by (Clarify_tac 1);
  11.761 - by(res_inst_tac [("x","us@[v]")] exI 1);
  11.762 - by(asm_full_simp_tac (simpset() addsimps [accepts_def]) 1);
  11.763 - by(Blast_tac 1);
  11.764 + by (res_inst_tac [("x","us@[v]")] exI 1);
  11.765 + by (asm_full_simp_tac (simpset() addsimps [accepts_def]) 1);
  11.766 + by (Blast_tac 1);
  11.767  by (Clarify_tac 1);
  11.768 -by(res_inst_tac [("xs","us")] rev_exhaust 1);
  11.769 - by(Asm_simp_tac 1);
  11.770 - by(Blast_tac 1);
  11.771 +by (res_inst_tac [("xs","us")] rev_exhaust 1);
  11.772 + by (Asm_simp_tac 1);
  11.773 + by (Blast_tac 1);
  11.774  by (Clarify_tac 1);
  11.775 -by(asm_full_simp_tac (simpset() addsimps [accepts_def]) 1);
  11.776 -by(Blast_tac 1);
  11.777 +by (asm_full_simp_tac (simpset() addsimps [accepts_def]) 1);
  11.778 +by (Blast_tac 1);
  11.779  qed "accepts_star";
  11.780  
  11.781  
  11.782 @@ -659,10 +659,10 @@
  11.783  
  11.784  Goal
  11.785   "!w. accepts (rexp2nae r) w = (w : lang r)";
  11.786 -by(induct_tac "r" 1);
  11.787 -    by(simp_tac (simpset() addsimps [accepts_def]) 1);
  11.788 -   by(simp_tac(simpset() addsimps [accepts_atom]) 1);
  11.789 -  by(asm_simp_tac (simpset() addsimps [accepts_union]) 1);
  11.790 - by(asm_simp_tac (simpset() addsimps [accepts_conc,RegSet.conc_def]) 1);
  11.791 -by(asm_simp_tac (simpset() addsimps [accepts_star,in_star]) 1);
  11.792 +by (induct_tac "r" 1);
  11.793 +    by (simp_tac (simpset() addsimps [accepts_def]) 1);
  11.794 +   by (simp_tac(simpset() addsimps [accepts_atom]) 1);
  11.795 +  by (asm_simp_tac (simpset() addsimps [accepts_union]) 1);
  11.796 + by (asm_simp_tac (simpset() addsimps [accepts_conc,RegSet.conc_def]) 1);
  11.797 +by (asm_simp_tac (simpset() addsimps [accepts_star,in_star]) 1);
  11.798  qed "accepts_rexp2nae";
    12.1 --- a/src/HOL/Lex/RegSet.ML	Fri Jul 10 15:24:22 1998 +0200
    12.2 +++ b/src/HOL/Lex/RegSet.ML	Sun Jul 12 11:49:17 1998 +0200
    12.3 @@ -15,7 +15,7 @@
    12.4  
    12.5  Goal
    12.6   "w : star U = (? us. (!u : set(us). u : U) & (w = concat us))";
    12.7 -br iffI 1;
    12.8 +by (rtac iffI 1);
    12.9   be star.induct 1;
   12.10    by (res_inst_tac [("x","[]")] exI 1);
   12.11    by (Simp_tac 1);
    13.1 --- a/src/HOL/Lex/RegSet_of_nat_DA.ML	Fri Jul 10 15:24:22 1998 +0200
    13.2 +++ b/src/HOL/Lex/RegSet_of_nat_DA.ML	Sun Jul 12 11:49:17 1998 +0200
    13.3 @@ -210,6 +210,6 @@
    13.4  Goalw [regset_of_DA_def]
    13.5   "[| bounded (next A) k; start A < k; j < k |] ==> \
    13.6  \ w : regset_of_DA A k = accepts A w";
    13.7 -by(asm_simp_tac (simpset() addcongs [conj_cong] addsimps
    13.8 +by (asm_simp_tac (simpset() addcongs [conj_cong] addsimps
    13.9   [regset_below,deltas_below,accepts_def,delta_def]) 1);
   13.10  qed "regset_DA_equiv";
    14.1 --- a/src/HOL/Lex/Scanner.ML	Fri Jul 10 15:24:22 1998 +0200
    14.2 +++ b/src/HOL/Lex/Scanner.ML	Sun Jul 12 11:49:17 1998 +0200
    14.3 @@ -6,5 +6,5 @@
    14.4  
    14.5  Goal
    14.6   "DA.accepts (nae2da(rexp2nae r)) w = (w : lang r)";
    14.7 -by(simp_tac (simpset() addsimps [NAe_DA_equiv,accepts_rexp2nae]) 1);
    14.8 +by (simp_tac (simpset() addsimps [NAe_DA_equiv,accepts_rexp2nae]) 1);
    14.9  qed "accepts_nae2da_rexp2nae";
    15.1 --- a/src/HOL/List.ML	Fri Jul 10 15:24:22 1998 +0200
    15.2 +++ b/src/HOL/List.ML	Sun Jul 12 11:49:17 1998 +0200
    15.3 @@ -21,7 +21,7 @@
    15.4  (* Induction over the length of a list: *)
    15.5  val [prem] = Goal
    15.6    "(!!xs. (!ys. length ys < length xs --> P ys) ==> P xs) ==> P(xs)";
    15.7 -by(rtac measure_induct 1 THEN etac prem 1);
    15.8 +by (rtac measure_induct 1 THEN etac prem 1);
    15.9  qed "length_induct";
   15.10  
   15.11  
   15.12 @@ -184,14 +184,14 @@
   15.13   [same_append_eq RS iffD1, append1_eq_conv RS iffD1, append_same_eq RS iffD1];
   15.14  
   15.15  Goal "(xs @ ys = ys) = (xs=[])";
   15.16 -by(cut_inst_tac [("zs","[]")] append_same_eq 1);
   15.17 +by (cut_inst_tac [("zs","[]")] append_same_eq 1);
   15.18  by (Auto_tac);
   15.19  qed "append_self_conv2";
   15.20  
   15.21  Goal "(ys = xs @ ys) = (xs=[])";
   15.22 -by(simp_tac (simpset() addsimps
   15.23 +by (simp_tac (simpset() addsimps
   15.24       [simplify (simpset()) (read_instantiate[("ys","[]")]append_same_eq)]) 1);
   15.25 -by(Blast_tac 1);
   15.26 +by (Blast_tac 1);
   15.27  qed "self_append_conv2";
   15.28  AddIffs [append_self_conv2,self_append_conv2];
   15.29  
   15.30 @@ -309,16 +309,16 @@
   15.31  AddIffs [Nil_is_rev_conv];
   15.32  
   15.33  val prems = Goal "[| P []; !!x xs. P xs ==> P(xs@[x]) |] ==> P xs";
   15.34 -by(stac (rev_rev_ident RS sym) 1);
   15.35 +by (stac (rev_rev_ident RS sym) 1);
   15.36  br(read_instantiate [("P","%xs. ?P(rev xs)")]list.induct)1;
   15.37 -by(ALLGOALS Simp_tac);
   15.38 -brs prems 1;
   15.39 -bes prems 1;
   15.40 +by (ALLGOALS Simp_tac);
   15.41 +by (resolve_tac prems 1);
   15.42 +by (eresolve_tac prems 1);
   15.43  qed "rev_induct";
   15.44  
   15.45  Goal  "(xs = [] --> P) -->  (!ys y. xs = ys@[y] --> P) --> P";
   15.46 -by(res_inst_tac [("xs","xs")] rev_induct 1);
   15.47 -by(Auto_tac);
   15.48 +by (res_inst_tac [("xs","xs")] rev_induct 1);
   15.49 +by (Auto_tac);
   15.50  bind_thm ("rev_exhaust",
   15.51    impI RSN (2,allI RSN (2,allI RSN (2,impI RS (result() RS mp RS mp)))));
   15.52  
    16.1 --- a/src/HOL/NatDef.ML	Fri Jul 10 15:24:22 1998 +0200
    16.2 +++ b/src/HOL/NatDef.ML	Sun Jul 12 11:49:17 1998 +0200
    16.3 @@ -601,7 +601,7 @@
    16.4  Goal "(m::nat) <= n | n <= m";
    16.5  by (simp_tac (simpset() addsimps [le_eq_less_or_eq]) 1);
    16.6  by (cut_facts_tac [less_linear] 1);
    16.7 -by(Blast_tac 1);
    16.8 +by (Blast_tac 1);
    16.9  qed "nat_le_linear";
   16.10  
   16.11  
    17.1 --- a/src/HOL/Ord.ML	Fri Jul 10 15:24:22 1998 +0200
    17.2 +++ b/src/HOL/Ord.ML	Sun Jul 12 11:49:17 1998 +0200
    17.3 @@ -58,31 +58,31 @@
    17.4  
    17.5  Goal "!!x::'a::linorder. x<y | x=y | y<x";
    17.6  by (simp_tac (simpset() addsimps [order_less_le]) 1);
    17.7 -by(cut_facts_tac [linorder_linear] 1);
    17.8 +by (cut_facts_tac [linorder_linear] 1);
    17.9  by (Blast_tac 1);
   17.10  qed "linorder_less_linear";
   17.11  
   17.12  Goalw [max_def] "!!z::'a::linorder. (z <= max x y) = (z <= x | z <= y)";
   17.13  by (Simp_tac 1);
   17.14 -by(cut_facts_tac [linorder_linear] 1);
   17.15 +by (cut_facts_tac [linorder_linear] 1);
   17.16  by (blast_tac (claset() addIs [order_trans]) 1);
   17.17  qed "le_max_iff_disj";
   17.18  
   17.19  Goalw [max_def] "!!z::'a::linorder. (max x y <= z) = (x <= z & y <= z)";
   17.20  by (Simp_tac 1);
   17.21 -by(cut_facts_tac [linorder_linear] 1);
   17.22 +by (cut_facts_tac [linorder_linear] 1);
   17.23  by (blast_tac (claset() addIs [order_trans]) 1);
   17.24  qed "max_le_iff_conj";
   17.25  
   17.26  Goalw [min_def] "!!z::'a::linorder. (z <= min x y) = (z <= x & z <= y)";
   17.27  by (Simp_tac 1);
   17.28 -by(cut_facts_tac [linorder_linear] 1);
   17.29 +by (cut_facts_tac [linorder_linear] 1);
   17.30  by (blast_tac (claset() addIs [order_trans]) 1);
   17.31  qed "le_min_iff_conj";
   17.32  
   17.33  Goalw [min_def] "!!z::'a::linorder. (min x y <= z) = (x <= z | y <= z)";
   17.34  by (Simp_tac 1);
   17.35 -by(cut_facts_tac [linorder_linear] 1);
   17.36 +by (cut_facts_tac [linorder_linear] 1);
   17.37  by (blast_tac (claset() addIs [order_trans]) 1);
   17.38  qed "min_le_iff_disj";
   17.39  
    18.1 --- a/src/HOL/Prod.ML	Fri Jul 10 15:24:22 1998 +0200
    18.2 +++ b/src/HOL/Prod.ML	Sun Jul 12 11:49:17 1998 +0200
    18.3 @@ -156,7 +156,7 @@
    18.4  Addsimps split_etas; (* pragmatic solution *)
    18.5  
    18.6  Goal "(%(x,y,z).f(x,y,z)) = t";
    18.7 -by(simp_tac (simpset() addsimps [cond_split_eta]) 1);
    18.8 +by (simp_tac (simpset() addsimps [cond_split_eta]) 1);
    18.9  
   18.10  qed_goal "split_beta" Prod.thy "(%(x,y). P x y) z = P (fst z) (snd z)"
   18.11  	(K [stac surjective_pairing 1, stac split 1, rtac refl 1]);
    19.1 --- a/src/HOL/Trancl.ML	Fri Jul 10 15:24:22 1998 +0200
    19.2 +++ b/src/HOL/Trancl.ML	Sun Jul 12 11:49:17 1998 +0200
    19.3 @@ -114,9 +114,9 @@
    19.4  Addsimps [rtrancl_idemp];
    19.5  
    19.6  Goal "R^* O R^* = R^*";
    19.7 -br set_ext 1;
    19.8 -by(split_all_tac 1);
    19.9 -by(blast_tac (claset() addIs [rtrancl_trans]) 1);
   19.10 +by (rtac set_ext 1);
   19.11 +by (split_all_tac 1);
   19.12 +by (blast_tac (claset() addIs [rtrancl_trans]) 1);
   19.13  qed "rtrancl_idemp_self_comp";
   19.14  Addsimps [rtrancl_idemp_self_comp];
   19.15  
   19.16 @@ -341,7 +341,7 @@
   19.17  by (etac rtranclE 1);
   19.18  by  (Auto_tac );
   19.19  by (etac rtrancl_into_trancl1 1);
   19.20 -ba 1;
   19.21 +by (assume_tac 1);
   19.22  qed "reflcl_trancl";
   19.23  Addsimps[reflcl_trancl];
   19.24  
    20.1 --- a/src/HOL/UNITY/Traces.ML	Fri Jul 10 15:24:22 1998 +0200
    20.2 +++ b/src/HOL/UNITY/Traces.ML	Sun Jul 12 11:49:17 1998 +0200
    20.3 @@ -53,7 +53,7 @@
    20.4  \        ==> P s' |] \
    20.5  \  ==> P za";
    20.6  by (cut_facts_tac [major] 1);
    20.7 -auto();
    20.8 +by Auto_tac;
    20.9  be traces.induct 1;
   20.10  by (ALLGOALS (blast_tac (claset() addIs prems)));
   20.11  qed "reachable_induct";
    21.1 --- a/src/HOL/WF.ML	Fri Jul 10 15:24:22 1998 +0200
    21.2 +++ b/src/HOL/WF.ML	Sun Jul 12 11:49:17 1998 +0200
    21.3 @@ -232,7 +232,7 @@
    21.4  by (simp_tac (HOL_ss addsimps [cuts_eq]) 1);
    21.5  by (Clarify_tac 1);
    21.6  by (stac cut_apply 1);
    21.7 - by(fast_tac (claset() addDs [transD]) 1);
    21.8 + by (fast_tac (claset() addDs [transD]) 1);
    21.9  by (rtac (refl RSN (2,H_cong)) 1);
   21.10  by (fold_tac [is_recfun_def]);
   21.11  by (asm_simp_tac (wf_super_ss addsimps[is_recfun_cut]) 1);
    22.1 --- a/src/HOL/arith_data.ML	Fri Jul 10 15:24:22 1998 +0200
    22.2 +++ b/src/HOL/arith_data.ML	Sun Jul 12 11:49:17 1998 +0200
    22.3 @@ -226,7 +226,7 @@
    22.4  by (induct_tac "l" 1);
    22.5  by (Simp_tac 1);
    22.6  by (Clarify_tac 1);
    22.7 -be less_SucE 1;
    22.8 +by (etac less_SucE 1);
    22.9  by (asm_simp_tac (simpset() addsimps [diff_Suc_le_Suc_diff RS le_less_trans,
   22.10  				      Suc_diff_n]) 1);
   22.11  by (Clarify_tac 1);
    23.1 --- a/src/HOLCF/IOA/NTP/Multiset.ML	Fri Jul 10 15:24:22 1998 +0200
    23.2 +++ b/src/HOLCF/IOA/NTP/Multiset.ML	Sun Jul 12 11:49:17 1998 +0200
    23.3 @@ -38,7 +38,7 @@
    23.4  by (res_inst_tac [("M","M")] Multiset.induction 1);
    23.5   by (simp_tac (simpset() addsimps [Multiset.countm_empty_def]) 1);
    23.6  by (simp_tac (simpset() addsimps[Multiset.countm_nonempty_def]) 1);
    23.7 -auto();
    23.8 +by Auto_tac;
    23.9  qed "countm_props";
   23.10  
   23.11  Goal "!!P. ~P(obj) ==> countm M P = countm (delm M obj) P";
    24.1 --- a/src/HOLCF/IOA/meta_theory/Abstraction.ML	Fri Jul 10 15:24:22 1998 +0200
    24.2 +++ b/src/HOLCF/IOA/meta_theory/Abstraction.ML	Sun Jul 12 11:49:17 1998 +0200
    24.3 @@ -39,13 +39,13 @@
    24.4  Goal "temp_weakening Q P h = (! ex. (ex |== P) --> (cex_abs h ex |== Q))";
    24.5  by (simp_tac (simpset() addsimps [temp_weakening_def,temp_strengthening_def,
    24.6       NOT_def,temp_sat_def,satisfies_def]) 1);
    24.7 -auto();
    24.8 +by Auto_tac;
    24.9  qed"temp_weakening_def2";
   24.10  
   24.11  Goal "state_weakening Q P h = (! s t a. P (s,a,t) --> Q (h(s),a,h(t)))";
   24.12  by (simp_tac (simpset() addsimps [state_weakening_def,state_strengthening_def,
   24.13       NOT_def]) 1);
   24.14 -auto();
   24.15 +by Auto_tac;
   24.16  qed"state_weakening_def2";
   24.17  
   24.18  
   24.19 @@ -74,7 +74,7 @@
   24.20  
   24.21  Goal "!!A. is_abstraction h C A ==> weakeningIOA A C h";
   24.22  by (asm_full_simp_tac (simpset() addsimps [weakeningIOA_def])1);
   24.23 -auto();
   24.24 +by Auto_tac;
   24.25  by (asm_full_simp_tac (simpset() addsimps [executions_def]) 1);
   24.26  (* start state *) 
   24.27  by (rtac conjI 1);
   24.28 @@ -87,7 +87,7 @@
   24.29  
   24.30  Goal "!!A. [|is_abstraction h C A; validIOA A Q; temp_strengthening Q P h |] \
   24.31  \         ==> validIOA C P";
   24.32 -bd abs_is_weakening 1;
   24.33 +by (dtac abs_is_weakening 1);
   24.34  by (asm_full_simp_tac (simpset() addsimps [weakeningIOA_def, 
   24.35      validIOA_def, temp_strengthening_def])1);
   24.36  by (safe_tac set_cs);
   24.37 @@ -120,8 +120,8 @@
   24.38     "!!A. [|is_live_abstraction h (C,L) (A,M); \
   24.39  \         validLIOA (A,M) Q;  temp_strengthening Q P h |] \
   24.40  \         ==> validLIOA (C,L) P";
   24.41 -auto();
   24.42 -bd abs_is_weakening 1;
   24.43 +by Auto_tac;
   24.44 +by (dtac abs_is_weakening 1);
   24.45  by (asm_full_simp_tac (simpset() addsimps [weakeningIOA_def, temp_weakening_def2,
   24.46      validLIOA_def, validIOA_def, temp_strengthening_def])1);
   24.47  by (safe_tac set_cs);
   24.48 @@ -134,8 +134,8 @@
   24.49  \         validLIOA (A,M) (H1 .--> Q);  temp_strengthening Q P h; \
   24.50  \         temp_weakening H1 H2 h; validLIOA (C,L) H2 |] \
   24.51  \         ==> validLIOA (C,L) P";
   24.52 -auto();
   24.53 -bd abs_is_weakening 1;
   24.54 +by Auto_tac;
   24.55 +by (dtac abs_is_weakening 1);
   24.56  by (asm_full_simp_tac (simpset() addsimps [weakeningIOA_def, temp_weakening_def2,
   24.57      validLIOA_def, validIOA_def, temp_strengthening_def])1);
   24.58  by (safe_tac set_cs);
   24.59 @@ -162,10 +162,10 @@
   24.60  \                  is_abstraction h C A |] \
   24.61  \               ==> C =<| A";
   24.62  by (asm_full_simp_tac (simpset() addsimps [ioa_implements_def]) 1);
   24.63 -br trace_inclusion 1;
   24.64 +by (rtac trace_inclusion 1);
   24.65  by (simp_tac (simpset() addsimps [externals_def])1);
   24.66  by (SELECT_GOAL (auto_tac (claset(),simpset()))1);
   24.67 -be abstraction_is_ref_map 1;
   24.68 +by (etac abstraction_is_ref_map 1);
   24.69  qed"abs_safety";
   24.70  
   24.71  
   24.72 @@ -244,7 +244,7 @@
   24.73  
   24.74  Goalw [ioa_implements_def] 
   24.75  "!! A. [| A =<| B; B =<| C|] ==> A =<| C"; 
   24.76 -auto();
   24.77 +by Auto_tac;
   24.78  qed"implements_trans";
   24.79  
   24.80  
   24.81 @@ -260,13 +260,13 @@
   24.82  \                  A =<| Q ; \
   24.83  \                  is_abstraction h2 Q P |] \
   24.84  \               ==> C =<| P";   
   24.85 -bd abs_safety 1;
   24.86 +by (dtac abs_safety 1);
   24.87  by (REPEAT (atac 1));
   24.88 -bd abs_safety 1;
   24.89 +by (dtac abs_safety 1);
   24.90  by (REPEAT (atac 1));
   24.91 -be implements_trans 1;
   24.92 -be implements_trans 1;
   24.93 -ba 1;
   24.94 +by (etac implements_trans 1);
   24.95 +by (etac implements_trans 1);
   24.96 +by (assume_tac 1);
   24.97  qed"AbsRuleA1";
   24.98  
   24.99  
  24.100 @@ -276,13 +276,13 @@
  24.101  \                  live_implements (A,LA) (Q,LQ) ; \
  24.102  \                  is_live_abstraction h2 (Q,LQ) (P,LP) |] \
  24.103  \               ==> live_implements (C,LC) (P,LP)";   
  24.104 -bd abs_liveness 1;
  24.105 +by (dtac abs_liveness 1);
  24.106  by (REPEAT (atac 1));
  24.107 -bd abs_liveness 1;
  24.108 +by (dtac abs_liveness 1);
  24.109  by (REPEAT (atac 1));
  24.110 -be live_implements_trans 1;
  24.111 -be live_implements_trans 1;
  24.112 -ba 1;
  24.113 +by (etac live_implements_trans 1);
  24.114 +by (etac live_implements_trans 1);
  24.115 +by (assume_tac 1);
  24.116  qed"AbsRuleA2";
  24.117  
  24.118  
  24.119 @@ -299,21 +299,21 @@
  24.120  "!! h. [| temp_strengthening P1 Q1 h; \
  24.121  \         temp_strengthening P2 Q2 h |] \
  24.122  \      ==> temp_strengthening (P1 .& P2) (Q1 .& Q2) h";
  24.123 -auto();
  24.124 +by Auto_tac;
  24.125  qed"strength_AND";
  24.126  
  24.127  Goalw [temp_strengthening_def]
  24.128  "!! h. [| temp_strengthening P1 Q1 h; \
  24.129  \         temp_strengthening P2 Q2 h |] \
  24.130  \      ==> temp_strengthening (P1 .| P2) (Q1 .| Q2) h";
  24.131 -auto();
  24.132 +by Auto_tac;
  24.133  qed"strength_OR";
  24.134  
  24.135  Goalw [temp_strengthening_def]
  24.136  "!! h. [| temp_weakening P Q h |] \
  24.137  \      ==> temp_strengthening (.~ P) (.~ Q) h";
  24.138  by (asm_full_simp_tac (simpset() addsimps [temp_weakening_def2])1);
  24.139 -auto();
  24.140 +by Auto_tac;
  24.141  qed"strength_NOT";
  24.142  
  24.143  Goalw [temp_strengthening_def]
  24.144 @@ -347,7 +347,7 @@
  24.145  "!! h. [| temp_strengthening P Q h |] \
  24.146  \      ==> temp_weakening (.~ P) (.~ Q) h";
  24.147  by (asm_full_simp_tac (simpset() addsimps [temp_weakening_def2])1);
  24.148 -auto();
  24.149 +by Auto_tac;
  24.150  qed"weak_NOT";
  24.151  
  24.152  Goalw [temp_strengthening_def]
  24.153 @@ -387,16 +387,16 @@
  24.154  by (asm_full_simp_tac (simpset() addsimps [nil_is_Conc])1);
  24.155  (* cons case *)
  24.156  by (pair_tac "aa" 1);
  24.157 -auto();
  24.158 +by Auto_tac;
  24.159  qed_spec_mp"ex2seqConc";
  24.160  
  24.161  (* important property of ex2seq: can be shiftet, as defined "pointwise" *)
  24.162  
  24.163  Goalw [tsuffix_def,suffix_def]
  24.164  "!!s. tsuffix s (ex2seq ex) ==> ? ex'. s = (ex2seq ex')";
  24.165 -auto();
  24.166 -bd ex2seqConc 1;
  24.167 -auto();
  24.168 +by Auto_tac;
  24.169 +by (dtac ex2seqConc 1);
  24.170 +by Auto_tac;
  24.171  qed"ex2seq_tsuffix";
  24.172  
  24.173  
  24.174 @@ -414,7 +414,7 @@
  24.175  
  24.176  Goalw [tsuffix_def,suffix_def,cex_absSeq_def]
  24.177  "!! s. tsuffix s t ==> tsuffix (cex_absSeq h s) (cex_absSeq h t)";
  24.178 -auto();
  24.179 +by Auto_tac;
  24.180  by (asm_full_simp_tac (simpset() addsimps [Mapnil])1);
  24.181  by (asm_full_simp_tac (simpset() addsimps [MapUU])1);
  24.182  by (res_inst_tac [("x","Map (%(s,a,t). (h s,a, h t))`s1")] exI 1);
  24.183 @@ -486,7 +486,7 @@
  24.184  by (pair_tac "ex" 1);
  24.185  by (Seq_case_simp_tac "y" 1);
  24.186  by (pair_tac "a" 1);
  24.187 -auto();
  24.188 +by Auto_tac;
  24.189  qed"TLex2seq";
  24.190  
  24.191  
  24.192 @@ -520,9 +520,9 @@
  24.193  (* cons case *)
  24.194  by (asm_full_simp_tac (simpset() addsimps [TL_ex2seq_nil,TL_ex2seq_UU,
  24.195          ex2seq_abs_cex,cex_absSeq_TL RS sym, ex2seqUUTL,ex2seqnilTL])1);
  24.196 -bd TLex2seq 1;
  24.197 -ba 1;
  24.198 -auto();
  24.199 +by (dtac TLex2seq 1);
  24.200 +by (assume_tac 1);
  24.201 +by Auto_tac;
  24.202  qed"strength_Next";
  24.203  
  24.204  
  24.205 @@ -572,18 +572,18 @@
  24.206  Goalw [Diamond_def]
  24.207  "!! h. [| temp_strengthening P Q h |]\
  24.208  \      ==> temp_strengthening (<> P) (<> Q) h";
  24.209 -br strength_NOT 1;
  24.210 -br weak_Box 1;
  24.211 -be weak_NOT 1;
  24.212 +by (rtac strength_NOT 1);
  24.213 +by (rtac weak_Box 1);
  24.214 +by (etac weak_NOT 1);
  24.215  qed"strength_Diamond";
  24.216  
  24.217  Goalw [Leadsto_def]
  24.218  "!! h. [| temp_weakening P1 P2 h;\
  24.219  \         temp_strengthening Q1 Q2 h |]\
  24.220  \      ==> temp_strengthening (P1 ~> Q1) (P2 ~> Q2) h";
  24.221 -br strength_Box 1;
  24.222 -be strength_IMPLIES 1;
  24.223 -be strength_Diamond 1;
  24.224 +by (rtac strength_Box 1);
  24.225 +by (etac strength_IMPLIES 1);
  24.226 +by (etac strength_Diamond 1);
  24.227  qed"strength_Leadsto";
  24.228  
  24.229  
  24.230 @@ -595,30 +595,30 @@
  24.231  Goalw [Diamond_def]
  24.232  "!! h. [| temp_weakening P Q h |]\
  24.233  \      ==> temp_weakening (<> P) (<> Q) h";
  24.234 -br weak_NOT 1;
  24.235 -br strength_Box 1;
  24.236 -be strength_NOT 1;
  24.237 +by (rtac weak_NOT 1);
  24.238 +by (rtac strength_Box 1);
  24.239 +by (etac strength_NOT 1);
  24.240  qed"weak_Diamond";
  24.241  
  24.242  Goalw [Leadsto_def]
  24.243  "!! h. [| temp_strengthening P1 P2 h;\
  24.244  \         temp_weakening Q1 Q2 h |]\
  24.245  \      ==> temp_weakening (P1 ~> Q1) (P2 ~> Q2) h";
  24.246 -br weak_Box 1;
  24.247 -be weak_IMPLIES 1;
  24.248 -be weak_Diamond 1;
  24.249 +by (rtac weak_Box 1);
  24.250 +by (etac weak_IMPLIES 1);
  24.251 +by (etac weak_Diamond 1);
  24.252  qed"weak_Leadsto";
  24.253  
  24.254  Goalw [WF_def]
  24.255    " !!A. [| !! s. Enabled A acts (h s) ==> Enabled C acts s|] \ 
  24.256  \   ==> temp_weakening (WF A acts) (WF C acts) h";
  24.257 -br weak_IMPLIES 1;
  24.258 -br strength_Diamond 1;
  24.259 -br strength_Box 1;
  24.260 -br strength_Init 1;
  24.261 -br weak_Box 2;
  24.262 -br weak_Diamond 2;
  24.263 -br weak_Init 2;
  24.264 +by (rtac weak_IMPLIES 1);
  24.265 +by (rtac strength_Diamond 1);
  24.266 +by (rtac strength_Box 1);
  24.267 +by (rtac strength_Init 1);
  24.268 +by (rtac weak_Box 2);
  24.269 +by (rtac weak_Diamond 2);
  24.270 +by (rtac weak_Init 2);
  24.271  by (auto_tac (claset(),
  24.272                simpset() addsimps [state_weakening_def,state_strengthening_def,
  24.273                               xt2_def,plift_def,option_lift_def,NOT_def]));
  24.274 @@ -627,13 +627,13 @@
  24.275  Goalw [SF_def]
  24.276    " !!A. [| !! s. Enabled A acts (h s) ==> Enabled C acts s|] \ 
  24.277  \   ==> temp_weakening (SF A acts) (SF C acts) h";
  24.278 -br weak_IMPLIES 1;
  24.279 -br strength_Box 1;
  24.280 -br strength_Diamond 1;
  24.281 -br strength_Init 1;
  24.282 -br weak_Box 2;
  24.283 -br weak_Diamond 2;
  24.284 -br weak_Init 2;
  24.285 +by (rtac weak_IMPLIES 1);
  24.286 +by (rtac strength_Box 1);
  24.287 +by (rtac strength_Diamond 1);
  24.288 +by (rtac strength_Init 1);
  24.289 +by (rtac weak_Box 2);
  24.290 +by (rtac weak_Diamond 2);
  24.291 +by (rtac weak_Init 2);
  24.292  by (auto_tac (claset(),
  24.293                simpset() addsimps [state_weakening_def,state_strengthening_def,
  24.294                               xt2_def,plift_def,option_lift_def,NOT_def]));
    25.1 --- a/src/HOLCF/IOA/meta_theory/Deadlock.ML	Fri Jul 10 15:24:22 1998 +0200
    25.2 +++ b/src/HOLCF/IOA/meta_theory/Deadlock.ML	Sun Jul 12 11:49:17 1998 +0200
    25.3 @@ -59,7 +59,7 @@
    25.4  by (rtac conjI 1);
    25.5  (* a : act (A||B) *)
    25.6  by (asm_full_simp_tac (simpset() addsimps [actions_of_par]) 2);
    25.7 -by(blast_tac (claset() addDs [int_is_act,out_is_act]) 2);
    25.8 +by (blast_tac (claset() addDs [int_is_act,out_is_act]) 2);
    25.9  
   25.10  (* Filter B (sch@@[a]) : schedules B *)
   25.11  
    26.1 --- a/src/HOLCF/IOA/meta_theory/LiveIOA.ML	Fri Jul 10 15:24:22 1998 +0200
    26.2 +++ b/src/HOLCF/IOA/meta_theory/LiveIOA.ML	Sun Jul 12 11:49:17 1998 +0200
    26.3 @@ -12,7 +12,7 @@
    26.4  Goalw [live_implements_def] 
    26.5  "!! A. [| live_implements (A,LA) (B,LB); live_implements (B,LB) (C,LC) |] \
    26.6  \     ==> live_implements (A,LA) (C,LC)"; 
    26.7 -auto();
    26.8 +by Auto_tac;
    26.9  qed"live_implements_trans";
   26.10  
   26.11  
   26.12 @@ -51,7 +51,7 @@
   26.13    by (asm_full_simp_tac (simpset() addsimps [reachable.reachable_0]) 1);
   26.14  
   26.15   (* Liveness *)
   26.16 -auto();
   26.17 +by Auto_tac;
   26.18  qed"live_implements";
   26.19  
   26.20  
    27.1 --- a/src/HOLCF/IOA/meta_theory/RefCorrectness.ML	Fri Jul 10 15:24:22 1998 +0200
    27.2 +++ b/src/HOLCF/IOA/meta_theory/RefCorrectness.ML	Sun Jul 12 11:49:17 1998 +0200
    27.3 @@ -256,7 +256,7 @@
    27.4  
    27.5  
    27.6  Goalw [fin_often_def] "(~inf_often P s) = fin_often P s";
    27.7 -auto();
    27.8 +by Auto_tac;
    27.9  qed"fininf";
   27.10  
   27.11  
   27.12 @@ -264,17 +264,17 @@
   27.13  "is_wfair A W (s,ex) = \
   27.14  \ (fin_often (%x. ~Enabled A W (snd x)) ex --> inf_often (%x. fst x :W) ex)";
   27.15  by (asm_full_simp_tac (simpset() addsimps [is_wfair_def,fin_often_def])1);
   27.16 -auto();
   27.17 +by Auto_tac;
   27.18  qed"WF_alt";
   27.19  
   27.20  Goal  
   27.21  "!! ex. [|is_wfair A W (s,ex); inf_often (%x. Enabled A W (snd x)) ex; \
   27.22  \         en_persistent A W|] \
   27.23  \   ==> inf_often (%x. fst x :W) ex";
   27.24 -bd persistent 1;
   27.25 -ba 1;
   27.26 +by (dtac persistent 1);
   27.27 +by (assume_tac 1);
   27.28  by (asm_full_simp_tac (simpset() addsimps [WF_alt])1);
   27.29 -auto();
   27.30 +by Auto_tac;
   27.31  qed"WF_persistent";
   27.32  
   27.33  
   27.34 @@ -305,7 +305,7 @@
   27.35    by (asm_full_simp_tac (simpset() addsimps [reachable.reachable_0]) 1);
   27.36  
   27.37   (* Fairness *)
   27.38 -auto();
   27.39 +by Auto_tac;
   27.40  qed"fair_trace_inclusion";
   27.41  
   27.42  Goal "!! C A. \
   27.43 @@ -335,7 +335,7 @@
   27.44    by (asm_full_simp_tac (simpset() addsimps [reachable.reachable_0]) 1);
   27.45  
   27.46   (* Fairness *)
   27.47 -auto();
   27.48 +by Auto_tac;
   27.49  qed"fair_trace_inclusion2";
   27.50  
   27.51  
    28.1 --- a/src/HOLCF/IOA/meta_theory/SimCorrectness.ML	Fri Jul 10 15:24:22 1998 +0200
    28.2 +++ b/src/HOLCF/IOA/meta_theory/SimCorrectness.ML	Sun Jul 12 11:49:17 1998 +0200
    28.3 @@ -27,9 +27,9 @@
    28.4  \                              @@ ((corresp_ex_simC A R `xs) T'))   \
    28.5  \                        `x) ))";
    28.6  by (rtac trans 1);
    28.7 -br fix_eq2 1;
    28.8 -br corresp_ex_simC_def 1;
    28.9 -br beta_cfun 1;
   28.10 +by (rtac fix_eq2 1);
   28.11 +by (rtac corresp_ex_simC_def 1);
   28.12 +by (rtac beta_cfun 1);
   28.13  by (simp_tac (simpset() addsimps [flift1_def]) 1);
   28.14  qed"corresp_ex_simC_unfold";
   28.15  
   28.16 @@ -48,7 +48,7 @@
   28.17  \           in  \
   28.18  \            (@cex. move A cex s a T')  \ 
   28.19  \             @@ ((corresp_ex_simC A R`xs) T'))";
   28.20 -br trans 1;
   28.21 +by (rtac trans 1);
   28.22  by (stac corresp_ex_simC_unfold 1);
   28.23  by (asm_full_simp_tac (simpset() addsimps [Cons_def,flift1_def]) 1);
   28.24  by (Simp_tac 1);
   28.25 @@ -84,15 +84,15 @@
   28.26  by (eres_inst_tac [("x","a")] allE 2);
   28.27  by (Asm_full_simp_tac 2); 
   28.28  (* Go on as usual *)
   28.29 -be exE 1;
   28.30 +by (etac exE 1);
   28.31  by (dres_inst_tac [("x","t'"),
   28.32           ("P","%t'. ? ex.(t,t'):R & move A ex s' a t'")] selectI 1);
   28.33 -be exE 1;
   28.34 -be conjE 1;
   28.35 +by (etac exE 1);
   28.36 +by (etac conjE 1);
   28.37  by (asm_full_simp_tac (simpset() addsimps [Let_def]) 1);
   28.38  by (res_inst_tac [("x","ex")] selectI 1);
   28.39 -be conjE 1;
   28.40 -ba 1;
   28.41 +by (etac conjE 1);
   28.42 +by (assume_tac 1);
   28.43  qed"move_is_move_sim";
   28.44  
   28.45  
   28.46 @@ -168,7 +168,7 @@
   28.47  ren "ex a t s s'" 1;
   28.48  by (asm_full_simp_tac (simpset() addsimps [mk_traceConc]) 1);
   28.49  by (forward_tac [reachable.reachable_n] 1);
   28.50 -ba 1;
   28.51 +by (assume_tac 1);
   28.52  by (eres_inst_tac [("x","t")] allE 1);
   28.53  by (eres_inst_tac [("x",
   28.54                      "@t'. ? ex1. (t,t'):R & move A ex1 s' a t'")] 
   28.55 @@ -202,12 +202,12 @@
   28.56      lemma_2_1 1);
   28.57  
   28.58  (* Finite *)
   28.59 -be (rewrite_rule [Let_def] move_subprop2_sim) 1;
   28.60 +by (etac (rewrite_rule [Let_def] move_subprop2_sim) 1);
   28.61  by (REPEAT (atac 1));
   28.62  by (rtac conjI 1);
   28.63  
   28.64  (* is_exec_frag *)
   28.65 -be  (rewrite_rule [Let_def] move_subprop1_sim) 1;
   28.66 +by (etac (rewrite_rule [Let_def] move_subprop1_sim) 1);
   28.67  by (REPEAT (atac 1));
   28.68  by (rtac conjI 1);
   28.69  
   28.70 @@ -219,11 +219,11 @@
   28.71       allE 1);
   28.72  by (Asm_full_simp_tac 1);
   28.73  by (forward_tac [reachable.reachable_n] 1);
   28.74 -ba 1;
   28.75 +by (assume_tac 1);
   28.76  by (asm_full_simp_tac (simpset() addsimps 
   28.77              [rewrite_rule [Let_def] move_subprop5_sim]) 1);
   28.78  (* laststate *)
   28.79 -be ((rewrite_rule [Let_def] move_subprop3_sim) RS sym) 1;
   28.80 +by (etac ((rewrite_rule [Let_def] move_subprop3_sim) RS sym) 1);
   28.81  by (REPEAT (atac 1));
   28.82  qed_spec_mp"correspsim_is_execution";
   28.83  
   28.84 @@ -246,11 +246,11 @@
   28.85    by (asm_full_simp_tac (simpset() addsimps [is_simulation_def,
   28.86           corresp_ex_sim_def, Int_non_empty,Image_def]) 1);
   28.87    by (REPEAT (etac conjE 1));
   28.88 -  be ballE 1;
   28.89 +  by (etac ballE 1);
   28.90    by (Blast_tac 2);
   28.91 -  be exE 1;
   28.92 -  br selectI2 1;
   28.93 -  ba 1;
   28.94 +  by (etac exE 1);
   28.95 +  by (rtac selectI2 1);
   28.96 +  by (assume_tac 1);
   28.97    by (Blast_tac 1);
   28.98  qed"simulation_starts";
   28.99  
  28.100 @@ -290,7 +290,7 @@
  28.101    (* is-execution-fragment *)
  28.102    by (asm_full_simp_tac (simpset() addsimps [corresp_ex_sim_def]) 1);
  28.103    by (res_inst_tac [("s","s")] correspsim_is_execution 1);
  28.104 -  ba 1;
  28.105 +  by (assume_tac 1);
  28.106    by (asm_full_simp_tac (simpset() addsimps [reachable.reachable_0,sim_starts1]) 1);
  28.107  qed"trace_inclusion_for_simulations"; 
  28.108  
    29.1 --- a/src/HOLCF/IOA/meta_theory/Simulations.ML	Fri Jul 10 15:24:22 1998 +0200
    29.2 +++ b/src/HOLCF/IOA/meta_theory/Simulations.ML	Sun Jul 12 11:49:17 1998 +0200
    29.3 @@ -10,7 +10,7 @@
    29.4  
    29.5  Goal "(A~={}) = (? x. x:A)";
    29.6  by (safe_tac set_cs);
    29.7 -auto();
    29.8 +by Auto_tac;
    29.9  qed"set_non_empty";
   29.10  
   29.11  Goal "(A Int B ~= {}) = (? x. x: A & x:B)";
    30.1 --- a/src/HOLCF/IOA/meta_theory/TL.ML	Fri Jul 10 15:24:22 1998 +0200
    30.2 +++ b/src/HOLCF/IOA/meta_theory/TL.ML	Sun Jul 12 11:49:17 1998 +0200
    30.3 @@ -8,9 +8,9 @@
    30.4  
    30.5  
    30.6  Goal "[] <> (.~ P) = (.~ <> [] P)";
    30.7 -br ext 1;
    30.8 +by (rtac ext 1);
    30.9  by (simp_tac (simpset() addsimps [Diamond_def,NOT_def,Box_def])1);
   30.10 -auto();
   30.11 +by Auto_tac;
   30.12  qed"simple_try";
   30.13  
   30.14  Goal "nil |= [] P";
   30.15 @@ -39,7 +39,7 @@
   30.16  Goal "suffix s s";
   30.17  by (simp_tac (simpset() addsimps [suffix_def])1);
   30.18  by (res_inst_tac [("x","nil")] exI 1);
   30.19 -auto();
   30.20 +by Auto_tac;
   30.21  qed"suffix_refl";
   30.22  
   30.23  Goal "s~=UU & s~=nil --> (s |= [] F .--> F)";
   30.24 @@ -52,19 +52,19 @@
   30.25  
   30.26  Goal "!!x. [| suffix y x ; suffix z y |]  ==> suffix z x";
   30.27  by (asm_full_simp_tac (simpset() addsimps [suffix_def])1);
   30.28 -auto();
   30.29 +by Auto_tac;
   30.30  by (res_inst_tac [("x","s1 @@ s1a")] exI 1);
   30.31 -auto();
   30.32 +by Auto_tac;
   30.33  by (simp_tac (simpset() addsimps [Conc_assoc]) 1); 
   30.34  qed"suffix_trans";
   30.35  
   30.36  Goal "s |= [] F .--> [] [] F";
   30.37  by (simp_tac (simpset() addsimps [satisfies_def,IMPLIES_def,Box_def,tsuffix_def])1);
   30.38 -auto();
   30.39 -bd suffix_trans 1;
   30.40 -ba 1;
   30.41 +by Auto_tac;
   30.42 +by (dtac suffix_trans 1);
   30.43 +by (assume_tac 1);
   30.44  by (eres_inst_tac [("x","s2a")] allE 1);
   30.45 -auto();
   30.46 +by Auto_tac;
   30.47  qed"transT";
   30.48  
   30.49  
   30.50 @@ -76,13 +76,13 @@
   30.51  (*
   30.52  Goal "s |= <> F .& <> G .--> (<> (F .& <> G) .| <> (G .& <> F))";
   30.53  by (simp_tac (simpset() addsimps [satisfies_def,IMPLIES_def,AND_def,OR_def,Diamond_def2])1);
   30.54 -br impI 1;
   30.55 -be conjE 1;
   30.56 -be exE 1;
   30.57 -be exE 1;
   30.58 +by (rtac impI 1);
   30.59 +by (etac conjE 1);
   30.60 +by (etac exE 1);
   30.61 +by (etac exE 1);
   30.62  
   30.63  
   30.64 -br disjI1 1;
   30.65 +by (rtac disjI1 1);
   30.66  
   30.67  Goal "!!s. [| tsuffix s1 s ; tsuffix s2 s|] ==> tsuffix s2 s1 | tsuffix s1 s2";
   30.68  by (asm_full_simp_tac (simpset() addsimps [tsuffix_def,suffix_def])1);
   30.69 @@ -109,8 +109,8 @@
   30.70  qed"STL1b";
   30.71  
   30.72  Goal "!! P. valid P ==> validT ([] (Init P))";
   30.73 -br STL1a 1;
   30.74 -be STL1b 1;
   30.75 +by (rtac STL1a 1);
   30.76 +by (etac STL1b 1);
   30.77  qed"STL1";
   30.78  
   30.79  
   30.80 @@ -130,10 +130,10 @@
   30.81  
   30.82  Goalw [tsuffix_def,suffix_def]
   30.83  "s~=UU & s~=nil --> tsuffix s2 (TL`s) --> tsuffix s2 s";
   30.84 -auto();
   30.85 +by Auto_tac;
   30.86  by (Seq_case_simp_tac "s" 1);
   30.87  by (res_inst_tac [("x","a>>s1")] exI 1);
   30.88 -auto();
   30.89 +by Auto_tac;
   30.90  qed_spec_mp"tsuffix_TL";
   30.91  
   30.92  val tsuffix_TL2 = conjI RS tsuffix_TL;
   30.93 @@ -141,16 +141,16 @@
   30.94  Delsplits[split_if];
   30.95  Goalw [Next_def,satisfies_def,NOT_def,IMPLIES_def,AND_def,Box_def] 
   30.96     "s~=UU & s~=nil --> (s |= [] F .--> (F .& (Next ([] F))))";
   30.97 -auto();
   30.98 +by Auto_tac;
   30.99  (* []F .--> F *)
  30.100  by (eres_inst_tac [("x","s")] allE 1);
  30.101  by (asm_full_simp_tac (simpset() addsimps [tsuffix_def,suffix_refl])1);
  30.102  (* []F .--> Next [] F *)
  30.103  by (asm_full_simp_tac (simpset() addsplits [split_if]) 1);
  30.104 -auto();
  30.105 -bd tsuffix_TL2 1;
  30.106 +by Auto_tac;
  30.107 +by (dtac tsuffix_TL2 1);
  30.108  by (REPEAT (atac 1));
  30.109 -auto();
  30.110 +by Auto_tac;
  30.111  qed"LTL1";
  30.112  Addsplits[split_if];
  30.113  
  30.114 @@ -173,11 +173,11 @@
  30.115  Goalw [Next_def,satisfies_def,Box_def,NOT_def,IMPLIES_def] 
  30.116   "s |= [] (F .--> Next F) .--> F .--> []F";
  30.117  by (Asm_full_simp_tac 1);
  30.118 -auto();
  30.119 +by Auto_tac;
  30.120  
  30.121  
  30.122  by (asm_full_simp_tac (simpset() addsimps [tsuffix_def,suffix_def])1);
  30.123 -auto();
  30.124 +by Auto_tac;
  30.125  
  30.126  
  30.127  
    31.1 --- a/src/HOLCF/IOA/meta_theory/TrivEx.ML	Fri Jul 10 15:24:22 1998 +0200
    31.2 +++ b/src/HOLCF/IOA/meta_theory/TrivEx.ML	Sun Jul 12 11:49:17 1998 +0200
    31.3 @@ -7,7 +7,7 @@
    31.4  *)
    31.5  
    31.6  val prems = goal HOL.thy "(P ==> Q-->R) ==> P&Q --> R";
    31.7 -  by(fast_tac (claset() addDs prems) 1);
    31.8 +  by (fast_tac (claset() addDs prems) 1);
    31.9  qed "imp_conj_lemma";
   31.10  
   31.11  
   31.12 @@ -24,14 +24,14 @@
   31.13          C_ioa_def,A_ioa_def,C_trans_def,A_trans_def])1);
   31.14  by (simp_tac (simpset() addsimps [h_abs_def]) 1);
   31.15  by (action.induct_tac "a" 1);
   31.16 -auto();
   31.17 +by Auto_tac;
   31.18  qed"h_abs_is_abstraction";
   31.19  
   31.20  
   31.21  Goal "validIOA C_ioa (<>[] <%(n,a,m). n~=0>)";
   31.22 -br AbsRuleT1 1;
   31.23 -br h_abs_is_abstraction 1;
   31.24 -br MC_result 1;
   31.25 +by (rtac AbsRuleT1 1);
   31.26 +by (rtac h_abs_is_abstraction 1);
   31.27 +by (rtac MC_result 1);
   31.28  by (abstraction_tac 1);
   31.29  by (asm_full_simp_tac (simpset() addsimps [h_abs_def]) 1);
   31.30  qed"TrivEx_abstraction";
    32.1 --- a/src/HOLCF/IOA/meta_theory/TrivEx2.ML	Fri Jul 10 15:24:22 1998 +0200
    32.2 +++ b/src/HOLCF/IOA/meta_theory/TrivEx2.ML	Sun Jul 12 11:49:17 1998 +0200
    32.3 @@ -7,7 +7,7 @@
    32.4  *)
    32.5  
    32.6  val prems = goal HOL.thy "(P ==> Q-->R) ==> P&Q --> R";
    32.7 -  by(fast_tac (claset() addDs prems) 1);
    32.8 +  by (fast_tac (claset() addDs prems) 1);
    32.9  qed "imp_conj_lemma";
   32.10  
   32.11  
   32.12 @@ -24,7 +24,7 @@
   32.13          C_ioa_def,A_ioa_def,C_trans_def,A_trans_def])1);
   32.14  by (simp_tac (simpset() addsimps [h_abs_def]) 1);
   32.15  by (action.induct_tac "a" 1);
   32.16 -auto();
   32.17 +by Auto_tac;
   32.18  qed"h_abs_is_abstraction";
   32.19  
   32.20  
   32.21 @@ -39,26 +39,26 @@
   32.22  Goalw [Enabled_def, enabled_def, h_abs_def,A_ioa_def,C_ioa_def,A_trans_def,
   32.23             C_trans_def,trans_of_def] 
   32.24  "!!s. Enabled A_ioa {INC} (h_abs s) ==> Enabled C_ioa {INC} s";
   32.25 -auto();
   32.26 +by Auto_tac;
   32.27  qed"Enabled_implication";
   32.28  
   32.29  
   32.30  Goalw [is_live_abstraction_def]
   32.31  "is_live_abstraction h_abs (C_ioa, WF C_ioa {INC}) (A_ioa, WF A_ioa {INC})";
   32.32 -auto();
   32.33 +by Auto_tac;
   32.34  (* is_abstraction *)
   32.35 -br h_abs_is_abstraction 1;
   32.36 +by (rtac h_abs_is_abstraction 1);
   32.37  (* temp_weakening *)
   32.38  by (abstraction_tac 1);
   32.39 -be Enabled_implication 1;
   32.40 +by (etac Enabled_implication 1);
   32.41  qed"h_abs_is_liveabstraction";
   32.42  
   32.43  
   32.44  Goalw [C_live_ioa_def]
   32.45  "validLIOA C_live_ioa (<>[] <%(n,a,m). n~=0>)";
   32.46 -br AbsRuleT2 1;
   32.47 -br h_abs_is_liveabstraction 1;
   32.48 -br MC_result 1;
   32.49 +by (rtac AbsRuleT2 1);
   32.50 +by (rtac h_abs_is_liveabstraction 1);
   32.51 +by (rtac MC_result 1);
   32.52  by (abstraction_tac 1);
   32.53  by (asm_full_simp_tac (simpset() addsimps [h_abs_def]) 1);
   32.54  qed"TrivEx2_abstraction";