New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
authorpaulson
Wed Dec 24 10:02:30 1997 +0100 (1997-12-24 ago)
changeset 4477b3e5857d8d99
parent 4476 fbdc87f8ac7e
child 4478 9c5a0eef74ff
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
src/FOL/simpdata.ML
src/HOL/Auth/Event.ML
src/HOL/Auth/Message.ML
src/HOL/Auth/NS_Public.ML
src/HOL/Auth/NS_Public_Bad.ML
src/HOL/Auth/NS_Shared.ML
src/HOL/Auth/OtwayRees.ML
src/HOL/Auth/OtwayRees_AN.ML
src/HOL/Auth/OtwayRees_Bad.ML
src/HOL/Auth/Public.ML
src/HOL/Auth/Recur.ML
src/HOL/Auth/Shared.ML
src/HOL/Auth/TLS.ML
src/HOL/Auth/WooLam.ML
src/HOL/Auth/Yahalom.ML
src/HOL/Auth/Yahalom2.ML
src/HOL/Divides.ML
src/HOL/Finite.ML
src/HOL/IMP/Denotation.ML
src/HOL/IMP/Transition.ML
src/HOL/IOA/Solve.ML
src/HOL/Induct/Exp.ML
src/HOL/Induct/LFilter.ML
src/HOL/Induct/LList.ML
src/HOL/Induct/Mutil.ML
src/HOL/Integ/Integ.ML
src/HOL/Option.ML
src/HOL/Quot/HQUOT.ML
src/HOL/Quot/NPAIR.ML
src/HOL/Set.ML
src/HOL/Subst/Subst.ML
src/HOL/Sum.ML
src/HOL/TLA/Action.ML
src/HOL/TLA/Buffer/DBuffer.ML
src/HOL/TLA/Inc/Inc.ML
src/HOL/TLA/Memory/MIlive.ML
src/HOL/TLA/Memory/MemoryImplementation.ML
src/HOL/TLA/ROOT.ML
src/HOL/TLA/TLA.ML
src/HOL/equalities.ML
src/HOL/ex/Recdef.ML
src/HOL/simpdata.ML
src/HOLCF/Fix.ML
src/HOLCF/IOA/ABP/Correctness.ML
src/HOLCF/IOA/meta_theory/Automata.ML
src/HOLCF/IOA/meta_theory/CompoScheds.ML
src/HOLCF/IOA/meta_theory/CompoTraces.ML
src/HOLCF/IOA/meta_theory/Compositionality.ML
src/HOLCF/IOA/meta_theory/RefMappings.ML
src/HOLCF/IOA/meta_theory/Seq.ML
src/HOLCF/IOA/meta_theory/Sequence.ML
src/HOLCF/IOA/meta_theory/ShortExecutions.ML
src/HOLCF/IOA/meta_theory/Traces.ML
src/HOLCF/Lift.ML
src/HOLCF/Lift3.ML
src/HOLCF/Tr.ML
src/ZF/CardinalArith.ML
src/ZF/Coind/MT.ML
src/ZF/Perm.ML
src/ZF/QPair.ML
src/ZF/Sum.ML
src/ZF/ex/Limit.ML
src/ZF/ex/misc.ML
src/ZF/pair.ML
     1.1 --- a/src/FOL/simpdata.ML	Tue Dec 23 11:56:09 1997 +0100
     1.2 +++ b/src/FOL/simpdata.ML	Wed Dec 24 10:02:30 1997 +0100
     1.3 @@ -362,14 +362,25 @@
     1.4  fun op addcongs2 arg = pair_upd2 (op addcongs) arg;
     1.5  fun op delcongs2 arg = pair_upd2 (op delcongs) arg;
     1.6  
     1.7 -fun auto_tac (cs,ss) = 
     1.8 +
     1.9 +fun mk_auto_tac (cs, ss) m n =
    1.10      let val cs' = cs addss ss 
    1.11 -    in  EVERY [TRY (safe_tac cs'),
    1.12 -	       REPEAT (FIRSTGOAL (fast_tac cs')),
    1.13 +	val bdt = Blast.depth_tac cs m;
    1.14 +	fun blast_depth_tac i thm = bdt i thm handle Blast.TRANS s => 
    1.15 +		(warning ("Blast_tac: " ^ s); Seq.empty);
    1.16 +        val maintac = 
    1.17 +          blast_depth_tac	   (*fast but can't use addss*)
    1.18 +          ORELSE'
    1.19 +          depth_tac cs' n;         (*slower but general*)
    1.20 +    in  EVERY [ALLGOALS (asm_full_simp_tac ss),
    1.21 +	       TRY (safe_tac cs'),
    1.22 +	       REPEAT (FIRSTGOAL maintac),
    1.23                 TRY (safe_tac (cs addSss ss)),
    1.24  	       prune_params_tac] 
    1.25      end;
    1.26  
    1.27 -fun Auto_tac () = auto_tac (claset(), simpset());
    1.28 +fun auto_tac (cs,ss) = mk_auto_tac (cs,ss) 4 2;
    1.29  
    1.30 -fun auto () = by (Auto_tac ());
    1.31 +fun Auto_tac st = auto_tac (claset(), simpset()) st;
    1.32 +
    1.33 +fun auto () = by Auto_tac;
     2.1 --- a/src/HOL/Auth/Event.ML	Tue Dec 23 11:56:09 1997 +0100
     2.2 +++ b/src/HOL/Auth/Event.ML	Wed Dec 24 10:02:30 1997 +0100
     2.3 @@ -27,7 +27,7 @@
     2.4  \      ((ALL A B X. ev = Says A B X --> P(sf A B X)) & \
     2.5  \       (ALL A X. ev = Notes A X --> P(nf A X)))";
     2.6  by (induct_tac "ev" 1);
     2.7 -by (Auto_tac());
     2.8 +by Auto_tac;
     2.9  qed "expand_event_case";
    2.10  
    2.11  goal thy "spies (Says A B X # evs) = insert X (spies evs)";
     3.1 --- a/src/HOL/Auth/Message.ML	Tue Dec 23 11:56:09 1997 +0100
     3.2 +++ b/src/HOL/Auth/Message.ML	Wed Dec 24 10:02:30 1997 +0100
     3.3 @@ -20,15 +20,15 @@
     3.4  
     3.5  (*Equations hold because constructors are injective; cannot prove for all f*)
     3.6  goal thy "(Friend x : Friend``A) = (x:A)";
     3.7 -by (Auto_tac());
     3.8 +by Auto_tac;
     3.9  qed "Friend_image_eq";
    3.10  
    3.11  goal thy "(Key x : Key``A) = (x:A)";
    3.12 -by (Auto_tac());
    3.13 +by Auto_tac;
    3.14  qed "Key_image_eq";
    3.15  
    3.16  goal thy "(Nonce x ~: Key``A)";
    3.17 -by (Auto_tac());
    3.18 +by Auto_tac;
    3.19  qed "Nonce_Key_image_eq";
    3.20  Addsimps [Friend_image_eq, Key_image_eq, Nonce_Key_image_eq];
    3.21  
    3.22 @@ -90,7 +90,7 @@
    3.23  
    3.24  goalw thy [keysFor_def]
    3.25      "keysFor (insert (Crypt K X) H) = insert (invKey K) (keysFor H)";
    3.26 -by (Auto_tac());
    3.27 +by Auto_tac;
    3.28  qed "keysFor_insert_Crypt";
    3.29  
    3.30  Addsimps [keysFor_empty, keysFor_Un, keysFor_UN, 
    3.31 @@ -101,7 +101,7 @@
    3.32  	keysFor_UN RS equalityD1 RS subsetD RS UN_E];
    3.33  
    3.34  goalw thy [keysFor_def] "keysFor (Key``E) = {}";
    3.35 -by (Auto_tac ());
    3.36 +by Auto_tac;
    3.37  qed "keysFor_image_Key";
    3.38  Addsimps [keysFor_image_Key];
    3.39  
    3.40 @@ -235,7 +235,7 @@
    3.41  goal thy "!!H. [| Y: parts (insert X G);  X: parts H |] \
    3.42  \              ==> Y: parts (G Un H)";
    3.43  by (etac parts_trans 1);
    3.44 -by (Auto_tac());
    3.45 +by Auto_tac;
    3.46  qed "parts_cut";
    3.47  
    3.48  goal thy "!!H. X: parts H ==> parts (insert X H) = parts H";
    3.49 @@ -279,7 +279,7 @@
    3.50  by (rtac equalityI 1);
    3.51  by (rtac subsetI 1);
    3.52  by (etac parts.induct 1);
    3.53 -by (Auto_tac());
    3.54 +by Auto_tac;
    3.55  by (etac parts.induct 1);
    3.56  by (ALLGOALS (blast_tac (claset() addIs [parts.Body])));
    3.57  qed "parts_insert_Crypt";
    3.58 @@ -289,7 +289,7 @@
    3.59  by (rtac equalityI 1);
    3.60  by (rtac subsetI 1);
    3.61  by (etac parts.induct 1);
    3.62 -by (Auto_tac());
    3.63 +by Auto_tac;
    3.64  by (etac parts.induct 1);
    3.65  by (ALLGOALS (blast_tac (claset() addIs [parts.Fst, parts.Snd])));
    3.66  qed "parts_insert_MPair";
    3.67 @@ -300,9 +300,9 @@
    3.68  
    3.69  
    3.70  goal thy "parts (Key``N) = Key``N";
    3.71 -by (Auto_tac());
    3.72 +by Auto_tac;
    3.73  by (etac parts.induct 1);
    3.74 -by (Auto_tac());
    3.75 +by Auto_tac;
    3.76  qed "parts_image_Key";
    3.77  Addsimps [parts_image_Key];
    3.78  
    3.79 @@ -359,9 +359,9 @@
    3.80  Addsimps [parts_analz];
    3.81  
    3.82  goal thy "analz (parts H) = parts H";
    3.83 -by (Auto_tac());
    3.84 +by Auto_tac;
    3.85  by (etac analz.induct 1);
    3.86 -by (Auto_tac());
    3.87 +by Auto_tac;
    3.88  qed "analz_parts";
    3.89  Addsimps [analz_parts];
    3.90  
    3.91 @@ -427,7 +427,7 @@
    3.92  by (rtac equalityI 1);
    3.93  by (rtac subsetI 1);
    3.94  by (etac analz.induct 1);
    3.95 -by (Auto_tac());
    3.96 +by Auto_tac;
    3.97  by (etac analz.induct 1);
    3.98  by (ALLGOALS (blast_tac (claset() addIs [analz.Fst, analz.Snd])));
    3.99  qed "analz_insert_MPair";
   3.100 @@ -450,9 +450,9 @@
   3.101  goal thy "!!H. Key (invKey K) : analz H ==>  \
   3.102  \              insert (Crypt K X) (analz (insert X H)) <= \
   3.103  \              analz (insert (Crypt K X) H)";
   3.104 -by (Auto_tac());
   3.105 +by Auto_tac;
   3.106  by (eres_inst_tac [("za","x")] analz.induct 1);
   3.107 -by (Auto_tac());
   3.108 +by Auto_tac;
   3.109  by (blast_tac (claset() addIs [analz_insertI, analz.Decrypt]) 1);
   3.110  val lemma2 = result();
   3.111  
   3.112 @@ -484,14 +484,14 @@
   3.113  \          insert (Crypt K X) (analz (insert X H))";
   3.114  by (rtac subsetI 1);
   3.115  by (etac analz.induct 1);
   3.116 -by (Auto_tac());
   3.117 +by Auto_tac;
   3.118  qed "analz_insert_Crypt_subset";
   3.119  
   3.120  
   3.121  goal thy "analz (Key``N) = Key``N";
   3.122 -by (Auto_tac());
   3.123 +by Auto_tac;
   3.124  by (etac analz.induct 1);
   3.125 -by (Auto_tac());
   3.126 +by Auto_tac;
   3.127  qed "analz_image_Key";
   3.128  
   3.129  Addsimps [analz_image_Key];
   3.130 @@ -808,7 +808,7 @@
   3.131  qed "MPair_eq_HPair";
   3.132  
   3.133  goalw thy [HPair_def] "(Hash[X] Y = {|X',Y'|}) = (X' = Hash{|X,Y|} & Y'=Y)";
   3.134 -by (Auto_tac());
   3.135 +by Auto_tac;
   3.136  qed "HPair_eq_MPair";
   3.137  
   3.138  AddIffs [HPair_eq, MPair_eq_HPair, HPair_eq_MPair];
     4.1 --- a/src/HOL/Auth/NS_Public.ML	Tue Dec 23 11:56:09 1997 +0100
     4.2 +++ b/src/HOL/Auth/NS_Public.ML	Wed Dec 24 10:02:30 1997 +0100
     4.3 @@ -36,7 +36,7 @@
     4.4  (*Nobody sends themselves messages*)
     4.5  goal thy "!!evs. evs : ns_public ==> ALL A X. Says A A X ~: set evs";
     4.6  by (etac ns_public.induct 1);
     4.7 -by (Auto_tac());
     4.8 +by Auto_tac;
     4.9  qed_spec_mp "not_Says_to_self";
    4.10  Addsimps [not_Says_to_self];
    4.11  AddSEs   [not_Says_to_self RSN (2, rev_notE)];
    4.12 @@ -66,7 +66,7 @@
    4.13  
    4.14  goal thy 
    4.15   "!!A. evs: ns_public ==> (Key (priK A) : analz (spies evs)) = (A : bad)";
    4.16 -by (Auto_tac());
    4.17 +by Auto_tac;
    4.18  qed "Spy_analz_priK";
    4.19  Addsimps [Spy_analz_priK];
    4.20  
     5.1 --- a/src/HOL/Auth/NS_Public_Bad.ML	Tue Dec 23 11:56:09 1997 +0100
     5.2 +++ b/src/HOL/Auth/NS_Public_Bad.ML	Wed Dec 24 10:02:30 1997 +0100
     5.3 @@ -33,7 +33,7 @@
     5.4  (*Nobody sends themselves messages*)
     5.5  goal thy "!!evs. evs : ns_public ==> ALL A X. Says A A X ~: set evs";
     5.6  by (etac ns_public.induct 1);
     5.7 -by (Auto_tac());
     5.8 +by Auto_tac;
     5.9  qed_spec_mp "not_Says_to_self";
    5.10  Addsimps [not_Says_to_self];
    5.11  AddSEs   [not_Says_to_self RSN (2, rev_notE)];
    5.12 @@ -286,7 +286,7 @@
    5.13  (*NS3: unicity of NB identifies A and NA, but not B*)
    5.14  by (forw_inst_tac [("A'","A")] (Says_imp_spies RS parts.Inj RS unique_NB) 1
    5.15      THEN REPEAT (eresolve_tac [asm_rl, Says_imp_spies RS parts.Inj] 1));
    5.16 -by (Auto_tac());
    5.17 +by Auto_tac;
    5.18  by (rename_tac "C B' evs3" 1);
    5.19  
    5.20  (*
     6.1 --- a/src/HOL/Auth/NS_Shared.ML	Tue Dec 23 11:56:09 1997 +0100
     6.2 +++ b/src/HOL/Auth/NS_Shared.ML	Wed Dec 24 10:02:30 1997 +0100
     6.3 @@ -45,7 +45,7 @@
     6.4  (*Nobody sends themselves messages*)
     6.5  goal thy "!!evs. evs : ns_shared ==> ALL A X. Says A A X ~: set evs";
     6.6  by (etac ns_shared.induct 1);
     6.7 -by (Auto_tac());
     6.8 +by Auto_tac;
     6.9  qed_spec_mp "not_Says_to_self";
    6.10  Addsimps [not_Says_to_self];
    6.11  AddSEs   [not_Says_to_self RSN (2, rev_notE)];
    6.12 @@ -84,7 +84,7 @@
    6.13  
    6.14  goal thy 
    6.15   "!!evs. evs : ns_shared ==> (Key (shrK A) : analz (spies evs)) = (A : bad)";
    6.16 -by (Auto_tac());
    6.17 +by Auto_tac;
    6.18  qed "Spy_analz_shrK";
    6.19  Addsimps [Spy_analz_shrK];
    6.20  
    6.21 @@ -124,7 +124,7 @@
    6.22  \            K' = shrK A";
    6.23  by (etac rev_mp 1);
    6.24  by (etac ns_shared.induct 1);
    6.25 -by (Auto_tac());
    6.26 +by Auto_tac;
    6.27  qed "Says_Server_message_form";
    6.28  
    6.29  
    6.30 @@ -193,7 +193,7 @@
    6.31  by (blast_tac (claset() addSEs partsEs
    6.32                          addDs [impOfSubs parts_insert_subset_Un]) 1);
    6.33  (*Base, NS4 and NS5*)
    6.34 -by (Auto_tac());
    6.35 +by Auto_tac;
    6.36  result();
    6.37  
    6.38  
     7.1 --- a/src/HOL/Auth/OtwayRees.ML	Tue Dec 23 11:56:09 1997 +0100
     7.2 +++ b/src/HOL/Auth/OtwayRees.ML	Wed Dec 24 10:02:30 1997 +0100
     7.3 @@ -39,7 +39,7 @@
     7.4  (*Nobody sends themselves messages*)
     7.5  goal thy "!!evs. evs : otway ==> ALL A X. Says A A X ~: set evs";
     7.6  by (etac otway.induct 1);
     7.7 -by (Auto_tac());
     7.8 +by Auto_tac;
     7.9  qed_spec_mp "not_Says_to_self";
    7.10  Addsimps [not_Says_to_self];
    7.11  AddSEs   [not_Says_to_self RSN (2, rev_notE)];
    7.12 @@ -49,13 +49,13 @@
    7.13  
    7.14  goal thy "!!evs. Says A' B {|N, Agent A, Agent B, X|} : set evs \
    7.15  \                ==> X : analz (spies evs)";
    7.16 -bd (Says_imp_spies RS analz.Inj) 1;
    7.17 +by (dtac (Says_imp_spies RS analz.Inj) 1);
    7.18  by (Blast_tac 1);
    7.19  qed "OR2_analz_spies";
    7.20  
    7.21  goal thy "!!evs. Says S' B {|N, X, Crypt (shrK B) X'|} : set evs \
    7.22  \                ==> X : analz (spies evs)";
    7.23 -bd (Says_imp_spies RS analz.Inj) 1;
    7.24 +by (dtac (Says_imp_spies RS analz.Inj) 1);
    7.25  by (Blast_tac 1);
    7.26  qed "OR4_analz_spies";
    7.27  
     8.1 --- a/src/HOL/Auth/OtwayRees_AN.ML	Tue Dec 23 11:56:09 1997 +0100
     8.2 +++ b/src/HOL/Auth/OtwayRees_AN.ML	Wed Dec 24 10:02:30 1997 +0100
     8.3 @@ -39,7 +39,7 @@
     8.4  (*Nobody sends themselves messages*)
     8.5  goal thy "!!evs. evs : otway ==> ALL A X. Says A A X ~: set evs";
     8.6  by (etac otway.induct 1);
     8.7 -by (Auto_tac());
     8.8 +by Auto_tac;
     8.9  qed_spec_mp "not_Says_to_self";
    8.10  Addsimps [not_Says_to_self];
    8.11  AddSEs   [not_Says_to_self RSN (2, rev_notE)];
    8.12 @@ -49,7 +49,7 @@
    8.13  
    8.14  goal thy "!!evs. Says S' B {|X, Crypt(shrK B) X'|} : set evs ==> \
    8.15  \                X : analz (spies evs)";
    8.16 -bd (Says_imp_spies RS analz.Inj) 1;
    8.17 +by (dtac (Says_imp_spies RS analz.Inj) 1);
    8.18  by (Blast_tac 1);
    8.19  qed "OR4_analz_spies";
    8.20  
     9.1 --- a/src/HOL/Auth/OtwayRees_Bad.ML	Tue Dec 23 11:56:09 1997 +0100
     9.2 +++ b/src/HOL/Auth/OtwayRees_Bad.ML	Wed Dec 24 10:02:30 1997 +0100
     9.3 @@ -38,7 +38,7 @@
     9.4  (*Nobody sends themselves messages*)
     9.5  goal thy "!!evs. evs : otway ==> ALL A X. Says A A X ~: set evs";
     9.6  by (etac otway.induct 1);
     9.7 -by (Auto_tac());
     9.8 +by Auto_tac;
     9.9  qed_spec_mp "not_Says_to_self";
    9.10  Addsimps [not_Says_to_self];
    9.11  AddSEs   [not_Says_to_self RSN (2, rev_notE)];
    10.1 --- a/src/HOL/Auth/Public.ML	Tue Dec 23 11:56:09 1997 +0100
    10.2 +++ b/src/HOL/Auth/Public.ML	Wed Dec 24 10:02:30 1997 +0100
    10.3 @@ -38,16 +38,16 @@
    10.4  (** "Image" equations that hold for injective functions **)
    10.5  
    10.6  goal thy "(invKey x : invKey``A) = (x:A)";
    10.7 -by (Auto_tac());
    10.8 +by Auto_tac;
    10.9  qed "invKey_image_eq";
   10.10  
   10.11  (*holds because invKey is injective*)
   10.12  goal thy "(pubK x : pubK``A) = (x:A)";
   10.13 -by (Auto_tac());
   10.14 +by Auto_tac;
   10.15  qed "pubK_image_eq";
   10.16  
   10.17  goal thy "(priK x ~: pubK``A)";
   10.18 -by (Auto_tac());
   10.19 +by Auto_tac;
   10.20  qed "priK_pubK_image_eq";
   10.21  Addsimps [invKey_image_eq, pubK_image_eq, priK_pubK_image_eq];
   10.22  
   10.23 @@ -67,7 +67,7 @@
   10.24  (*Agents see their own private keys!*)
   10.25  goal thy "Key (priK A) : initState A";
   10.26  by (induct_tac "A" 1);
   10.27 -by (Auto_tac());
   10.28 +by Auto_tac;
   10.29  qed "priK_in_initState";
   10.30  AddIffs [priK_in_initState];
   10.31  
   10.32 @@ -114,7 +114,7 @@
   10.33  
   10.34  goal thy "Nonce N ~: parts (initState B)";
   10.35  by (induct_tac "B" 1);
   10.36 -by (Auto_tac ());
   10.37 +by Auto_tac;
   10.38  qed "Nonce_notin_initState";
   10.39  AddIffs [Nonce_notin_initState];
   10.40  
    11.1 --- a/src/HOL/Auth/Recur.ML	Tue Dec 23 11:56:09 1997 +0100
    11.2 +++ b/src/HOL/Auth/Recur.ML	Wed Dec 24 10:02:30 1997 +0100
    11.3 @@ -77,7 +77,7 @@
    11.4  (*Nobody sends themselves messages*)
    11.5  goal thy "!!evs. evs : recur ==> ALL A X. Says A A X ~: set evs";
    11.6  by (etac recur.induct 1);
    11.7 -by (Auto_tac());
    11.8 +by Auto_tac;
    11.9  qed_spec_mp "not_Says_to_self";
   11.10  Addsimps [not_Says_to_self];
   11.11  AddSEs   [not_Says_to_self RSN (2, rev_notE)];
   11.12 @@ -175,7 +175,7 @@
   11.13  \        ==> K : range shrK";
   11.14  by (etac rev_mp 1);
   11.15  by (etac (respond_imp_responses RS responses.induct) 1);
   11.16 -by (Auto_tac());
   11.17 +by Auto_tac;
   11.18  qed_spec_mp "Key_in_keysFor_parts";
   11.19  
   11.20  
   11.21 @@ -358,7 +358,7 @@
   11.22  \        ==> ALL C X Y. Says Server C {|X, Agent Server, Y|} ~: set evs";
   11.23  by (etac recur.induct 1);
   11.24  by (etac (respond.induct) 5);
   11.25 -by (Auto_tac());
   11.26 +by Auto_tac;
   11.27  qed_spec_mp "Says_Server_not";
   11.28  AddSEs [Says_Server_not RSN (2,rev_notE)];
   11.29  
   11.30 @@ -479,7 +479,7 @@
   11.31  \        ==> Hash {|Key (shrK B), M|} : parts H";
   11.32  by (etac rev_mp 1);
   11.33  by (etac (respond_imp_responses RS responses.induct) 1);
   11.34 -by (Auto_tac());
   11.35 +by Auto_tac;
   11.36  qed "Hash_in_parts_respond";
   11.37  
   11.38  (*Only RA1 or RA2 can have caused such a part of a message to appear.
    12.1 --- a/src/HOL/Auth/Shared.ML	Tue Dec 23 11:56:09 1997 +0100
    12.2 +++ b/src/HOL/Auth/Shared.ML	Wed Dec 24 10:02:30 1997 +0100
    12.3 @@ -24,7 +24,7 @@
    12.4  
    12.5  goalw thy [keysFor_def] "keysFor (parts (initState C)) = {}";
    12.6  by (induct_tac "C" 1);
    12.7 -by (Auto_tac ());
    12.8 +by Auto_tac;
    12.9  qed "keysFor_parts_initState";
   12.10  Addsimps [keysFor_parts_initState];
   12.11  
   12.12 @@ -70,7 +70,7 @@
   12.13  (*Agents see their own shared keys!*)
   12.14  goal thy "Key (shrK A) : initState A";
   12.15  by (induct_tac "A" 1);
   12.16 -by (Auto_tac());
   12.17 +by Auto_tac;
   12.18  qed "shrK_in_initState";
   12.19  AddIffs [shrK_in_initState];
   12.20  
   12.21 @@ -97,7 +97,7 @@
   12.22  
   12.23  goal thy "Nonce N ~: parts (initState B)";
   12.24  by (induct_tac "B" 1);
   12.25 -by (Auto_tac ());
   12.26 +by Auto_tac;
   12.27  qed "Nonce_notin_initState";
   12.28  AddIffs [Nonce_notin_initState];
   12.29  
   12.30 @@ -169,7 +169,7 @@
   12.31  by (etac exE 1);
   12.32  by (cut_inst_tac [("evs","evs'")] 
   12.33      (Finites.emptyI RS Finites.insertI RS Key_supply_ax) 1);
   12.34 -by (Auto_tac());
   12.35 +by Auto_tac;
   12.36  qed "Key_supply2";
   12.37  
   12.38  goal thy "EX K K' K''. Key K ~: used evs & Key K' ~: used evs' & \
    13.1 --- a/src/HOL/Auth/TLS.ML	Tue Dec 23 11:56:09 1997 +0100
    13.2 +++ b/src/HOL/Auth/TLS.ML	Wed Dec 24 10:02:30 1997 +0100
    13.3 @@ -130,7 +130,7 @@
    13.4  (*Nobody sends themselves messages*)
    13.5  goal thy "!!evs. evs : tls ==> ALL A X. Says A A X ~: set evs";
    13.6  by (etac tls.induct 1);
    13.7 -by (Auto_tac());
    13.8 +by Auto_tac;
    13.9  qed_spec_mp "not_Says_to_self";
   13.10  Addsimps [not_Says_to_self];
   13.11  AddSEs   [not_Says_to_self RSN (2, rev_notE)];
    14.1 --- a/src/HOL/Auth/WooLam.ML	Tue Dec 23 11:56:09 1997 +0100
    14.2 +++ b/src/HOL/Auth/WooLam.ML	Wed Dec 24 10:02:30 1997 +0100
    14.3 @@ -37,7 +37,7 @@
    14.4  (*Nobody sends themselves messages*)
    14.5  goal thy "!!evs. evs : woolam ==> ALL A X. Says A A X ~: set evs";
    14.6  by (etac woolam.induct 1);
    14.7 -by (Auto_tac());
    14.8 +by Auto_tac;
    14.9  qed_spec_mp "not_Says_to_self";
   14.10  Addsimps [not_Says_to_self];
   14.11  AddSEs   [not_Says_to_self RSN (2, rev_notE)];
   14.12 @@ -72,7 +72,7 @@
   14.13  
   14.14  goal thy 
   14.15   "!!evs. evs : woolam ==> (Key (shrK A) : analz (spies evs)) = (A : bad)";
   14.16 -by (Auto_tac());
   14.17 +by Auto_tac;
   14.18  qed "Spy_analz_shrK";
   14.19  Addsimps [Spy_analz_shrK];
   14.20  
    15.1 --- a/src/HOL/Auth/Yahalom.ML	Tue Dec 23 11:56:09 1997 +0100
    15.2 +++ b/src/HOL/Auth/Yahalom.ML	Wed Dec 24 10:02:30 1997 +0100
    15.3 @@ -34,7 +34,7 @@
    15.4  (*Nobody sends themselves messages*)
    15.5  goal thy "!!evs. evs: yahalom ==> ALL A X. Says A A X ~: set evs";
    15.6  by (etac yahalom.induct 1);
    15.7 -by (Auto_tac());
    15.8 +by Auto_tac;
    15.9  qed_spec_mp "not_Says_to_self";
   15.10  Addsimps [not_Says_to_self];
   15.11  AddSEs   [not_Says_to_self RSN (2, rev_notE)];
    16.1 --- a/src/HOL/Auth/Yahalom2.ML	Tue Dec 23 11:56:09 1997 +0100
    16.2 +++ b/src/HOL/Auth/Yahalom2.ML	Wed Dec 24 10:02:30 1997 +0100
    16.3 @@ -34,7 +34,7 @@
    16.4  (*Nobody sends themselves messages*)
    16.5  goal thy "!!evs. evs: yahalom ==> ALL A X. Says A A X ~: set evs";
    16.6  by (etac yahalom.induct 1);
    16.7 -by (Auto_tac());
    16.8 +by Auto_tac;
    16.9  qed_spec_mp "not_Says_to_self";
   16.10  Addsimps [not_Says_to_self];
   16.11  AddSEs   [not_Says_to_self RSN (2, rev_notE)];
    17.1 --- a/src/HOL/Divides.ML	Tue Dec 23 11:56:09 1997 +0100
    17.2 +++ b/src/HOL/Divides.ML	Wed Dec 24 10:02:30 1997 +0100
    17.3 @@ -244,7 +244,7 @@
    17.4  goal Divides.thy "(0 < m mod 2) = (m mod 2 = 1)";
    17.5  by (subgoal_tac "m mod 2 < 2" 1);
    17.6  by (asm_simp_tac (simpset() addsimps [mod_less_divisor]) 2);
    17.7 -by (Auto_tac());
    17.8 +by Auto_tac;
    17.9  qed "mod2_gr_0";
   17.10  Addsimps [mod2_gr_0];
   17.11  
    18.1 --- a/src/HOL/Finite.ML	Tue Dec 23 11:56:09 1997 +0100
    18.2 +++ b/src/HOL/Finite.ML	Wed Dec 24 10:02:30 1997 +0100
    18.3 @@ -192,7 +192,7 @@
    18.4    by (simp_tac (simpset() addsplits [expand_split]) 1);
    18.5   by (etac finite_imageI 1);
    18.6  by (simp_tac (simpset() addsimps [inverse_def,image_def]) 1);
    18.7 -by (Auto_tac());
    18.8 +by Auto_tac;
    18.9   by (rtac bexI 1);
   18.10   by (assume_tac 2);
   18.11   by (Simp_tac 1);
    19.1 --- a/src/HOL/IMP/Denotation.ML	Tue Dec 23 11:56:09 1997 +0100
    19.2 +++ b/src/HOL/IMP/Denotation.ML	Wed Dec 24 10:02:30 1997 +0100
    19.3 @@ -29,7 +29,7 @@
    19.4  
    19.5  (* start with rule induction *)
    19.6  by (etac evalc.induct 1);
    19.7 -by (Auto_tac());
    19.8 +by Auto_tac;
    19.9  (* while *)
   19.10  by (rewtac Gamma_def);
   19.11  by (stac (rewrite_rule [Gamma_def] (Gamma_mono RS lfp_Tarski)) 1);
    20.1 --- a/src/HOL/IMP/Transition.ML	Tue Dec 23 11:56:09 1997 +0100
    20.2 +++ b/src/HOL/IMP/Transition.ML	Wed Dec 24 10:02:30 1997 +0100
    20.3 @@ -193,7 +193,7 @@
    20.4  goal Transition.thy 
    20.5    "!!c s. ((c,s) -1-> (c',s')) ==> (!t. <c',s'> -c-> t --> <c,s> -c-> t)";
    20.6  by (etac evalc1.induct 1);
    20.7 -by (Auto_tac());
    20.8 +by Auto_tac;
    20.9  qed_spec_mp "FB_lemma3";
   20.10  
   20.11  val [major] = goal Transition.thy
    21.1 --- a/src/HOL/IOA/Solve.ML	Tue Dec 23 11:56:09 1997 +0100
    21.2 +++ b/src/HOL/IOA/Solve.ML	Wed Dec 24 10:02:30 1997 +0100
    21.3 @@ -205,5 +205,5 @@
    21.4  by (rtac impI 1);
    21.5  by (etac conjE 1);
    21.6  by (cut_inst_tac [("C","C"),("g","g"),("s","s")] reachable_rename_ioa 1);
    21.7 -by (Auto_tac());
    21.8 +by Auto_tac;
    21.9  qed"rename_through_pmap";
    22.1 --- a/src/HOL/Induct/Exp.ML	Tue Dec 23 11:56:09 1997 +0100
    22.2 +++ b/src/HOL/Induct/Exp.ML	Wed Dec 24 10:02:30 1997 +0100
    22.3 @@ -109,7 +109,7 @@
    22.4  (*This theorem says that "WHILE TRUE DO c" cannot terminate*)
    22.5  goal thy "!!x. (c', s) -[eval]-> t ==> (c' = WHILE (N 0) DO c) --> False";
    22.6  by (etac exec.induct 1);
    22.7 -by (Auto_tac());
    22.8 +by Auto_tac;
    22.9  bind_thm ("while_true_E", refl RSN (2, result() RS mp));
   22.10  
   22.11  
    23.1 --- a/src/HOL/Induct/LFilter.ML	Tue Dec 23 11:56:09 1997 +0100
    23.2 +++ b/src/HOL/Induct/LFilter.ML	Wed Dec 24 10:02:30 1997 +0100
    23.3 @@ -190,7 +190,7 @@
    23.4  (*Cases: p x is true or false*)
    23.5  by (rtac (lfilter_cases RS disjE) 1);
    23.6  by (etac ssubst 1);
    23.7 -by (Auto_tac());
    23.8 +by Auto_tac;
    23.9  qed "lfilter_idem";
   23.10  
   23.11  
   23.12 @@ -211,7 +211,7 @@
   23.13  \              ==> (l, LCons x l') : findRel q --> ~ p x     \
   23.14  \                  --> l' : Domain (findRel (%x. p x & q x))";
   23.15  by (etac findRel.induct 1);
   23.16 -by (Auto_tac());
   23.17 +by Auto_tac;
   23.18  qed_spec_mp "findRel_not_conj_Domain";
   23.19  
   23.20  
   23.21 @@ -229,9 +229,9 @@
   23.22  by (etac findRel.induct 1);
   23.23  by (blast_tac (claset() addSDs [sym RS lfilter_eq_LCons]
   23.24                         addIs  [findRel_conj]) 1);
   23.25 -by (Auto_tac());
   23.26 +by Auto_tac;
   23.27  by (dtac (sym RS lfilter_eq_LCons) 1);
   23.28 -by (Auto_tac());
   23.29 +by Auto_tac;
   23.30  by (dtac spec 1);
   23.31  by (dtac (refl RS rev_mp) 1);
   23.32  by (blast_tac (claset() addIs [findRel_conj2]) 1);
   23.33 @@ -303,7 +303,7 @@
   23.34  \              (EX y l''. x = f y & l' = lmap f l'' & l = LCons y l'')";
   23.35  by (stac (lmap_def RS def_llist_corec) 1);
   23.36  by (res_inst_tac [("l", "l")] llistE 1);
   23.37 -by (Auto_tac());
   23.38 +by Auto_tac;
   23.39  qed_spec_mp "lmap_eq_LCons";
   23.40  
   23.41  
    24.1 --- a/src/HOL/Induct/LList.ML	Tue Dec 23 11:56:09 1997 +0100
    24.2 +++ b/src/HOL/Induct/LList.ML	Wed Dec 24 10:02:30 1997 +0100
    24.3 @@ -652,7 +652,7 @@
    24.4  (*Surprisingly hard to prove.  Used with lfilter*)
    24.5  goalw thy [llistD_Fun_def, prod_fun_def]
    24.6      "!!A B. A<=B ==> llistD_Fun A <= llistD_Fun B";
    24.7 -by (Auto_tac());
    24.8 +by Auto_tac;
    24.9  by (rtac image_eqI 1);
   24.10  by (fast_tac (claset() addss (simpset())) 1);
   24.11  by (blast_tac (claset() addIs [impOfSubs LListD_Fun_mono]) 1);
    25.1 --- a/src/HOL/Induct/Mutil.ML	Tue Dec 23 11:56:09 1997 +0100
    25.2 +++ b/src/HOL/Induct/Mutil.ML	Wed Dec 24 10:02:30 1997 +0100
    25.3 @@ -53,7 +53,7 @@
    25.4  \    {(i, n+n), (i, Suc(n+n))}" 1);
    25.5  by (Blast_tac 2);
    25.6  by (asm_simp_tac (simpset() addsimps [domino.horiz]) 1);
    25.7 -by (Auto_tac());
    25.8 +by Auto_tac;
    25.9  qed "dominoes_tile_row";
   25.10  
   25.11  goal thy "(below m) Times below(n+n) : tiling domino";
    26.1 --- a/src/HOL/Integ/Integ.ML	Tue Dec 23 11:56:09 1997 +0100
    26.2 +++ b/src/HOL/Integ/Integ.ML	Wed Dec 24 10:02:30 1997 +0100
    26.3 @@ -847,7 +847,7 @@
    26.4  	  negative_eq_positive, not_znat_zless_negative]; 
    26.5  
    26.6  goalw Integ.thy [zdiff_def,zless_def] "!! x. znegative x = (x < $# 0)";
    26.7 -  by (Auto_tac()); 
    26.8 +  by Auto_tac; 
    26.9  qed "znegative_less_0"; 
   26.10  
   26.11  goalw Integ.thy [zdiff_def,zless_def] "!! x. (~znegative x) = ($# 0 <= x)";
   26.12 @@ -868,7 +868,7 @@
   26.13    by (dtac zle_imp_zless_or_eq 1); 
   26.14    by (etac disjE 1); 
   26.15    by (dtac zless_eq_zadd_Suc 1); 
   26.16 -  by (Auto_tac()); 
   26.17 +  by Auto_tac; 
   26.18  qed "not_znegativeD"; 
   26.19  
   26.20  (* a case theorem distinguishing positive and negative int *)  
    27.1 --- a/src/HOL/Option.ML	Tue Dec 23 11:56:09 1997 +0100
    27.2 +++ b/src/HOL/Option.ML	Wed Dec 24 10:02:30 1997 +0100
    27.3 @@ -8,7 +8,7 @@
    27.4  open Option;
    27.5  
    27.6  qed_goal "not_None_eq" thy "(x ~= None) = (? y. x = Some y)"
    27.7 -	(K [option.induct_tac "x" 1, Auto_tac()]);
    27.8 +	(K [option.induct_tac "x" 1, Auto_tac]);
    27.9  
   27.10  section "case analysis in premises";
   27.11  
   27.12 @@ -31,7 +31,7 @@
   27.13  	res_inst_tac [("opt","x")] optionE 1,
   27.14  	 forward_tac prems 1,
   27.15  	  forward_tac prems 3, 
   27.16 -	   Auto_tac()]);
   27.17 +	   Auto_tac]);
   27.18  fun option_case_tac i = EVERY [
   27.19  	etac option_caseE i,
   27.20  	 hyp_subst_tac (i+1),
   27.21 @@ -56,4 +56,4 @@
   27.22  val option_map_SomeD = prove_goalw thy [option_map_def]
   27.23  	"!!x. option_map f x = Some y ==> ? z. x = Some z & f z = y" (K [
   27.24  	optionE_tac "x" 1,
   27.25 -	 Auto_tac()]);
   27.26 +	 Auto_tac]);
    28.1 --- a/src/HOL/Quot/HQUOT.ML	Tue Dec 23 11:56:09 1997 +0100
    28.2 +++ b/src/HOL/Quot/HQUOT.ML	Wed Dec 24 10:02:30 1997 +0100
    28.3 @@ -82,14 +82,14 @@
    28.4  by (cut_facts_tac prems 1);
    28.5  by (rtac notI 1);
    28.6  by (dtac per_class_eqE 1);
    28.7 -by (Auto_tac());
    28.8 +by Auto_tac;
    28.9  qed "per_class_neqI";
   28.10  
   28.11  val prems = goal thy "~(x::'a::er)===y==><[x]>~=<[y]>";
   28.12  by (cut_facts_tac prems 1);
   28.13  by (rtac notI 1);
   28.14  by (dtac er_class_eqE 1);
   28.15 -by (Auto_tac());
   28.16 +by Auto_tac;
   28.17  qed "er_class_neqI";
   28.18  
   28.19  val prems = goal thy "<[x]>~=<[y]>==>~x===y";
    29.1 --- a/src/HOL/Quot/NPAIR.ML	Tue Dec 23 11:56:09 1997 +0100
    29.2 +++ b/src/HOL/Quot/NPAIR.ML	Wed Dec 24 10:02:30 1997 +0100
    29.3 @@ -7,13 +7,13 @@
    29.4  open NPAIR;
    29.5  
    29.6  goalw thy [rep_NP_def] "rep_NP(abs_NP np) = np";
    29.7 -by (Auto_tac());
    29.8 +by Auto_tac;
    29.9  qed "rep_abs_NP";
   29.10  
   29.11  Addsimps [rep_abs_NP];
   29.12  
   29.13  val prems = goalw thy [per_NP_def] "eqv (x::NP) y ==> eqv y x";
   29.14  by (cut_facts_tac prems 1);
   29.15 -by (Auto_tac());
   29.16 +by Auto_tac;
   29.17  qed "per_sym_NP";
   29.18  
    30.1 --- a/src/HOL/Set.ML	Tue Dec 23 11:56:09 1997 +0100
    30.2 +++ b/src/HOL/Set.ML	Wed Dec 24 10:02:30 1997 +0100
    30.3 @@ -470,7 +470,7 @@
    30.4  
    30.5  (*The order of the premises presupposes that A is rigid; b may be flexible*)
    30.6  goal Set.thy "!!b. [| a:A;  b: B(a) |] ==> b: (UN x:A. B(x))";
    30.7 -by (Auto_tac());
    30.8 +by Auto_tac;
    30.9  qed "UN_I";
   30.10  
   30.11  val major::prems = goalw Set.thy [UNION_def]
   30.12 @@ -494,7 +494,7 @@
   30.13  section "Intersections of families -- INTER x:A. B(x) is Inter(B``A)";
   30.14  
   30.15  goalw Set.thy [INTER_def] "(b: (INT x:A. B(x))) = (ALL x:A. b: B(x))";
   30.16 -by (Auto_tac());
   30.17 +by Auto_tac;
   30.18  qed "INT_iff";
   30.19  
   30.20  Addsimps [INT_iff];
   30.21 @@ -505,7 +505,7 @@
   30.22  qed "INT_I";
   30.23  
   30.24  goal Set.thy "!!b. [| b : (INT x:A. B(x));  a:A |] ==> b: B(a)";
   30.25 -by (Auto_tac());
   30.26 +by Auto_tac;
   30.27  qed "INT_D";
   30.28  
   30.29  (*"Classical" elimination -- by the Excluded Middle on a:A *)
   30.30 @@ -537,7 +537,7 @@
   30.31  
   30.32  (*The order of the premises presupposes that C is rigid; A may be flexible*)
   30.33  goal Set.thy "!!X. [| X:C;  A:X |] ==> A : Union(C)";
   30.34 -by (Auto_tac());
   30.35 +by Auto_tac;
   30.36  qed "UnionI";
   30.37  
   30.38  val major::prems = goalw Set.thy [Union_def]
   30.39 @@ -566,7 +566,7 @@
   30.40  (*A "destruct" rule -- every X in C contains A as an element, but
   30.41    A:X can hold when X:C does not!  This rule is analogous to "spec". *)
   30.42  goal Set.thy "!!X. [| A : Inter(C);  X:C |] ==> A:X";
   30.43 -by (Auto_tac());
   30.44 +by Auto_tac;
   30.45  qed "InterD";
   30.46  
   30.47  (*"Classical" elimination rule -- does not require proving X:C *)
   30.48 @@ -672,7 +672,7 @@
   30.49  
   30.50  goalw Set.thy [psubset_def]
   30.51      "!!x. A < insert x B ==> (x ~: A) & A<=B | x:A & A-{x}<B";
   30.52 -by (Auto_tac());
   30.53 +by Auto_tac;
   30.54  qed "psubset_insertD";
   30.55  
   30.56  bind_thm ("psubset_eq", psubset_def RS meta_eq_to_obj_eq);
    31.1 --- a/src/HOL/Subst/Subst.ML	Tue Dec 23 11:56:09 1997 +0100
    31.2 +++ b/src/HOL/Subst/Subst.ML	Wed Dec 24 10:02:30 1997 +0100
    31.3 @@ -181,7 +181,7 @@
    31.4  by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [sdom_iff,srange_iff])));
    31.5  by (Blast_tac 2);
    31.6  by (safe_tac (claset() addSIs [exI, vars_var_iff RS iffD1 RS sym]));
    31.7 -by (Auto_tac());
    31.8 +by Auto_tac;
    31.9  qed_spec_mp "Var_intro";
   31.10  
   31.11  goal Subst.thy
    32.1 --- a/src/HOL/Sum.ML	Tue Dec 23 11:56:09 1997 +0100
    32.2 +++ b/src/HOL/Sum.ML	Wed Dec 24 10:02:30 1997 +0100
    32.3 @@ -149,7 +149,7 @@
    32.4  goal Sum.thy "R(sum_case f g s) = \
    32.5  \             ((! x. s = Inl(x) --> R(f(x))) & (! y. s = Inr(y) --> R(g(y))))";
    32.6  by (res_inst_tac [("s","s")] sumE 1);
    32.7 -by (Auto_tac());
    32.8 +by Auto_tac;
    32.9  qed "expand_sum_case";
   32.10  
   32.11  (*Prevents simplification of f and g: much faster*)
    33.1 --- a/src/HOL/TLA/Action.ML	Tue Dec 23 11:56:09 1997 +0100
    33.2 +++ b/src/HOL/TLA/Action.ML	Wed Dec 24 10:02:30 1997 +0100
    33.3 @@ -219,17 +219,17 @@
    33.4  
    33.5  qed_goalw "idle_squareI" Action.thy [square_def]
    33.6     "!!s t. ([[s,t]] |= unchanged v) ==> ([[s,t]] |= [A]_v)"
    33.7 -   (fn _ => [ Auto_tac() ]);
    33.8 +   (fn _ => [ Auto_tac ]);
    33.9  
   33.10  qed_goalw "busy_squareI" Action.thy [square_def]
   33.11     "!!s t. ([[s,t]] |= A) ==> ([[s,t]] |= [A]_v)"
   33.12 -   (fn _ => [ Auto_tac() ]);
   33.13 +   (fn _ => [ Auto_tac ]);
   33.14  
   33.15  qed_goalw "square_simulation" Action.thy [square_def]
   33.16     "[| unchanged f .& .~B .-> unchanged g;   \
   33.17  \      A .& .~unchanged g .-> B              \
   33.18  \   |] ==> [A]_f .-> [B]_g"
   33.19 -   (fn [p1,p2] => [Auto_tac(),
   33.20 +   (fn [p1,p2] => [Auto_tac,
   33.21                     etac (action_conjimpE p2) 1,
   33.22                     etac swap 3, etac (action_conjimpE p1) 3,
   33.23                     ALLGOALS atac
   33.24 @@ -237,11 +237,11 @@
   33.25                     
   33.26  qed_goalw "not_square" Action.thy [square_def,angle_def]
   33.27     "(.~ [A]_v) .= <.~A>_v"
   33.28 -   (fn _ => [ Auto_tac() ]);
   33.29 +   (fn _ => [ Auto_tac ]);
   33.30  
   33.31  qed_goalw "not_angle" Action.thy [square_def,angle_def]
   33.32     "(.~ <A>_v) .= [.~A]_v"
   33.33 -   (fn _ => [ Auto_tac() ]);
   33.34 +   (fn _ => [ Auto_tac ]);
   33.35  
   33.36  (* ============================== Facts about ENABLED ============================== *)
   33.37  
   33.38 @@ -278,22 +278,22 @@
   33.39  
   33.40  qed_goal "enabled_disj1" Action.thy
   33.41    "!!s. (Enabled F) s ==> (Enabled (F .| G)) s"
   33.42 -  (fn _ => [etac enabled_mono 1, Auto_tac()
   33.43 +  (fn _ => [etac enabled_mono 1, Auto_tac
   33.44  	   ]);
   33.45  
   33.46  qed_goal "enabled_disj2" Action.thy
   33.47    "!!s. (Enabled G) s ==> (Enabled (F .| G)) s"
   33.48 -  (fn _ => [etac enabled_mono 1, Auto_tac()
   33.49 +  (fn _ => [etac enabled_mono 1, Auto_tac
   33.50  	   ]);
   33.51  
   33.52  qed_goal "enabled_conj1" Action.thy
   33.53    "!!s. (Enabled (F .& G)) s ==> (Enabled F) s"
   33.54 -  (fn _ => [etac enabled_mono 1, Auto_tac()
   33.55 +  (fn _ => [etac enabled_mono 1, Auto_tac
   33.56             ]);
   33.57  
   33.58  qed_goal "enabled_conj2" Action.thy
   33.59    "!!s. (Enabled (F .& G)) s ==> (Enabled G) s"
   33.60 -  (fn _ => [etac enabled_mono 1, Auto_tac()
   33.61 +  (fn _ => [etac enabled_mono 1, Auto_tac
   33.62             ]);
   33.63  
   33.64  qed_goal "enabled_conjE" Action.thy
    34.1 --- a/src/HOL/TLA/Buffer/DBuffer.ML	Tue Dec 23 11:56:09 1997 +0100
    34.2 +++ b/src/HOL/TLA/Buffer/DBuffer.ML	Wed Dec 24 10:02:30 1997 +0100
    34.3 @@ -37,8 +37,8 @@
    34.4  goal DBuffer.thy "$Enabled (<DBDeq>_<inp,mid,out,q1,q2>) .= ($q2 .~= .[])";
    34.5  by (rewtac (action_rewrite DBDeq_visible));
    34.6  by (cut_facts_tac [DB_base] 1);
    34.7 -by (auto_tac (db_css addSEs2 [base_enabled,enabledE] 
    34.8 -                     addsimps2 [angle_def,DBDeq_def,Deq_def]));
    34.9 +by (old_auto_tac (db_css addSEs2 [base_enabled,enabledE] 
   34.10 +                         addsimps2 [angle_def,DBDeq_def,Deq_def]));
   34.11  qed "DBDeq_enabled";
   34.12  
   34.13  goal DBuffer.thy "<DBPass>_<inp,mid,out,q1,q2> .= DBPass";
    35.1 --- a/src/HOL/TLA/Inc/Inc.ML	Tue Dec 23 11:56:09 1997 +0100
    35.2 +++ b/src/HOL/TLA/Inc/Inc.ML	Wed Dec 24 10:02:30 1997 +0100
    35.3 @@ -171,7 +171,7 @@
    35.4    (fn _ => [auto_tac (Inc_css addSIs2 [(temp_mp N2_leadsto_a) RSN(2,leadsto_init)]),
    35.5  	    rewrite_goals_tac (Init_def::action_rews),
    35.6  	    pcount.induct_tac "pc2 (fst_st sigma)" 1,
    35.7 -	    Auto_tac()
    35.8 +	    Auto_tac
    35.9  	   ]);
   35.10  
   35.11  (* Now prove that the first component will eventually reach pc1 = b from pc1 = a *)
   35.12 @@ -217,7 +217,7 @@
   35.13    (fn _ => [auto_tac (Inc_css addSIs2 [(temp_mp N1_leadsto_b) RSN(2,leadsto_init)]),
   35.14  	    rewrite_goals_tac (Init_def::action_rews),
   35.15  	    pcount.induct_tac "pc1 (fst_st sigma)" 1,
   35.16 -	    Auto_tac()
   35.17 +	    Auto_tac
   35.18  	   ]);
   35.19  
   35.20  qed_goal "N1_enabled_at_b" Inc.thy
    36.1 --- a/src/HOL/TLA/Memory/MIlive.ML	Tue Dec 23 11:56:09 1997 +0100
    36.2 +++ b/src/HOL/TLA/Memory/MIlive.ML	Wed Dec 24 10:02:30 1997 +0100
    36.3 @@ -286,7 +286,7 @@
    36.4     "[](ImpNext p .& [HNext rmhist p]_<c p,r p,m p, rmhist@p> .& $(ImpInv rmhist p)) \
    36.5  \   .& SF(MClkReply memCh crCh cst p)_(c p) .& []<>($(S6 rmhist p))  \
    36.6  \   .-> []<>($(S1 rmhist p))"
    36.7 -   (fn _ => [Auto_tac(),
    36.8 +   (fn _ => [Auto_tac,
    36.9  	     subgoal_tac "sigma |= []<>(<MClkReply memCh crCh cst p>_(c p))" 1,
   36.10  	     eres_inst_tac [("P","<MClkReply memCh crCh cst p>_(c p)")]
   36.11  	                   EnsuresInfinite 1, atac 1,
    37.1 --- a/src/HOL/TLA/Memory/MemoryImplementation.ML	Tue Dec 23 11:56:09 1997 +0100
    37.2 +++ b/src/HOL/TLA/Memory/MemoryImplementation.ML	Wed Dec 24 10:02:30 1997 +0100
    37.3 @@ -77,7 +77,7 @@
    37.4     "Init(RALL p. $(ImpInit p)) .& [](RALL p. ImpNext p)  \
    37.5  \   .-> (EEX rmhist.    Init(RALL p. $(HInit rmhist p)) \
    37.6  \                    .& [](RALL p. [HNext rmhist p]_<c p, r p, m p, rmhist@p>))"
    37.7 -   (fn _ => [Auto_tac(),
    37.8 +   (fn _ => [Auto_tac,
    37.9               rtac historyI 1, TRYALL atac,
   37.10               action_simp_tac (simpset() addsimps [HInit_def]) [] [] 1,
   37.11               res_inst_tac [("x","p")] fun_cong 1, atac 1,
   37.12 @@ -87,7 +87,7 @@
   37.13  
   37.14  qed_goal "History" MemoryImplementation.thy
   37.15     "Implementation .-> (EEX rmhist. Hist rmhist)"
   37.16 -   (fn _ => [Auto_tac(),
   37.17 +   (fn _ => [Auto_tac,
   37.18               rtac ((temp_mp HistoryLemma) RS eex_mono) 1,
   37.19               SELECT_GOAL 
   37.20                 (auto_tac (MI_css 
   37.21 @@ -609,7 +609,7 @@
   37.22               action_simp_tac (simpset() addsimps [ImpNext_def])
   37.23                               [] [S4EnvUnchE,S4ClerkUnchE,S4RPCUnchE] 1,
   37.24               TRYALL (action_simp_tac (simpset() addsimps [square_def]) [] [S4WriteE]),
   37.25 -             Auto_tac()
   37.26 +             Auto_tac
   37.27              ]);
   37.28  
   37.29  qed_goal "Step2_2" MemoryImplementation.thy
   37.30 @@ -664,7 +664,7 @@
   37.31  (* The main theorem: introduce hiding and eliminate history variable. *)
   37.32  qed_goal "Implementation" MemoryImplementation.thy
   37.33     "Implementation .-> USpec memCh"
   37.34 -   (fn _ => [Auto_tac(),
   37.35 +   (fn _ => [Auto_tac,
   37.36               forward_tac [temp_mp History] 1,
   37.37               auto_tac (MI_css addsimps2 [USpec_def] 
   37.38                                addIs2 (map temp_mp [eexI, Impl_IUSpec])
    38.1 --- a/src/HOL/TLA/ROOT.ML	Tue Dec 23 11:56:09 1997 +0100
    38.2 +++ b/src/HOL/TLA/ROOT.ML	Wed Dec 24 10:02:30 1997 +0100
    38.3 @@ -14,6 +14,16 @@
    38.4  
    38.5  reset global_names;
    38.6  
    38.7 +(*FIXME: the old auto_tac is sometimes needed!*)
    38.8 +fun old_auto_tac (cs,ss) = 
    38.9 +    let val cs' = cs addss ss 
   38.10 +    in  EVERY [TRY (safe_tac cs'),
   38.11 +               REPEAT (FIRSTGOAL (fast_tac cs')),
   38.12 +               TRY (safe_tac (cs addSss ss)),
   38.13 +               prune_params_tac] 
   38.14 +    end;
   38.15 +
   38.16 +
   38.17  use_thy "TLA";
   38.18  
   38.19  val TLA_build_completed = ();
    39.1 --- a/src/HOL/TLA/TLA.ML	Tue Dec 23 11:56:09 1997 +0100
    39.2 +++ b/src/HOL/TLA/TLA.ML	Wed Dec 24 10:02:30 1997 +0100
    39.3 @@ -135,7 +135,7 @@
    39.4  
    39.5  (* ------------------------ STL4 ------------------------------------------- *)
    39.6  qed_goal "STL4" TLA.thy "(F .-> G)  ==> ([]F .-> []G)"
    39.7 -   (fn [prem] => [Auto_tac(),
    39.8 +   (fn [prem] => [Auto_tac,
    39.9  		  rtac ((temp_mp normalT) RS mp) 1,
   39.10  		  REPEAT (ares_tac [prem, necT RS tempD] 1)
   39.11  		 ]);
   39.12 @@ -163,7 +163,7 @@
   39.13  
   39.14  (* ------------------------ STL5 ------------------------------------------- *)
   39.15  qed_goal "STL5" TLA.thy "([]F .& []G) .= ([](F .& G))"
   39.16 -   (fn _ => [Auto_tac(),
   39.17 +   (fn _ => [Auto_tac,
   39.18  	     subgoal_tac "sigma |= [](G .-> (F .& G))" 1,
   39.19  	     etac ((temp_mp normalT) RS mp) 1, atac 1,
   39.20  	     ALLGOALS (fast_tac (temp_cs addSEs [STL4E]))
   39.21 @@ -238,7 +238,7 @@
   39.22  
   39.23  qed_goalw "DmdImpl2" TLA.thy [dmd_def]
   39.24     "!!sigma. [| (sigma |= <>F); (sigma |= [](F .-> G)) |] ==> (sigma |= <>G)"
   39.25 -   (fn _ => [Auto_tac(),
   39.26 +   (fn _ => [Auto_tac,
   39.27  	     etac notE 1,
   39.28  	     merge_box_tac 1,
   39.29  	     fast_tac (temp_cs addSEs [STL4E]) 1
   39.30 @@ -256,7 +256,7 @@
   39.31  (* ------------------------ STL6 ------------------------------------------- *)
   39.32  (* Used in the proof of STL6, but useful in itself. *)
   39.33  qed_goalw "BoxDmdT" TLA.thy [dmd_def] "[]F .& <>G .-> <>([]F .& G)"
   39.34 -  (fn _ => [ Auto_tac(),
   39.35 +  (fn _ => [ Auto_tac,
   39.36               etac dup_boxE 1,
   39.37  	     merge_box_tac 1,
   39.38               etac swap 1,
   39.39 @@ -265,7 +265,7 @@
   39.40  
   39.41  (* weaker than BoxDmd, but more polymorphic (and often just right) *)
   39.42  qed_goalw "BoxDmdT2" TLA.thy [dmd_def] "<>F .& []G .-> <>(F .& G)"
   39.43 -  (fn _ => [ Auto_tac(),
   39.44 +  (fn _ => [ Auto_tac,
   39.45  	     merge_box_tac 1,
   39.46               fast_tac (temp_cs addSEs [notE,STL4E]) 1
   39.47  	   ]);
   39.48 @@ -278,7 +278,7 @@
   39.49  	    etac DmdImplE 1, rtac BoxDmdT 1,
   39.50  	    (* the second subgoal needs commutativity of .&, which complicates the proof *)
   39.51  	    etac DmdImplE 1,
   39.52 -	    Auto_tac(),
   39.53 +	    Auto_tac,
   39.54  	    etac (temp_conjimpE BoxDmdT) 1, atac 1, etac thin_rl 1,
   39.55  	    fast_tac (temp_cs addSEs [DmdImplE]) 1
   39.56  	   ]);
   39.57 @@ -347,10 +347,10 @@
   39.58  section "Further rewrites";
   39.59  
   39.60  qed_goalw "NotBox" TLA.thy [dmd_def] "(.~[]F) .= (<>.~F)"
   39.61 -   (fn _ => [ Auto_tac() ]);
   39.62 +   (fn _ => [ Auto_tac ]);
   39.63  
   39.64  qed_goalw "NotDmd" TLA.thy [dmd_def] "(.~<>F) .= ([].~F)"
   39.65 -   (fn _ => [ Auto_tac () ]);
   39.66 +   (fn _ => [ Auto_tac ]);
   39.67  
   39.68  (* These are not by default included in temp_css, because they could be harmful,
   39.69     e.g. []F .& .~[]F becomes []F .& <>.~F !! *)
   39.70 @@ -363,7 +363,7 @@
   39.71                rtac ccontr 1,
   39.72                subgoal_tac "sigma |= <>[][]F .& <>[].~[]F" 1,
   39.73                etac thin_rl 1,
   39.74 -              Auto_tac(),
   39.75 +              Auto_tac,
   39.76  	      etac (temp_conjimpE STL6) 1, atac 1,
   39.77  	      Asm_full_simp_tac 1,
   39.78  	      ALLGOALS (asm_full_simp_tac (simpset() addsimps more_temp_simps))
   39.79 @@ -382,18 +382,19 @@
   39.80     (fn _ => [ fast_tac (temp_cs addSEs [STL4E]) 1 ]);
   39.81  
   39.82  qed_goal "DBImplBD" TLA.thy "<>[](F::temporal) .-> []<>F"
   39.83 -  (fn _ => [Auto_tac(),
   39.84 +  (fn _ => [Auto_tac,
   39.85  	    rtac ccontr 1,
   39.86 -	    auto_tac (temp_css addsimps2 more_temp_simps addEs2 [temp_conjimpE STL6])
   39.87 +	    old_auto_tac (temp_css addsimps2 more_temp_simps 
   39.88 +			           addEs2 [temp_conjimpE STL6])
   39.89  	   ]);
   39.90  
   39.91  (* Although the script is the same, the derivation isn't polymorphic and doesn't
   39.92     work for other types of formulas (uses STL2).
   39.93  *)
   39.94  qed_goal "DBImplBDAct" TLA.thy "<>[](A::action) .-> []<>A"
   39.95 -  (fn _ => [Auto_tac(),
   39.96 +  (fn _ => [Auto_tac,
   39.97  	    rtac ccontr 1,
   39.98 -	    auto_tac (temp_css addsimps2 more_temp_simps addEs2 [temp_conjimpE STL6])
   39.99 +	    old_auto_tac (temp_css addsimps2 more_temp_simps addEs2 [temp_conjimpE STL6])
  39.100  	   ]);
  39.101  
  39.102  qed_goal "BoxDmdDmdBox" TLA.thy
  39.103 @@ -420,7 +421,7 @@
  39.104  
  39.105  (* Auxiliary lemma allows priming of boxed actions *)
  39.106  qed_goal "BoxPrime" TLA.thy "[]P .-> [](P .& P`)"
  39.107 -  (fn _ => [Auto_tac(),
  39.108 +  (fn _ => [Auto_tac,
  39.109  	    etac dup_boxE 1,
  39.110  	    auto_tac (temp_css addsimps2 [boxact_def]
  39.111  		               addSIs2 [STL2bD_pr] addSEs2 [STL4E])
  39.112 @@ -517,7 +518,7 @@
  39.113  	    ]);
  39.114  
  39.115  qed_goalw "DmdRec" TLA.thy [dmd_def] "(<>$P) .= (Init($P) .| (<>P$))"
  39.116 -   (fn _ => [Auto_tac(),
  39.117 +   (fn _ => [Auto_tac,
  39.118  	     etac notE 1,
  39.119  	     SELECT_GOAL (auto_tac (temp_css addsimps2 (stable_def::Init_simps)
  39.120  				             addIs2 [INV1I] addEs2 [STL4E])) 1,
  39.121 @@ -533,7 +534,7 @@
  39.122  
  39.123  (* The "=>" part of the following is a little intricate. *)
  39.124  qed_goal "InfinitePrime" TLA.thy "([]<>$P) .= ([]<>P$)"
  39.125 -   (fn _ => [Auto_tac(),
  39.126 +   (fn _ => [Auto_tac,
  39.127  	     rtac classical 1,
  39.128  	     rtac (temp_mp DBImplBDAct) 1,
  39.129  	     subgoal_tac "sigma |= <>[]$P" 1,
  39.130 @@ -592,7 +593,7 @@
  39.131  
  39.132  qed_goalw "streett_leadsto" TLA.thy [leadsto]
  39.133     "([]<>P .-> []<>Q) .= (<>(P ~> Q))"
  39.134 -   (fn _ => [Auto_tac(),
  39.135 +   (fn _ => [Auto_tac,
  39.136               asm_full_simp_tac (simpset() addsimps boxact_def::more_temp_simps) 1,
  39.137               SELECT_GOAL (auto_tac (temp_css addSEs2 [DmdImplE,STL4E] 
  39.138                                               addsimps2 Init_simps)) 1,
  39.139 @@ -725,26 +726,26 @@
  39.140  \      P .& N .-> $(Enabled(<A>_v)) |]   \
  39.141  \  ==> []N .& WF(A)_v .-> (P ~> Q)"
  39.142     (fn [prem1,prem2,prem3]
  39.143 -             => [auto_tac (temp_css addSDs2 [BoxWFI]),
  39.144 -		 etac STL4Edup 1, atac 1,
  39.145 -		 Auto_tac(),
  39.146 -		 subgoal_tac "sigmaa |= [](P .-> P` .| Q`)" 1,
  39.147 -		 auto_tac (temp_css addSDs2 [unless]),
  39.148 -		 etac (temp_conjimpE INV1) 1, atac 1,
  39.149 -		 merge_box_tac 1,
  39.150 -		 rtac STL2D 1,
  39.151 -		 rtac EnsuresInfinite 1, atac 2,
  39.152 -		 SELECT_GOAL (auto_tac (temp_css addsimps2 [WF_alt])) 1,
  39.153 -		 atac 2,
  39.154 -		 subgoal_tac "sigmaa |= [][]$(Enabled(<A>_v))" 1,
  39.155 -		 merge_box_tac 1,
  39.156 -		 SELECT_GOAL (auto_tac (temp_css addsimps2 [dmd_def])) 1,
  39.157 -		 SELECT_GOAL ((rewtac (temp_rewrite STL3)) THEN
  39.158 -			      (auto_tac (temp_css addSEs2 [STL4E] addSIs2 [action_mp prem3]))) 1,
  39.159 -		 fast_tac (action_cs addSIs [action_mp prem2]) 1,
  39.160 -		 fast_tac (temp_cs addIs [temp_mp DmdPrime]) 1,
  39.161 -		 fast_tac (temp_cs addSEs [STL4E] addSIs [action_mp prem1]) 1
  39.162 -		]);
  39.163 +	 => [auto_tac (temp_css addSDs2 [BoxWFI]),
  39.164 +	     etac STL4Edup 1, atac 1,
  39.165 +	     Auto_tac,
  39.166 +	     subgoal_tac "sigmaa |= [](P .-> P` .| Q`)" 1,
  39.167 +	     auto_tac (temp_css addSDs2 [unless]),
  39.168 +	     etac (temp_conjimpE INV1) 1, atac 1,
  39.169 +	     merge_box_tac 1,
  39.170 +	     rtac STL2D 1,
  39.171 +	     rtac EnsuresInfinite 1, atac 2,
  39.172 +	     SELECT_GOAL (old_auto_tac (temp_css addsimps2 [WF_alt])) 1,
  39.173 +	     atac 2,
  39.174 +	     subgoal_tac "sigmaa |= [][]$(Enabled(<A>_v))" 1,
  39.175 +	     merge_box_tac 1,
  39.176 +	     SELECT_GOAL (auto_tac (temp_css addsimps2 [dmd_def])) 1,
  39.177 +	     SELECT_GOAL ((rewtac (temp_rewrite STL3)) THEN
  39.178 +			  (auto_tac (temp_css addSEs2 [STL4E] addSIs2 [action_mp prem3]))) 1,
  39.179 +	     fast_tac (action_cs addSIs [action_mp prem2]) 1,
  39.180 +	     fast_tac (temp_cs addIs [temp_mp DmdPrime]) 1,
  39.181 +	     fast_tac (temp_cs addSEs [STL4E] addSIs [action_mp prem1]) 1
  39.182 +	    ]);
  39.183  
  39.184  (* Sometimes easier to use; designed for action B rather than state predicate Q *)
  39.185  qed_goalw "WF_leadsto" TLA.thy [leadsto]
  39.186 @@ -755,7 +756,7 @@
  39.187     (fn [prem1,prem2,prem3]
  39.188         => [auto_tac (temp_css addSDs2 [BoxWFI]),
  39.189             etac STL4Edup 1, atac 1,
  39.190 -           Auto_tac(),
  39.191 +           Auto_tac,
  39.192             subgoal_tac "sigmaa |= <><A>_v" 1,
  39.193             SELECT_GOAL (auto_tac (temp_css addSEs2 [DmdImpl2,STL4E] addSIs2 [action_mp prem2])) 1,
  39.194             rtac classical 1,
  39.195 @@ -779,14 +780,14 @@
  39.196  		 eres_inst_tac [("F","F")] dup_boxE 1,
  39.197  		 merge_temp_box_tac 1,
  39.198  		 etac STL4Edup 1, atac 1,
  39.199 -		 Auto_tac(),
  39.200 +		 Auto_tac,
  39.201  		 subgoal_tac "sigmaa |= [](P .-> P` .| Q`)" 1,
  39.202  		 auto_tac (temp_css addSDs2 [unless]),
  39.203  		 etac (temp_conjimpE INV1) 1, atac 1,
  39.204  		 merge_act_box_tac 1,
  39.205  		 rtac STL2D 1,
  39.206  		 rtac EnsuresInfinite 1, atac 2,
  39.207 -		 SELECT_GOAL (auto_tac (temp_css addsimps2 [SF_alt])) 1,
  39.208 +		 SELECT_GOAL (old_auto_tac (temp_css addsimps2 [SF_alt])) 1,
  39.209  		 atac 2,
  39.210  		 subgoal_tac "sigmaa |= []<>$(Enabled(<A>_v))" 1,
  39.211  		 SELECT_GOAL (auto_tac (temp_css addsimps2 [dmd_def])) 1,
  39.212 @@ -805,7 +806,7 @@
  39.213  \      [](N .& [.~B]_f) .& WF(A)_f .& []F .& <>[]($(Enabled(<M>_g))) .-> <>[]P |]   \
  39.214  \  ==> []N .& WF(A)_f .& []F .-> WF(M)_g"
  39.215     (fn [prem1,prem2,prem3,prem4]
  39.216 -       => [Auto_tac(),
  39.217 +       => [Auto_tac,
  39.218  	   case_tac "sigma |= <>[]$Enabled(<M>_g)" 1,
  39.219  	   SELECT_GOAL (auto_tac (temp_css addsimps2 [WF_def,dmd_def])) 2,
  39.220  	   case_tac "sigma |= <>[][.~B]_f" 1,
  39.221 @@ -819,7 +820,7 @@
  39.222  	   subgoal_tac "sigma |= <>([]N .& []P .& []<><A>_f)" 1,
  39.223  	   rtac ((temp_unlift DmdBoxDmd) RS iffD1) 1,
  39.224  	   eres_inst_tac [("F","[]N .& []P .& []<><A>_f")] DmdImplE 1,
  39.225 -	   SELECT_GOAL (Auto_tac()) 1,
  39.226 +	   SELECT_GOAL Auto_tac 1,
  39.227  	   dres_inst_tac [("P","P")] (temp_mp BoxPrime) 1,
  39.228  	   merge_act_box_tac 1,
  39.229  	   etac InfImpl 1, atac 1,
  39.230 @@ -827,7 +828,7 @@
  39.231  	   etac BoxDmd 1,
  39.232  	   dres_inst_tac [("F","<><A>_f"),("G","[]P")] BoxDmd 1, atac 1,
  39.233  	   eres_inst_tac [("F","[]<><A>_f .& []P")] DmdImplE 1,
  39.234 -	   SELECT_GOAL (Auto_tac ()) 1,
  39.235 +	   SELECT_GOAL Auto_tac 1,
  39.236  	   rtac (temp_mp (prem3 RS STL4 RS DmdImpl)) 1,
  39.237  	   fast_tac (temp_cs addIs [STL4E,DmdImplE]) 1,
  39.238  	   etac (temp_conjimpE STL6) 1, atac 1,
  39.239 @@ -857,7 +858,7 @@
  39.240  \      [](N .& [.~B]_f) .& SF(A)_f .& []F .& []<>($(Enabled(<M>_g))) .-> <>[]P |]   \
  39.241  \  ==> []N .& SF(A)_f .& []F .-> SF(M)_g"
  39.242     (fn [prem1,prem2,prem3,prem4]
  39.243 -       => [Auto_tac(),
  39.244 +       => [Auto_tac,
  39.245  	   case_tac "sigma |= []<>$Enabled(<M>_g)" 1,
  39.246  	   SELECT_GOAL (auto_tac (temp_css addsimps2 [SF_def,dmd_def])) 2,
  39.247  	   case_tac "sigma |= <>[][.~B]_f" 1,
  39.248 @@ -871,7 +872,7 @@
  39.249  	   subgoal_tac "sigma |= <>([]N .& []P .& []<><A>_f)" 1,
  39.250  	   rtac ((temp_unlift DmdBoxDmd) RS iffD1) 1,
  39.251  	   eres_inst_tac [("F","[]N .& []P .& []<><A>_f")] DmdImplE 1,
  39.252 -	   SELECT_GOAL (Auto_tac()) 1,
  39.253 +	   SELECT_GOAL Auto_tac 1,
  39.254  	   dres_inst_tac [("P","P")] (temp_mp BoxPrime) 1,
  39.255  	   merge_act_box_tac 1,
  39.256  	   etac InfImpl 1, atac 1,
  39.257 @@ -879,7 +880,7 @@
  39.258  	   etac BoxDmd 1,
  39.259  	   dres_inst_tac [("F","<><A>_f"),("G","[]P")] BoxDmd 1, atac 1,
  39.260  	   eres_inst_tac [("F","[]<><A>_f .& []P")] DmdImplE 1,
  39.261 -	   SELECT_GOAL (Auto_tac ()) 1,
  39.262 +	   SELECT_GOAL Auto_tac 1,
  39.263  	   rtac (temp_mp (prem3 RS DmdImpl RS STL4)) 1,
  39.264  	   fast_tac (temp_cs addEs [STL4E,DmdImplE]) 1,
  39.265  	   dtac BoxSFI 1,
  39.266 @@ -915,7 +916,7 @@
  39.267            subgoal_tac "sigma |= []((REX y. #((y,x):r) .& F y) .-> <>G)" 1,
  39.268  	  cut_facts_tac prems 1,
  39.269  	  etac STL4Edup 1, atac 1,
  39.270 -	  Auto_tac(), etac swap 1, atac 1,
  39.271 +	  Auto_tac, etac swap 1, atac 1,
  39.272  	  rtac dup_dmdD 1,
  39.273  	  etac DmdImpl2 1, atac 1,
  39.274  	  subgoal_tac "sigma |= [](RALL y. #((y,x):r) .& F y .-> <>G)" 1,
  39.275 @@ -943,7 +944,7 @@
  39.276  (* If r is well-founded, state function v cannot decrease forever *)
  39.277  qed_goal "wf_not_box_decrease" TLA.thy
  39.278    "!!r. wf r ==> [][ {[v$, $v]} .: #r ]_v .-> <>[][#False]_v"
  39.279 -  (fn _ => [Auto_tac(),
  39.280 +  (fn _ => [Auto_tac,
  39.281              subgoal_tac "ALL x. (sigma |= [](Init($v .= #x) .-> <>[][#False]_v))" 1,
  39.282              etac allE 1,
  39.283              dtac STL2D 1,
  39.284 @@ -968,7 +969,7 @@
  39.285              dres_inst_tac [("P", "$v .= #xa")] (temp_mp BoxPrime) 1,
  39.286              SELECT_GOAL (auto_tac (temp_css addEs2 [STL4E] addsimps2 [square_def])) 1,
  39.287              SELECT_GOAL (auto_tac (temp_css addSIs2 [INV1I] addsimps2 [Init_def])) 1,
  39.288 -            auto_tac (temp_css addsimps2 [square_def] addSIs2 [unless] addSEs2 [STL4E])
  39.289 +            old_auto_tac (temp_css addsimps2 [square_def] addSIs2 [unless] addSEs2 [STL4E])
  39.290             ]);
  39.291  
  39.292  (* "wf ?r  ==>  <>[][{[?v$, $?v]} .: #?r]_?v .-> <>[][#False]_?v" *)
  39.293 @@ -980,14 +981,14 @@
  39.294  *)
  39.295  qed_goal "wf_box_dmd_decrease" TLA.thy
  39.296    "wf r ==> []<>({[v$, $v]} .: #r) .-> []<><.~({[v$, $v]} .: #r)>_v"
  39.297 -  (fn [prem] => [Auto_tac(),
  39.298 +  (fn [prem] => [Auto_tac,
  39.299                   rtac ccontr 1,
  39.300                   asm_full_simp_tac 
  39.301                     (simpset() addsimps ([action_rewrite not_angle] @ more_temp_simps)) 1,
  39.302                   dtac (prem RS (temp_mp wf_not_dmd_box_decrease)) 1,
  39.303                   dtac BoxDmdDmdBox 1, atac 1,
  39.304                   subgoal_tac "sigma |= []<>((#False)::action)" 1,
  39.305 -                 SELECT_GOAL (Auto_tac()) 1,
  39.306 +                 SELECT_GOAL Auto_tac 1,
  39.307                   etac STL4E 1,
  39.308                   rtac DmdImpl 1,
  39.309                   auto_tac (action_css addsimps2 [square_def] addSEs2 [prem RS wf_irrefl])
  39.310 @@ -998,12 +999,12 @@
  39.311  *)
  39.312  qed_goal "nat_box_dmd_decrease" TLA.thy
  39.313    "!!n::nat stfun. []<>(n$ .< $n) .-> []<>($n .< n$)"
  39.314 -  (fn _ => [Auto_tac(),
  39.315 +  (fn _ => [Auto_tac,
  39.316              subgoal_tac "sigma |= []<><.~( {[n$,$n]} .: #less_than)>_n" 1,
  39.317              etac thin_rl 1, etac STL4E 1, rtac DmdImpl 1,
  39.318              SELECT_GOAL (auto_tac (claset(), simpset() addsimps [angle_def])) 1,
  39.319              rtac nat_less_cases 1,
  39.320 -            Auto_tac(),
  39.321 +            Auto_tac,
  39.322              rtac (temp_mp wf_box_dmd_decrease) 1,
  39.323              auto_tac (claset() addSEs [STL4E] addSIs [DmdImpl], simpset())
  39.324             ]);
    40.1 --- a/src/HOL/equalities.ML	Tue Dec 23 11:56:09 1997 +0100
    40.2 +++ b/src/HOL/equalities.ML	Wed Dec 24 10:02:30 1997 +0100
    40.3 @@ -603,7 +603,7 @@
    40.4  AddIffs [all_not_in_conv];
    40.5  
    40.6  goalw thy [Pow_def] "Pow {} = {{}}";
    40.7 -by (Auto_tac());
    40.8 +by Auto_tac;
    40.9  qed "Pow_empty";
   40.10  Addsimps [Pow_empty];
   40.11  
    41.1 --- a/src/HOL/ex/Recdef.ML	Tue Dec 23 11:56:09 1997 +0100
    41.2 +++ b/src/HOL/ex/Recdef.ML	Wed Dec 24 10:02:30 1997 +0100
    41.3 @@ -24,7 +24,7 @@
    41.4  
    41.5  goal thy "g x < Suc x";
    41.6  by (res_inst_tac [("u","x")] g.induct 1);
    41.7 -by (Auto_tac());
    41.8 +by Auto_tac;
    41.9  by (trans_tac 1);
   41.10  qed "g_terminates";
   41.11  
    42.1 --- a/src/HOL/simpdata.ML	Tue Dec 23 11:56:09 1997 +0100
    42.2 +++ b/src/HOL/simpdata.ML	Wed Dec 24 10:02:30 1997 +0100
    42.3 @@ -471,14 +471,24 @@
    42.4  fun op addcongs2 arg = pair_upd2 (op addcongs) arg;
    42.5  fun op delcongs2 arg = pair_upd2 (op delcongs) arg;
    42.6  
    42.7 -fun auto_tac (cs,ss) = 
    42.8 +fun mk_auto_tac (cs, ss) m n =
    42.9      let val cs' = cs addss ss 
   42.10 -    in  EVERY [TRY (safe_tac cs'),
   42.11 -	       REPEAT (FIRSTGOAL (fast_tac cs')),
   42.12 +	val bdt = Blast.depth_tac cs m;
   42.13 +	fun blast_depth_tac i thm = bdt i thm handle Blast.TRANS s => 
   42.14 +		(warning ("Blast_tac: " ^ s); Seq.empty);
   42.15 +        val maintac = 
   42.16 +          blast_depth_tac	   (*fast but can't use addss*)
   42.17 +          ORELSE'
   42.18 +          depth_tac cs' n;         (*slower but general*)
   42.19 +    in  EVERY [ALLGOALS (asm_full_simp_tac ss),
   42.20 +	       TRY (safe_tac cs'),
   42.21 +	       REPEAT (FIRSTGOAL maintac),
   42.22                 TRY (safe_tac (cs addSss ss)),
   42.23  	       prune_params_tac] 
   42.24      end;
   42.25  
   42.26 -fun Auto_tac () = auto_tac (claset(), simpset());
   42.27 +fun auto_tac (cs,ss) = mk_auto_tac (cs,ss) 4 2;
   42.28  
   42.29 -fun auto () = by (Auto_tac ());
   42.30 +fun Auto_tac st = auto_tac (claset(), simpset()) st;
   42.31 +
   42.32 +fun auto () = by Auto_tac;
    43.1 --- a/src/HOLCF/Fix.ML	Tue Dec 23 11:56:09 1997 +0100
    43.2 +++ b/src/HOLCF/Fix.ML	Wed Dec 24 10:02:30 1997 +0100
    43.3 @@ -414,7 +414,7 @@
    43.4  	(cut_facts_tac prems 1),
    43.5  	(rtac trans 1),
    43.6  	(stac unfold 1),
    43.7 -	(Auto_tac ())
    43.8 +	Auto_tac
    43.9  	]);
   43.10  
   43.11  (* ------------------------------------------------------------------------ *)
    44.1 --- a/src/HOLCF/IOA/ABP/Correctness.ML	Tue Dec 23 11:56:09 1997 +0100
    44.2 +++ b/src/HOLCF/IOA/ABP/Correctness.ML	Wed Dec 24 10:02:30 1997 +0100
    44.3 @@ -159,7 +159,7 @@
    44.4  by (simp_tac (simpset() addsimps [and_de_morgan_and_absorbe]) 2);
    44.5  by (Step_tac 1);
    44.6  by (ALLGOALS (cut_inst_tac [("l","xs")] cons_not_nil));
    44.7 -by (Auto_tac());
    44.8 +by (Auto_tac);
    44.9  val reduce_tl =result();
   44.10  
   44.11  
    45.1 --- a/src/HOLCF/IOA/meta_theory/Automata.ML	Tue Dec 23 11:56:09 1997 +0100
    45.2 +++ b/src/HOLCF/IOA/meta_theory/Automata.ML	Wed Dec 24 10:02:30 1997 +0100
    45.3 @@ -112,7 +112,7 @@
    45.4  
    45.5  goal thy"compatible A B = compatible B A";
    45.6  by (asm_full_simp_tac (simpset() addsimps [compatible_def,Int_commute]) 1);
    45.7 -by (Auto_tac());
    45.8 +by Auto_tac;
    45.9  qed"compat_commute";
   45.10  
   45.11  goalw thy [externals_def,actions_def,compatible_def]
   45.12 @@ -289,7 +289,7 @@
   45.13  by (simp_tac (simpset() addsimps [actions_def,asig_internals_def,
   45.14          asig_outputs_def,asig_inputs_def,externals_def,asig_of_def,restrict_def,
   45.15          restrict_asig_def]) 1);
   45.16 -by (Auto_tac());
   45.17 +by Auto_tac;
   45.18  qed"acts_restrict";
   45.19  
   45.20  goal thy "starts_of(restrict ioa acts) = starts_of(ioa) &     \
   45.21 @@ -414,10 +414,11 @@
   45.22  
   45.23  goalw thy [is_trans_of_def,restrict_def,restrict_asig_def] 
   45.24  "!!A. is_trans_of A ==> is_trans_of (rename A f)";
   45.25 -by (asm_full_simp_tac (simpset() addsimps [actions_def,trans_of_def,
   45.26 -    asig_internals_def,asig_outputs_def,asig_inputs_def,externals_def,
   45.27 -   asig_of_def,rename_def,rename_set_def]) 1);
   45.28 -by (Auto_tac());
   45.29 +by (asm_full_simp_tac
   45.30 +    (simpset() addsimps [actions_def,trans_of_def, asig_internals_def,
   45.31 +			 asig_outputs_def,asig_inputs_def,externals_def,
   45.32 +			 asig_of_def,rename_def,rename_set_def]) 1);
   45.33 +by (Blast_tac 1);
   45.34  qed"is_trans_of_rename";
   45.35  
   45.36  goal thy "!! A. [| is_asig_of A; is_asig_of B; compatible A B|]  \
   45.37 @@ -426,7 +427,7 @@
   45.38         asig_comp_def,compatible_def,asig_internals_def,asig_outputs_def,
   45.39       asig_inputs_def,actions_def,is_asig_def]) 1);
   45.40  by (asm_full_simp_tac (simpset() addsimps [asig_of_def]) 1);
   45.41 -by (Auto_tac());
   45.42 +by Auto_tac;
   45.43  by (REPEAT (best_tac (set_cs addEs [equalityCE]) 1));
   45.44  qed"is_asig_of_par";
   45.45  
   45.46 @@ -434,7 +435,7 @@
   45.47             asig_internals_def,asig_outputs_def,asig_inputs_def,externals_def,o_def] 
   45.48  "!! A. is_asig_of A ==> is_asig_of (restrict A f)";
   45.49  by (Asm_full_simp_tac 1);
   45.50 -by (Auto_tac());
   45.51 +by Auto_tac;
   45.52  by (REPEAT (best_tac (set_cs addEs [equalityCE]) 1));
   45.53  qed"is_asig_of_restrict";
   45.54  
   45.55 @@ -442,7 +443,7 @@
   45.56  by (asm_full_simp_tac (simpset() addsimps [is_asig_of_def,
   45.57       rename_def,rename_set_def,asig_internals_def,asig_outputs_def,
   45.58       asig_inputs_def,actions_def,is_asig_def,asig_of_def]) 1);
   45.59 -by (Auto_tac()); 
   45.60 +by Auto_tac; 
   45.61  by (dres_inst_tac [("s","Some xb")] sym 1);
   45.62  by (rotate_tac ~1 1);
   45.63  by (Asm_full_simp_tac 1);
   45.64 @@ -466,7 +467,7 @@
   45.65  "!! A. [|compatible A B; compatible A C |]==> compatible A (B||C)";
   45.66  by (asm_full_simp_tac (simpset() addsimps [internals_of_par, 
   45.67     outputs_of_par,actions_of_par]) 1);
   45.68 -by (Auto_tac());
   45.69 +by Auto_tac;
   45.70  by (REPEAT (best_tac (set_cs addEs [equalityCE]) 1));
   45.71  qed"compatible_par";
   45.72  
   45.73 @@ -475,7 +476,7 @@
   45.74  "!! A. [|compatible A C; compatible B C |]==> compatible (A||B) C";
   45.75  by (asm_full_simp_tac (simpset() addsimps [internals_of_par, 
   45.76     outputs_of_par,actions_of_par]) 1);
   45.77 -by (Auto_tac());
   45.78 +by Auto_tac;
   45.79  by (REPEAT (best_tac (set_cs addEs [equalityCE]) 1));
   45.80  qed"compatible_par2";
   45.81  
    46.1 --- a/src/HOLCF/IOA/meta_theory/CompoScheds.ML	Tue Dec 23 11:56:09 1997 +0100
    46.2 +++ b/src/HOLCF/IOA/meta_theory/CompoScheds.ML	Wed Dec 24 10:02:30 1997 +0100
    46.3 @@ -115,7 +115,7 @@
    46.4  by (simp_tac (simpset() addsimps [mkex_def] 
    46.5                         setloop (split_tac [expand_if]) ) 1);
    46.6  by (cut_inst_tac [("exA","a>>exA")] mkex2_cons_1 1);
    46.7 -by (Auto_tac());
    46.8 +by Auto_tac;
    46.9  qed"mkex_cons_1";
   46.10  
   46.11  goal thy "!!x.[| x~:act A; x:act B |] \
   46.12 @@ -124,7 +124,7 @@
   46.13  by (simp_tac (simpset() addsimps [mkex_def] 
   46.14                         setloop (split_tac [expand_if]) ) 1);
   46.15  by (cut_inst_tac [("exB","b>>exB")] mkex2_cons_2 1);
   46.16 -by (Auto_tac());
   46.17 +by Auto_tac;
   46.18  qed"mkex_cons_2";
   46.19  
   46.20  goal thy "!!x.[| x:act A; x:act B |]  \
   46.21 @@ -133,7 +133,7 @@
   46.22  by (simp_tac (simpset() addsimps [mkex_def] 
   46.23                         setloop (split_tac [expand_if]) ) 1);
   46.24  by (cut_inst_tac [("exB","b>>exB"),("exA","a>>exA")] mkex2_cons_3 1);
   46.25 -by (Auto_tac());
   46.26 +by Auto_tac;
   46.27  qed"mkex_cons_3";
   46.28  
   46.29  Delsimps [mkex2_UU,mkex2_nil,mkex2_cons_1,mkex2_cons_2,mkex2_cons_3];
   46.30 @@ -364,7 +364,7 @@
   46.31  by (Seq_induct_tac "x" [] 1);
   46.32  by (Seq_case_simp_tac "y" 2);
   46.33  by (pair_tac "a" 1);
   46.34 -by (Auto_tac());
   46.35 +by Auto_tac;
   46.36  
   46.37  *)
   46.38  
    47.1 --- a/src/HOLCF/IOA/meta_theory/CompoTraces.ML	Tue Dec 23 11:56:09 1997 +0100
    47.2 +++ b/src/HOLCF/IOA/meta_theory/CompoTraces.ML	Wed Dec 24 10:02:30 1997 +0100
    47.3 @@ -170,7 +170,7 @@
    47.4  by (rtac (Forall_Conc_impl RS mp) 1);
    47.5  by (asm_full_simp_tac (simpset() addsimps [ForallPTakewhileQ,intA_is_not_actB,int_is_act]) 1);
    47.6  (* a~:A,a~:B *)
    47.7 -by (Auto_tac());
    47.8 +by Auto_tac;
    47.9  qed"ForallAorB_mksch1";
   47.10  
   47.11  bind_thm ("ForallAorB_mksch",ForallAorB_mksch1 RS spec RS spec RS mp);
   47.12 @@ -395,12 +395,12 @@
   47.13  \                             y = z @@ mksch A B`tr`a`b\
   47.14  \                             --> Finite tr";
   47.15  by (etac Seq_Finite_ind  1);
   47.16 -by (Auto_tac());
   47.17 +by Auto_tac;
   47.18  by (Seq_case_simp_tac "tr" 1);
   47.19  (* tr = UU *)
   47.20  by (asm_full_simp_tac (simpset() addsimps [nil_is_Conc]) 1);
   47.21  (* tr = nil *)
   47.22 -by (Auto_tac());
   47.23 +by Auto_tac;
   47.24  (* tr = Conc *)
   47.25  ren "s ss" 1;
   47.26  
   47.27 @@ -419,7 +419,7 @@
   47.28  by (Seq_case_simp_tac "tr" 1);
   47.29  (* tr = UU *)
   47.30  by (asm_full_simp_tac (simpset() addsimps [Conc_Conc_eq]) 1);
   47.31 -by (Auto_tac());
   47.32 +by Auto_tac;
   47.33  (* tr = nil ok *)
   47.34  (* tr = Conc *)
   47.35  by (Seq_case_simp_tac "z" 1);
   47.36 @@ -452,19 +452,19 @@
   47.37  
   47.38  goal thy "(x>>xs = y @@ z) = ((y=nil & x>>xs=z) | (? ys. y=x>>ys & xs=ys@@z))";
   47.39  by (Seq_case_simp_tac "y" 1);
   47.40 -by (Auto_tac());
   47.41 +by Auto_tac;
   47.42  qed"Conc_Conc_eq";
   47.43  
   47.44  goal thy "!! (y::'a Seq).Finite y ==> ~ y= x@@UU";
   47.45  by (etac Seq_Finite_ind 1);
   47.46  by (Seq_case_simp_tac "x" 1);
   47.47  by (Seq_case_simp_tac "x" 1);
   47.48 -by (Auto_tac());
   47.49 +by Auto_tac;
   47.50  qed"FiniteConcUU1";
   47.51  
   47.52  goal thy "~ Finite ((x::'a Seq)@@UU)";
   47.53  by (rtac (FiniteConcUU1 COMP rev_contrapos) 1);
   47.54 -by (Auto_tac());
   47.55 +by Auto_tac;
   47.56  qed"FiniteConcUU";
   47.57  
   47.58  finiteR_mksch
    48.1 --- a/src/HOLCF/IOA/meta_theory/Compositionality.ML	Tue Dec 23 11:56:09 1997 +0100
    48.2 +++ b/src/HOLCF/IOA/meta_theory/Compositionality.ML	Wed Dec 24 10:02:30 1997 +0100
    48.3 @@ -9,7 +9,7 @@
    48.4  
    48.5  
    48.6  goal thy "!! A. [|eA --> A ; eB & ~eA --> ~A|] ==> (eA | eB) --> A=eA";
    48.7 -by (Auto_tac());
    48.8 +by Auto_tac;
    48.9  qed"compatibility_consequence3";
   48.10  
   48.11  
   48.12 @@ -29,7 +29,7 @@
   48.13      or even better A||B= B||A, FIX *)
   48.14  
   48.15  goal thy "!! A. [|eA --> A ; eB & ~eA --> ~A|] ==> (eB | eA) --> A=eA";
   48.16 -by (Auto_tac());
   48.17 +by Auto_tac;
   48.18  qed"compatibility_consequence4";
   48.19  
   48.20  goal thy 
    49.1 --- a/src/HOLCF/IOA/meta_theory/RefMappings.ML	Tue Dec 23 11:56:09 1997 +0100
    49.2 +++ b/src/HOLCF/IOA/meta_theory/RefMappings.ML	Wed Dec 24 10:02:30 1997 +0100
    49.3 @@ -136,7 +136,7 @@
    49.4  by (rtac impI 1);
    49.5  by (etac conjE 1);
    49.6  by (forward_tac  [reachable_rename] 1);
    49.7 -by (Auto_tac());
    49.8 +by Auto_tac;
    49.9  qed"rename_through_pmap";
   49.10  
   49.11  
    50.1 --- a/src/HOLCF/IOA/meta_theory/Seq.ML	Tue Dec 23 11:56:09 1997 +0100
    50.2 +++ b/src/HOLCF/IOA/meta_theory/Seq.ML	Wed Dec 24 10:02:30 1997 +0100
    50.3 @@ -320,7 +320,7 @@
    50.4   "!!x. [|x~=UU;y~=UU|]==> (x##xs=y##ys) = (x=y & xs=ys)";
    50.5  by (rtac iffI 1);
    50.6  by (etac (hd seq.injects) 1);
    50.7 -by (Auto_tac());
    50.8 +by Auto_tac;
    50.9  qed"scons_inject_eq";
   50.10  
   50.11  goal thy "!!x. nil<<x ==> nil=x";
    51.1 --- a/src/HOLCF/IOA/meta_theory/Sequence.ML	Tue Dec 23 11:56:09 1997 +0100
    51.2 +++ b/src/HOLCF/IOA/meta_theory/Sequence.ML	Wed Dec 24 10:02:30 1997 +0100
    51.3 @@ -432,7 +432,7 @@
    51.4  by (etac (FiniteConc_2 RS spec RS spec RS mp) 1);
    51.5  by (rtac refl 1);
    51.6  by (rtac (FiniteConc_1 RS mp) 1);
    51.7 -by (Auto_tac());
    51.8 +by Auto_tac;
    51.9  qed"FiniteConc";
   51.10  
   51.11  Addsimps [FiniteConc];
   51.12 @@ -448,13 +448,13 @@
   51.13  by (Seq_case_simp_tac "t" 1);
   51.14  by (Asm_full_simp_tac 1);
   51.15  (* main case *)
   51.16 -by (Auto_tac());
   51.17 +by Auto_tac;
   51.18  by (Seq_case_simp_tac "t" 1);
   51.19  by (Asm_full_simp_tac 1);
   51.20  qed"FiniteMap2";
   51.21  
   51.22  goal thy "Finite (Map f`s) = Finite s";
   51.23 -by (Auto_tac());
   51.24 +by Auto_tac;
   51.25  by (etac (FiniteMap2 RS spec RS mp) 1);
   51.26  by (rtac refl 1);
   51.27  by (etac FiniteMap1 1);
   51.28 @@ -482,9 +482,9 @@
   51.29  by (etac conjE 1);
   51.30  by (etac nil_less_is_nil 1);
   51.31  (* main case *)
   51.32 -by (Auto_tac());
   51.33 +by Auto_tac;
   51.34  by (Seq_case_simp_tac "y" 1);
   51.35 -by (Auto_tac());
   51.36 +by Auto_tac;
   51.37  qed_spec_mp"Finite_flat";
   51.38  
   51.39  
   51.40 @@ -499,7 +499,7 @@
   51.41  by (eres_inst_tac [("x","j")] allE 1);
   51.42  by (cut_inst_tac [("x","Y 0"),("y","Y j")] Finite_flat 1);
   51.43  (* Generates a contradiction in subgoal 3 *)
   51.44 -by (Auto_tac());
   51.45 +by Auto_tac;
   51.46  qed"adm_Finite";
   51.47  
   51.48  Addsimps [adm_Finite];
   51.49 @@ -530,12 +530,12 @@
   51.50  (* FIX: should be same as nil_is_Conc2 when all nils are turned to right side !! *)
   51.51  goal thy "(nil = x @@ y) = ((x::'a Seq)= nil & y = nil)";
   51.52  by (Seq_case_simp_tac "x" 1);
   51.53 -by (Auto_tac());
   51.54 +by Auto_tac;
   51.55  qed"nil_is_Conc";
   51.56  
   51.57  goal thy "(x @@ y = nil) = ((x::'a Seq)= nil & y = nil)";
   51.58  by (Seq_case_simp_tac "x" 1);
   51.59 -by (Auto_tac());
   51.60 +by Auto_tac;
   51.61  qed"nil_is_Conc2";
   51.62  
   51.63  
   51.64 @@ -642,14 +642,14 @@
   51.65  by (strip_tac 1); 
   51.66  by (Seq_case_simp_tac "sa" 1);
   51.67  by (Asm_full_simp_tac 1);
   51.68 -by (Auto_tac());
   51.69 +by Auto_tac;
   51.70  qed"Forall_prefix";
   51.71   
   51.72  bind_thm ("Forall_prefixclosed",Forall_prefix RS spec RS mp RS mp);
   51.73  
   51.74  
   51.75  goal thy "!! h. [| Finite h; Forall P s; s= h @@ t |] ==> Forall P t";
   51.76 -by (Auto_tac());
   51.77 +by Auto_tac;
   51.78  qed"Forall_postfixclosed";
   51.79  
   51.80  
   51.81 @@ -728,7 +728,7 @@
   51.82  \                (Forall (%x. ~P x) ys  & ~Finite ys)";
   51.83  by (rtac conjI 1);
   51.84  by (cut_inst_tac [] (FilterUU_nFinite_lemma2 RS mp COMP rev_contrapos) 1);
   51.85 -by (Auto_tac());
   51.86 +by Auto_tac;
   51.87  by (blast_tac (claset() addSDs [FilterUU_nFinite_lemma1]) 1);
   51.88  qed"FilternPUUForallP";
   51.89  
   51.90 @@ -737,14 +737,14 @@
   51.91  \   ==> Filter P`ys = nil";
   51.92  by (etac ForallnPFilterPnil 1);
   51.93  by (etac ForallPForallQ 1);
   51.94 -by (Auto_tac());
   51.95 +by Auto_tac;
   51.96  qed"ForallQFilterPnil";
   51.97  
   51.98  goal thy "!! Q P. [| ~Finite ys; Forall Q ys;  !!x. Q x ==> ~P x|] \
   51.99  \   ==> Filter P`ys = UU ";
  51.100  by (etac ForallnPFilterPUU 1);
  51.101  by (etac ForallPForallQ 1);
  51.102 -by (Auto_tac());
  51.103 +by Auto_tac;
  51.104  qed"ForallQFilterPUU";
  51.105  
  51.106  
  51.107 @@ -762,7 +762,7 @@
  51.108  goal thy"!! P. [| !!x. Q x==> P x |] ==> Forall P (Takewhile Q`x)";
  51.109  by (rtac ForallPForallQ 1);
  51.110  by (rtac ForallPTakewhileP 1);
  51.111 -by (Auto_tac());
  51.112 +by Auto_tac;
  51.113  qed"ForallPTakewhileQ";
  51.114  
  51.115  
  51.116 @@ -771,7 +771,7 @@
  51.117  by (etac ForallnPFilterPnil 1);
  51.118  by (rtac ForallPForallQ 1);
  51.119  by (rtac ForallPTakewhileP 1);
  51.120 -by (Auto_tac());
  51.121 +by Auto_tac;
  51.122  qed"FilterPTakewhileQnil";
  51.123  
  51.124  goal thy "!! Q P. [| !!x. Q x ==> P x |] ==> \
  51.125 @@ -779,7 +779,7 @@
  51.126  by (rtac ForallPFilterPid 1);
  51.127  by (rtac ForallPForallQ 1);
  51.128  by (rtac ForallPTakewhileP 1);
  51.129 -by (Auto_tac());
  51.130 +by Auto_tac;
  51.131  qed"FilterPTakewhileQid";
  51.132  
  51.133  Addsimps [ForallPTakewhileP,ForallPTakewhileQ,
  51.134 @@ -864,14 +864,15 @@
  51.135  by (safe_tac set_cs);
  51.136  by (res_inst_tac [("x","x")] exI 1);
  51.137  by (cut_inst_tac [("P1","%x. ~ P x")] (divide_Seq_lemma RS mp) 1);
  51.138 -by (Auto_tac());
  51.139 +by Auto_tac;
  51.140  qed"divide_Seq2";
  51.141  
  51.142  
  51.143  goal thy  "!! y. ~Forall P y \
  51.144  \  ==> ? x bs rs. y= (bs @@ (x>>rs)) & Finite bs & Forall P bs & (~ P x)";
  51.145  by (cut_inst_tac [] divide_Seq2 1);
  51.146 -by (Auto_tac());
  51.147 +(*Auto_tac no longer proves it*)
  51.148 +by (REPEAT (fast_tac (claset() addss (simpset())) 1));
  51.149  qed"divide_Seq3";
  51.150  
  51.151  Addsimps [FilterPQ,FilterConc,Conc_cong];
  51.152 @@ -885,7 +886,7 @@
  51.153  goal thy "(!n. seq_take n`x = seq_take n`x') = (x = x')";
  51.154  by (rtac iffI 1);
  51.155  by (resolve_tac seq.take_lemmas 1);
  51.156 -by (Auto_tac());
  51.157 +by Auto_tac;
  51.158  qed"seq_take_lemma";
  51.159  
  51.160  goal thy 
  51.161 @@ -894,9 +895,9 @@
  51.162  by (Seq_induct_tac "x" [] 1);
  51.163  by (strip_tac 1);
  51.164  by (res_inst_tac [("n","n")] natE 1);
  51.165 -by (Auto_tac());
  51.166 +by Auto_tac;
  51.167  by (res_inst_tac [("n","n")] natE 1);
  51.168 -by (Auto_tac());
  51.169 +by Auto_tac;
  51.170  qed"take_reduction1";
  51.171  
  51.172  
  51.173 @@ -916,9 +917,9 @@
  51.174  by (Seq_induct_tac "x" [] 1);
  51.175  by (strip_tac 1);
  51.176  by (res_inst_tac [("n","n")] natE 1);
  51.177 -by (Auto_tac());
  51.178 +by Auto_tac;
  51.179  by (res_inst_tac [("n","n")] natE 1);
  51.180 -by (Auto_tac());
  51.181 +by Auto_tac;
  51.182  qed"take_reduction_less1";
  51.183  
  51.184  
  51.185 @@ -949,7 +950,7 @@
  51.186  goal thy "(!n. seq_take n`x << seq_take n`x') = (x << x')";
  51.187  by (rtac iffI 1);
  51.188  by (rtac take_lemma_less1 1);
  51.189 -by (Auto_tac());
  51.190 +by Auto_tac;
  51.191  by (etac monofun_cfun_arg 1);
  51.192  qed"take_lemma_less";
  51.193  
  51.194 @@ -973,7 +974,7 @@
  51.195  by (case_tac "Forall Q x" 1);
  51.196  by (auto_tac (claset() addSDs [divide_Seq3],simpset()));
  51.197  by (resolve_tac seq.take_lemmas 1);
  51.198 -by (Auto_tac());
  51.199 +by Auto_tac;
  51.200  qed"take_lemma_principle2";
  51.201  
  51.202  
  51.203 @@ -1190,8 +1191,9 @@
  51.204  
  51.205  
  51.206  goal thy "Map f`(x@@y) = (Map f`x) @@ (Map f`y)";
  51.207 -by (res_inst_tac [("A1","%x. True"),("x1","x")] (take_lemma_in_eq_out RS mp) 1);
  51.208 -by (Auto_tac());
  51.209 +by (res_inst_tac [("A1","%x. True"), ("x1","x")]
  51.210 +    (take_lemma_in_eq_out RS mp) 1);
  51.211 +by Auto_tac;
  51.212  qed"MapConc_takelemma";
  51.213  
  51.214  
    52.1 --- a/src/HOLCF/IOA/meta_theory/ShortExecutions.ML	Tue Dec 23 11:56:09 1997 +0100
    52.2 +++ b/src/HOLCF/IOA/meta_theory/ShortExecutions.ML	Wed Dec 24 10:02:30 1997 +0100
    52.3 @@ -106,7 +106,7 @@
    52.4               ForallQFilterPUU]) 1);
    52.5  (* main case *)
    52.6  by (asm_full_simp_tac (simpset() addsimps [Cut_Cons,ForallQFilterPnil]) 1);
    52.7 -by (Auto_tac());
    52.8 +by Auto_tac;
    52.9  qed"FilterCut";
   52.10  
   52.11  
   52.12 @@ -124,7 +124,7 @@
   52.13  (* main case *)
   52.14  by (asm_full_simp_tac (simpset() addsimps [Cut_Cons,ForallQFilterPnil]) 1);
   52.15  by (rtac take_reduction 1);
   52.16 -by (Auto_tac());
   52.17 +by Auto_tac;
   52.18  qed"Cut_idemp";
   52.19  
   52.20  
   52.21 @@ -148,7 +148,7 @@
   52.22  by (asm_full_simp_tac (simpset() addsimps [Cut_Cons,MapConc,
   52.23            ForallMap,FiniteMap1,o_def]) 1);
   52.24  by (rtac take_reduction 1);
   52.25 -by (Auto_tac());
   52.26 +by Auto_tac;
   52.27  qed"MapCut";
   52.28  
   52.29  
   52.30 @@ -174,7 +174,7 @@
   52.31  by (asm_full_simp_tac (simpset() addsimps [Cut_Cons]) 1);
   52.32  by (rtac take_reduction_less 1);
   52.33  (* auto makes also reasoning about Finiteness of parts of s ! *)
   52.34 -by (Auto_tac());
   52.35 +by Auto_tac;
   52.36  qed_spec_mp"Cut_prefixcl_nFinite";
   52.37  
   52.38  
    53.1 --- a/src/HOLCF/IOA/meta_theory/Traces.ML	Tue Dec 23 11:56:09 1997 +0100
    53.2 +++ b/src/HOLCF/IOA/meta_theory/Traces.ML	Wed Dec 24 10:02:30 1997 +0100
    53.3 @@ -179,7 +179,7 @@
    53.4  by (asm_full_simp_tac (simpset() addsimps [executions_def]) 1);
    53.5  by (pair_tac "x" 1);
    53.6  by (rtac (execfrag_in_sig RS spec RS mp) 1);
    53.7 -by (Auto_tac());
    53.8 +by Auto_tac;
    53.9  qed"exec_in_sig";
   53.10  
   53.11  goalw thy [schedules_def,has_schedule_def]
   53.12 @@ -213,7 +213,7 @@
   53.13  by (strip_tac 1);
   53.14  by (Seq_case_simp_tac "xa" 1);
   53.15  by (pair_tac "a" 1);
   53.16 -by (Auto_tac());
   53.17 +by Auto_tac;
   53.18  qed"execfrag_prefixclosed";
   53.19  
   53.20  bind_thm ("exec_prefixclosed",conjI RS (execfrag_prefixclosed RS spec RS spec RS mp));
   53.21 @@ -226,6 +226,6 @@
   53.22  by (strip_tac 1);
   53.23  by (Seq_case_simp_tac "s" 1);
   53.24  by (pair_tac "a" 1);
   53.25 -by (Auto_tac());
   53.26 +by Auto_tac;
   53.27  qed_spec_mp"exec_prefix2closed";
   53.28  
    54.1 --- a/src/HOLCF/Lift.ML	Tue Dec 23 11:56:09 1997 +0100
    54.2 +++ b/src/HOLCF/Lift.ML	Wed Dec 24 10:02:30 1997 +0100
    54.3 @@ -40,7 +40,7 @@
    54.4  back();
    54.5  by (safe_tac set_cs);
    54.6  by (rtac cont_flift1_not_arg 1);
    54.7 -by (Auto_tac());
    54.8 +by Auto_tac;
    54.9  by (rtac cont_flift1_arg 1);
   54.10  qed"cont_flift1_arg_and_not_arg";
   54.11  
    55.1 --- a/src/HOLCF/Lift3.ML	Tue Dec 23 11:56:09 1997 +0100
    55.2 +++ b/src/HOLCF/Lift3.ML	Wed Dec 24 10:02:30 1997 +0100
    55.3 @@ -148,7 +148,7 @@
    55.4  goal thy "!!f.[|cont g; cont f|] ==> cont(%x. ((f x)`(g x)) s)";
    55.5  by (rtac cont2cont_CF1L 1);
    55.6  by (REPEAT (resolve_tac cont_lemmas1 1));
    55.7 -by (Auto_tac());
    55.8 +by Auto_tac;
    55.9  qed"cont_fapp_app";
   55.10  
   55.11  goal thy "!!f.[|cont g; cont f|] ==> cont(%x. ((f x)`(g x)) s t)";
    56.1 --- a/src/HOLCF/Tr.ML	Tue Dec 23 11:56:09 1997 +0100
    56.2 +++ b/src/HOLCF/Tr.ML	Wed Dec 24 10:02:30 1997 +0100
    56.3 @@ -115,17 +115,17 @@
    56.4  "!!t.[|t~=UU|]==> ((t andalso s)=FF)=(t=FF | s=FF)";
    56.5  by (rtac iffI 1);
    56.6  by (res_inst_tac [("p","t")] trE 1);
    56.7 -by (Auto_tac());
    56.8 +by Auto_tac;
    56.9  by (res_inst_tac [("p","t")] trE 1);
   56.10 -by (Auto_tac());
   56.11 +by Auto_tac;
   56.12  qed"andalso_or";
   56.13  
   56.14  goal thy "!!t.[|t~=UU|]==> ((t andalso s)~=FF)=(t~=FF & s~=FF)";
   56.15  by (rtac iffI 1);
   56.16  by (res_inst_tac [("p","t")] trE 1);
   56.17 -by (Auto_tac());
   56.18 +by Auto_tac;
   56.19  by (res_inst_tac [("p","t")] trE 1);
   56.20 -by (Auto_tac());
   56.21 +by Auto_tac;
   56.22  qed"andalso_and";
   56.23  
   56.24  goal thy "(Def x ~=FF)= x";
    57.1 --- a/src/ZF/CardinalArith.ML	Tue Dec 23 11:56:09 1997 +0100
    57.2 +++ b/src/ZF/CardinalArith.ML	Wed Dec 24 10:02:30 1997 +0100
    57.3 @@ -806,7 +806,7 @@
    57.4  goal CardinalArith.thy "!!m n. [| m:nat; n:nat |] ==> m + n eqpoll m #+ n";
    57.5  by (rtac eqpoll_trans 1);
    57.6  by (resolve_tac [well_ord_radd RS well_ord_cardinal_eqpoll RS eqpoll_sym] 1);
    57.7 -by (REPEAT (eresolve_tac [nat_implies_well_ord] 1));
    57.8 +by (REPEAT (etac nat_implies_well_ord 1));
    57.9  by (asm_simp_tac (simpset() 
   57.10  		  addsimps [nat_cadd_eq_add RS sym, cadd_def, eqpoll_refl]) 1);
   57.11  qed "nat_sum_eqpoll_sum";
    58.1 --- a/src/ZF/Coind/MT.ML	Tue Dec 23 11:56:09 1997 +0100
    58.2 +++ b/src/ZF/Coind/MT.ML	Wed Dec 24 10:02:30 1997 +0100
    58.3 @@ -79,7 +79,7 @@
    58.4  by (excluded_middle_tac "f=y" 1);
    58.5  by (rtac UnI1 2);
    58.6  by (rtac UnI2 1);
    58.7 -by (Auto_tac());
    58.8 +by Auto_tac;
    58.9  qed "consistency_fix";
   58.10  
   58.11  
    59.1 --- a/src/ZF/Perm.ML	Tue Dec 23 11:56:09 1997 +0100
    59.2 +++ b/src/ZF/Perm.ML	Wed Dec 24 10:02:30 1997 +0100
    59.3 @@ -431,7 +431,7 @@
    59.4  by (Asm_full_simp_tac 1);
    59.5  by (rtac fun_extension 1);
    59.6  by (REPEAT (ares_tac [comp_fun, lam_type] 1));
    59.7 -by (Auto_tac());
    59.8 +by Auto_tac;
    59.9  qed "comp_eq_id_iff";
   59.10  
   59.11  goalw Perm.thy [bij_def]
    60.1 --- a/src/ZF/QPair.ML	Tue Dec 23 11:56:09 1997 +0100
    60.2 +++ b/src/ZF/QPair.ML	Wed Dec 24 10:02:30 1997 +0100
    60.3 @@ -110,14 +110,14 @@
    60.4  
    60.5  qed_goal "qfst_type" thy
    60.6      "!!p. p:QSigma(A,B) ==> qfst(p) : A"
    60.7 - (fn _=> [ Auto_tac() ]);
    60.8 + (fn _=> [ Auto_tac ]);
    60.9  
   60.10  qed_goal "qsnd_type" thy
   60.11      "!!p. p:QSigma(A,B) ==> qsnd(p) : B(qfst(p))"
   60.12 - (fn _=> [ Auto_tac() ]);
   60.13 + (fn _=> [ Auto_tac ]);
   60.14  
   60.15  goal thy "!!a A B. a: QSigma(A,B) ==> <qfst(a); qsnd(a)> = a";
   60.16 -by (Auto_tac());
   60.17 +by Auto_tac;
   60.18  qed "QPair_qfst_qsnd_eq";
   60.19  
   60.20  
   60.21 @@ -142,7 +142,7 @@
   60.22  goalw thy [qsplit_def]
   60.23    "!!u. u: A<*>B ==>   \
   60.24  \       R(qsplit(c,u)) <-> (ALL x:A. ALL y:B. u = <x;y> --> R(c(x,y)))";
   60.25 -by (Auto_tac());
   60.26 +by Auto_tac;
   60.27  qed "expand_qsplit";
   60.28  
   60.29  
    61.1 --- a/src/ZF/Sum.ML	Tue Dec 23 11:56:09 1997 +0100
    61.2 +++ b/src/ZF/Sum.ML	Wed Dec 24 10:02:30 1997 +0100
    61.3 @@ -156,7 +156,7 @@
    61.4  \       R(case(c,d,u)) <-> \
    61.5  \       ((ALL x:A. u = Inl(x) --> R(c(x))) & \
    61.6  \       (ALL y:B. u = Inr(y) --> R(d(y))))";
    61.7 -by (Auto_tac());
    61.8 +by Auto_tac;
    61.9  qed "expand_case";
   61.10  
   61.11  val major::prems = goal Sum.thy
   61.12 @@ -172,7 +172,7 @@
   61.13    "!!z. z: A+B ==>   \
   61.14  \       case(c, d, case(%x. Inl(c'(x)), %y. Inr(d'(y)), z)) = \
   61.15  \       case(%x. c(c'(x)), %y. d(d'(y)), z)";
   61.16 -by (Auto_tac());
   61.17 +by Auto_tac;
   61.18  qed "case_case";
   61.19  
   61.20  
    62.1 --- a/src/ZF/ex/Limit.ML	Tue Dec 23 11:56:09 1997 +0100
    62.2 +++ b/src/ZF/ex/Limit.ML	Wed Dec 24 10:02:30 1997 +0100
    62.3 @@ -49,8 +49,8 @@
    62.4  val [po,xy,yz,x,y,z] = goalw Limit.thy [po_def]
    62.5      "[|po(D); rel(D,x,y); rel(D,y,z); x:set(D);  \
    62.6  \      y:set(D); z:set(D)|] ==> rel(D,x,z)";
    62.7 -br (po RS conjunct2 RS conjunct1 RS bspec RS bspec 
    62.8 -   RS bspec RS mp RS mp) 1;
    62.9 +by (rtac (po RS conjunct2 RS conjunct1 RS bspec RS bspec 
   62.10 +   RS bspec RS mp RS mp) 1);
   62.11  by (rtac x 1); 
   62.12  by (rtac y 1);
   62.13  by (rtac z 1);
   62.14 @@ -126,8 +126,8 @@
   62.15  
   62.16  val prems = goal Limit.thy
   62.17      "[|islub(D,X,x); n:nat|] ==> rel(D,X`n,x)";
   62.18 -br (rewrite_rule[islub_def,isub_def](hd prems) RS conjunct1 
   62.19 -   RS conjunct2 RS bspec) 1;
   62.20 +by (rtac (rewrite_rule[islub_def,isub_def](hd prems) RS conjunct1 
   62.21 +   RS conjunct2 RS bspec) 1);
   62.22  by (resolve_tac prems 1);
   62.23  qed "islub_ub";
   62.24  
    63.1 --- a/src/ZF/ex/misc.ML	Tue Dec 23 11:56:09 1997 +0100
    63.2 +++ b/src/ZF/ex/misc.ML	Wed Dec 24 10:02:30 1997 +0100
    63.3 @@ -155,7 +155,8 @@
    63.4  \    : bij(Pow(A+B), Pow(A)*Pow(B))";
    63.5  by (res_inst_tac [("d", "%<X,Y>.{Inl(x).x:X} Un {Inr(y).y:Y}")] 
    63.6      lam_bijective 1);
    63.7 -by (Auto_tac());
    63.8 -val Pow_bij = result();
    63.9 +(*Auto_tac no longer proves it*)
   63.10 +by (REPEAT (fast_tac (claset() addss (simpset())) 1));
   63.11 +qed "Pow_bij";
   63.12  
   63.13  writeln"Reached end of file.";
    64.1 --- a/src/ZF/pair.ML	Tue Dec 23 11:56:09 1997 +0100
    64.2 +++ b/src/ZF/pair.ML	Wed Dec 24 10:02:30 1997 +0100
    64.3 @@ -118,14 +118,14 @@
    64.4  Addsimps [fst_conv,snd_conv];
    64.5  
    64.6  qed_goal "fst_type" ZF.thy "!!p. p:Sigma(A,B) ==> fst(p) : A"
    64.7 - (fn _=> [ Auto_tac() ]);
    64.8 + (fn _=> [ Auto_tac ]);
    64.9  
   64.10  qed_goal "snd_type" ZF.thy "!!p. p:Sigma(A,B) ==> snd(p) : B(fst(p))"
   64.11 - (fn _=> [ Auto_tac() ]);
   64.12 + (fn _=> [ Auto_tac ]);
   64.13  
   64.14  qed_goal "Pair_fst_snd_eq" ZF.thy
   64.15      "!!a A B. a: Sigma(A,B) ==> <fst(a),snd(a)> = a"
   64.16 - (fn _=> [ Auto_tac() ]);
   64.17 + (fn _=> [ Auto_tac ]);
   64.18  
   64.19  
   64.20  (*** Eliminator - split ***)
   64.21 @@ -148,7 +148,7 @@
   64.22  goalw ZF.thy [split_def]
   64.23    "!!u. u: A*B ==>   \
   64.24  \       R(split(c,u)) <-> (ALL x:A. ALL y:B. u = <x,y> --> R(c(x,y)))";
   64.25 -by (Auto_tac());
   64.26 +by Auto_tac;
   64.27  qed "expand_split";
   64.28  
   64.29