Calls Blast_tac
authorpaulson
Fri Apr 04 11:18:52 1997 +0200 (1997-04-04)
changeset 2891d8f254ad1ab9
parent 2890 f27002fc531d
child 2892 67fb21ddfe15
Calls Blast_tac
src/HOL/Auth/Message.ML
src/HOL/Auth/OtwayRees_AN.ML
src/HOL/Auth/Shared.ML
src/HOL/Lambda/Eta.ML
src/HOL/Lambda/Lambda.ML
src/HOL/Lambda/ParRed.ML
src/HOL/List.ML
src/HOL/NatDef.ML
src/HOL/Relation.ML
src/HOL/Set.ML
src/HOL/Sum.ML
src/HOL/Trancl.ML
src/HOL/Univ.ML
src/HOL/equalities.ML
src/HOL/ex/Mutil.ML
src/HOL/ex/cla.ML
     1.1 --- a/src/HOL/Auth/Message.ML	Fri Apr 04 11:18:19 1997 +0200
     1.2 +++ b/src/HOL/Auth/Message.ML	Fri Apr 04 11:18:52 1997 +0200
     1.3 @@ -37,20 +37,20 @@
     1.4  (**** keysFor operator ****)
     1.5  
     1.6  goalw thy [keysFor_def] "keysFor {} = {}";
     1.7 -by (Fast_tac 1);
     1.8 +by (Blast_tac 1);
     1.9  qed "keysFor_empty";
    1.10  
    1.11  goalw thy [keysFor_def] "keysFor (H Un H') = keysFor H Un keysFor H'";
    1.12 -by (Fast_tac 1);
    1.13 +by (Blast_tac 1);
    1.14  qed "keysFor_Un";
    1.15  
    1.16  goalw thy [keysFor_def] "keysFor (UN i. H i) = (UN i. keysFor (H i))";
    1.17 -by (Fast_tac 1);
    1.18 +by (Blast_tac 1);
    1.19  qed "keysFor_UN";
    1.20  
    1.21  (*Monotonicity*)
    1.22  goalw thy [keysFor_def] "!!G H. G<=H ==> keysFor(G) <= keysFor(H)";
    1.23 -by (Fast_tac 1);
    1.24 +by (Blast_tac 1);
    1.25  qed "keysFor_mono";
    1.26  
    1.27  goalw thy [keysFor_def] "keysFor (insert (Agent A) H) = keysFor H";
    1.28 @@ -83,7 +83,7 @@
    1.29            keysFor_insert_Hash, keysFor_insert_MPair, keysFor_insert_Crypt];
    1.30  
    1.31  goalw thy [keysFor_def] "!!H. Crypt K X : H ==> invKey K : keysFor H";
    1.32 -by (Fast_tac 1);
    1.33 +by (Blast_tac 1);
    1.34  qed "Crypt_imp_invKey_keysFor";
    1.35  
    1.36  
    1.37 @@ -108,7 +108,7 @@
    1.38       proofs concern only atomic messages.*)
    1.39  
    1.40  goal thy "H <= parts(H)";
    1.41 -by (Fast_tac 1);
    1.42 +by (Blast_tac 1);
    1.43  qed "parts_increasing";
    1.44  
    1.45  (*Monotonicity*)
    1.46 @@ -122,7 +122,7 @@
    1.47  goal thy "parts{} = {}";
    1.48  by (Step_tac 1);
    1.49  by (etac parts.induct 1);
    1.50 -by (ALLGOALS Fast_tac);
    1.51 +by (ALLGOALS Blast_tac);
    1.52  qed "parts_empty";
    1.53  Addsimps [parts_empty];
    1.54  
    1.55 @@ -134,7 +134,7 @@
    1.56  (*WARNING: loops if H = {Y}, therefore must not be repeated!*)
    1.57  goal thy "!!H. X: parts H ==> EX Y:H. X: parts {Y}";
    1.58  by (etac parts.induct 1);
    1.59 -by (ALLGOALS Fast_tac);
    1.60 +by (ALLGOALS Blast_tac);
    1.61  qed "parts_singleton";
    1.62  
    1.63  
    1.64 @@ -147,7 +147,7 @@
    1.65  goal thy "parts(G Un H) <= parts(G) Un parts(H)";
    1.66  by (rtac subsetI 1);
    1.67  by (etac parts.induct 1);
    1.68 -by (ALLGOALS Fast_tac);
    1.69 +by (ALLGOALS Blast_tac);
    1.70  val parts_Un_subset2 = result();
    1.71  
    1.72  goal thy "parts(G Un H) = parts(G) Un parts(H)";
    1.73 @@ -173,7 +173,7 @@
    1.74  goal thy "parts(UN x:A. H x) <= (UN x:A. parts(H x))";
    1.75  by (rtac subsetI 1);
    1.76  by (etac parts.induct 1);
    1.77 -by (ALLGOALS Fast_tac);
    1.78 +by (ALLGOALS Blast_tac);
    1.79  val parts_UN_subset2 = result();
    1.80  
    1.81  goal thy "parts(UN x:A. H x) = (UN x:A. parts(H x))";
    1.82 @@ -195,18 +195,18 @@
    1.83  
    1.84  goal thy "!!H. X: parts (parts H) ==> X: parts H";
    1.85  by (etac parts.induct 1);
    1.86 -by (ALLGOALS Fast_tac);
    1.87 +by (ALLGOALS Blast_tac);
    1.88  qed "parts_partsE";
    1.89 -AddSEs [parts_partsE];
    1.90 +AddSDs [parts_partsE];
    1.91  
    1.92  goal thy "parts (parts H) = parts H";
    1.93 -by (Fast_tac 1);
    1.94 +by (Blast_tac 1);
    1.95  qed "parts_idem";
    1.96  Addsimps [parts_idem];
    1.97  
    1.98  goal thy "!!H. [| X: parts G;  G <= parts H |] ==> X: parts H";
    1.99  by (dtac parts_mono 1);
   1.100 -by (Fast_tac 1);
   1.101 +by (Blast_tac 1);
   1.102  qed "parts_trans";
   1.103  
   1.104  (*Cut*)
   1.105 @@ -299,13 +299,13 @@
   1.106  Addsimps [analz.Inj];
   1.107  
   1.108  goal thy "H <= analz(H)";
   1.109 -by (Fast_tac 1);
   1.110 +by (Blast_tac 1);
   1.111  qed "analz_increasing";
   1.112  
   1.113  goal thy "analz H <= parts H";
   1.114  by (rtac subsetI 1);
   1.115  by (etac analz.induct 1);
   1.116 -by (ALLGOALS Fast_tac);
   1.117 +by (ALLGOALS Blast_tac);
   1.118  qed "analz_subset_parts";
   1.119  
   1.120  bind_thm ("not_parts_not_analz", analz_subset_parts RS contra_subsetD);
   1.121 @@ -315,7 +315,7 @@
   1.122  by (rtac equalityI 1);
   1.123  by (rtac (analz_subset_parts RS parts_mono RS subset_trans) 1);
   1.124  by (Simp_tac 1);
   1.125 -by (fast_tac (!claset addDs [analz_increasing RS parts_mono RS subsetD]) 1);
   1.126 +by (blast_tac (!claset addIs [analz_increasing RS parts_mono RS subsetD]) 1);
   1.127  qed "parts_analz";
   1.128  Addsimps [parts_analz];
   1.129  
   1.130 @@ -339,7 +339,7 @@
   1.131  goal thy "analz{} = {}";
   1.132  by (Step_tac 1);
   1.133  by (etac analz.induct 1);
   1.134 -by (ALLGOALS Fast_tac);
   1.135 +by (ALLGOALS Blast_tac);
   1.136  qed "analz_empty";
   1.137  Addsimps [analz_empty];
   1.138  
   1.139 @@ -386,8 +386,7 @@
   1.140  by (etac analz.induct 1);
   1.141  by (Auto_tac());
   1.142  by (etac analz.induct 1);
   1.143 -by (ALLGOALS
   1.144 -    (deepen_tac (!claset addIs [analz.Fst, analz.Snd, analz.Decrypt]) 0));
   1.145 +by (ALLGOALS (deepen_tac (!claset addIs [analz.Fst, analz.Snd]) 0));
   1.146  qed "analz_insert_MPair";
   1.147  
   1.148  (*Can pull out enCrypted message if the Key is not known*)
   1.149 @@ -459,24 +458,24 @@
   1.150  
   1.151  goal thy "!!H. X: analz (analz H) ==> X: analz H";
   1.152  by (etac analz.induct 1);
   1.153 -by (ALLGOALS Fast_tac);
   1.154 +by (ALLGOALS Blast_tac);
   1.155  qed "analz_analzE";
   1.156 -AddSEs [analz_analzE];
   1.157 +AddSDs [analz_analzE];
   1.158  
   1.159  goal thy "analz (analz H) = analz H";
   1.160 -by (Fast_tac 1);
   1.161 +by (Blast_tac 1);
   1.162  qed "analz_idem";
   1.163  Addsimps [analz_idem];
   1.164  
   1.165  goal thy "!!H. [| X: analz G;  G <= analz H |] ==> X: analz H";
   1.166  by (dtac analz_mono 1);
   1.167 -by (Fast_tac 1);
   1.168 +by (Blast_tac 1);
   1.169  qed "analz_trans";
   1.170  
   1.171  (*Cut; Lemma 2 of Lowe*)
   1.172  goal thy "!!H. [| Y: analz (insert X H);  X: analz H |] ==> Y: analz H";
   1.173  by (etac analz_trans 1);
   1.174 -by (Fast_tac 1);
   1.175 +by (Blast_tac 1);
   1.176  qed "analz_cut";
   1.177  
   1.178  (*Cut can be proved easily by induction on
   1.179 @@ -510,7 +509,7 @@
   1.180  \         analz H = H";
   1.181  by (Step_tac 1);
   1.182  by (etac analz.induct 1);
   1.183 -by (ALLGOALS Fast_tac);
   1.184 +by (ALLGOALS Blast_tac);
   1.185  qed "analz_trivial";
   1.186  
   1.187  (*Helps to prove Fake cases*)
   1.188 @@ -544,7 +543,7 @@
   1.189  AddSEs [Nonce_synth, Key_synth, Hash_synth, MPair_synth, Crypt_synth];
   1.190  
   1.191  goal thy "H <= synth(H)";
   1.192 -by (Fast_tac 1);
   1.193 +by (Blast_tac 1);
   1.194  qed "synth_increasing";
   1.195  
   1.196  (*Monotonicity*)
   1.197 @@ -569,39 +568,39 @@
   1.198  
   1.199  goal thy "!!H. X: synth (synth H) ==> X: synth H";
   1.200  by (etac synth.induct 1);
   1.201 -by (ALLGOALS Fast_tac);
   1.202 +by (ALLGOALS Blast_tac);
   1.203  qed "synth_synthE";
   1.204 -AddSEs [synth_synthE];
   1.205 +AddSDs [synth_synthE];
   1.206  
   1.207  goal thy "synth (synth H) = synth H";
   1.208 -by (Fast_tac 1);
   1.209 +by (Blast_tac 1);
   1.210  qed "synth_idem";
   1.211  
   1.212  goal thy "!!H. [| X: synth G;  G <= synth H |] ==> X: synth H";
   1.213  by (dtac synth_mono 1);
   1.214 -by (Fast_tac 1);
   1.215 +by (Blast_tac 1);
   1.216  qed "synth_trans";
   1.217  
   1.218  (*Cut; Lemma 2 of Lowe*)
   1.219  goal thy "!!H. [| Y: synth (insert X H);  X: synth H |] ==> Y: synth H";
   1.220  by (etac synth_trans 1);
   1.221 -by (Fast_tac 1);
   1.222 +by (Blast_tac 1);
   1.223  qed "synth_cut";
   1.224  
   1.225  goal thy "Agent A : synth H";
   1.226 -by (Fast_tac 1);
   1.227 +by (Blast_tac 1);
   1.228  qed "Agent_synth";
   1.229  
   1.230  goal thy "(Nonce N : synth H) = (Nonce N : H)";
   1.231 -by (Fast_tac 1);
   1.232 +by (Blast_tac 1);
   1.233  qed "Nonce_synth_eq";
   1.234  
   1.235  goal thy "(Key K : synth H) = (Key K : H)";
   1.236 -by (Fast_tac 1);
   1.237 +by (Blast_tac 1);
   1.238  qed "Key_synth_eq";
   1.239  
   1.240  goal thy "!!K. Key K ~: H ==> (Crypt K X : synth H) = (Crypt K X : H)";
   1.241 -by (Fast_tac 1);
   1.242 +by (Blast_tac 1);
   1.243  qed "Crypt_synth_eq";
   1.244  
   1.245  Addsimps [Agent_synth, Nonce_synth_eq, Key_synth_eq, Crypt_synth_eq];
   1.246 @@ -609,7 +608,7 @@
   1.247  
   1.248  goalw thy [keysFor_def]
   1.249      "keysFor (synth H) = keysFor H Un invKey``{K. Key K : H}";
   1.250 -by (Fast_tac 1);
   1.251 +by (Blast_tac 1);
   1.252  qed "keysFor_synth";
   1.253  Addsimps [keysFor_synth];
   1.254  
   1.255 @@ -655,11 +654,10 @@
   1.256  by (best_tac
   1.257      (!claset addEs [impOfSubs synth_increasing,
   1.258                      impOfSubs analz_mono]) 5);
   1.259 -by (Best_tac 1);
   1.260 -by (deepen_tac (!claset addIs [analz.Fst]) 0 1);
   1.261 -by (deepen_tac (!claset addIs [analz.Snd]) 0 1);
   1.262 -by (deepen_tac (!claset addSEs [analz.Decrypt]
   1.263 -                        addIs  [analz.Decrypt]) 0 1);
   1.264 +by (Blast_tac 1);
   1.265 +by (blast_tac (!claset addIs [analz.Inj RS analz.Fst]) 1);
   1.266 +by (blast_tac (!claset addIs [analz.Inj RS analz.Snd]) 1);
   1.267 +by (blast_tac (!claset addIs [analz.Decrypt]) 1);
   1.268  qed "analz_UN1_synth";
   1.269  Addsimps [analz_UN1_synth];
   1.270  
   1.271 @@ -668,7 +666,7 @@
   1.272  
   1.273  goal thy "!!Y. X: G ==> parts(insert X H) <= parts G Un parts H";
   1.274  by (rtac ([parts_mono, parts_Un_subset2] MRS subset_trans) 1);
   1.275 -by (Fast_tac 1);
   1.276 +by (Blast_tac 1);
   1.277  qed "parts_insert_subset_Un";
   1.278  
   1.279  (*More specifically for Fake*)
   1.280 @@ -676,7 +674,7 @@
   1.281  \              parts (insert X H) <= synth (analz G) Un parts G Un parts H";
   1.282  by (dtac parts_insert_subset_Un 1);
   1.283  by (Full_simp_tac 1);
   1.284 -by (Deepen_tac 0 1);
   1.285 +by (Blast_tac 1);
   1.286  qed "Fake_parts_insert";
   1.287  
   1.288  goal thy
   1.289 @@ -696,15 +694,15 @@
   1.290  by (best_tac (!claset addIs [impOfSubs (analz_mono RS synth_mono)]
   1.291                        addSEs [impOfSubs analz_mono]) 2);
   1.292  by (Full_simp_tac 1);
   1.293 -by (Fast_tac 1);
   1.294 +by (Blast_tac 1);
   1.295  qed "Fake_analz_insert";
   1.296  
   1.297  goal thy "(X: analz H & X: parts H) = (X: analz H)";
   1.298 -by (fast_tac (!claset addDs [impOfSubs analz_subset_parts]) 1);
   1.299 +by (blast_tac (!claset addIs [impOfSubs analz_subset_parts]) 1);
   1.300  val analz_conj_parts = result();
   1.301  
   1.302  goal thy "(X: analz H | X: parts H) = (X: parts H)";
   1.303 -by (fast_tac (!claset addDs [impOfSubs analz_subset_parts]) 1);
   1.304 +by (blast_tac (!claset addIs [impOfSubs analz_subset_parts]) 1);
   1.305  val analz_disj_parts = result();
   1.306  
   1.307  AddIffs [analz_conj_parts, analz_disj_parts];
   1.308 @@ -713,20 +711,20 @@
   1.309    redundant cases*)
   1.310  goal thy "({|X,Y|} : synth (analz H)) = \
   1.311  \         (X : synth (analz H) & Y : synth (analz H))";
   1.312 -by (Fast_tac 1);
   1.313 +by (Blast_tac 1);
   1.314  qed "MPair_synth_analz";
   1.315  
   1.316  AddIffs [MPair_synth_analz];
   1.317  
   1.318  goal thy "!!K. [| Key K : analz H;  Key (invKey K) : analz H |] \
   1.319  \              ==> (Crypt K X : synth (analz H)) = (X : synth (analz H))";
   1.320 -by (Fast_tac 1);
   1.321 +by (Blast_tac 1);
   1.322  qed "Crypt_synth_analz";
   1.323  
   1.324  
   1.325  goal thy "!!K. X ~: synth (analz H) \
   1.326  \   ==> (Hash{|X,Y|} : synth (analz H)) = (Hash{|X,Y|} : analz H)";
   1.327 -by (Fast_tac 1);
   1.328 +by (Blast_tac 1);
   1.329  qed "Hash_synth_analz";
   1.330  Addsimps [Hash_synth_analz];
   1.331  
   1.332 @@ -798,7 +796,7 @@
   1.333  \   ==> (Hash[X] Y : synth (analz H)) = \
   1.334  \       (Hash {|X, Y|} : analz H & Y : synth (analz H))";
   1.335  by (Simp_tac 1);
   1.336 -by (Fast_tac 1);
   1.337 +by (Blast_tac 1);
   1.338  qed "HPair_synth_analz";
   1.339  
   1.340  Addsimps [keysFor_insert_HPair, parts_insert_HPair, analz_insert_HPair, 
   1.341 @@ -866,6 +864,6 @@
   1.342  
   1.343  (*Needed occasionally with spy_analz_tac, e.g. in analz_insert_Key_newK*)
   1.344  goal Set.thy "A Un (B Un A) = B Un A";
   1.345 -by (Fast_tac 1);
   1.346 +by (Blast_tac 1);
   1.347  val Un_absorb3 = result();
   1.348  Addsimps [Un_absorb3];
     2.1 --- a/src/HOL/Auth/OtwayRees_AN.ML	Fri Apr 04 11:18:19 1997 +0200
     2.2 +++ b/src/HOL/Auth/OtwayRees_AN.ML	Fri Apr 04 11:18:52 1997 +0200
     2.3 @@ -311,7 +311,7 @@
     2.4  \           A ~: lost;  B ~: lost;  evs : otway lost |]             \
     2.5  \        ==> Key K ~: analz (sees lost Spy evs)";
     2.6  by (forward_tac [Says_Server_message_form] 1 THEN assume_tac 1);
     2.7 -by (fast_tac (!claset addSEs [lemma]) 1);
     2.8 +by (blast_tac (!claset addSEs [lemma]) 1);
     2.9  qed "Spy_not_see_encrypted_key";
    2.10  
    2.11  
    2.12 @@ -327,7 +327,7 @@
    2.13  by (rtac (subset_insertI RS sees_mono RS analz_mono RS contra_subsetD) 1);
    2.14  by (rtac (sees_lost_agent_subset_sees_Spy RS analz_mono RS contra_subsetD) 1);
    2.15  by (FIRSTGOAL (rtac Spy_not_see_encrypted_key));
    2.16 -by (REPEAT_FIRST (fast_tac (!claset addIs [otway_mono RS subsetD])));
    2.17 +by (REPEAT_FIRST (blast_tac (!claset addIs [otway_mono RS subsetD])));
    2.18  qed "Agent_not_see_encrypted_key";
    2.19  
    2.20  
     3.1 --- a/src/HOL/Auth/Shared.ML	Fri Apr 04 11:18:19 1997 +0200
     3.2 +++ b/src/HOL/Auth/Shared.ML	Fri Apr 04 11:18:52 1997 +0200
     3.3 @@ -125,12 +125,12 @@
     3.4  
     3.5  goal thy "sees lost A (Says A' B X # evs) <= insert X (sees lost A evs)";
     3.6  by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
     3.7 -by (Fast_tac 1);
     3.8 +by (Blast_tac 1);
     3.9  qed "sees_Says_subset_insert";
    3.10  
    3.11  goal thy "sees lost A evs <= sees lost A (Says A' B X # evs)";
    3.12  by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
    3.13 -by (Fast_tac 1);
    3.14 +by (Blast_tac 1);
    3.15  qed "sees_subset_sees_Says";
    3.16  
    3.17  (*Pushing Unions into parts.  One of the agents A is B, and thus sees Y.
    3.18 @@ -141,7 +141,7 @@
    3.19  by (etac rev_mp 1);     (*split_tac does not work on assumptions*)
    3.20  by (ALLGOALS
    3.21      (fast_tac (!claset unsafe_addss (!simpset addsimps [parts_Un, sees_Cons] 
    3.22 -                       setloop split_tac [expand_if]))));
    3.23 +				            setloop split_tac [expand_if]))));
    3.24  qed "UN_parts_sees_Says";
    3.25  
    3.26  goal thy "Says A B X : set_of_list evs --> X : sees lost Spy evs";
    3.27 @@ -179,12 +179,12 @@
    3.28  \          (EX A B. Says A B X : set_of_list evs) | (EX A. X = Key (shrK A))";
    3.29  by (list.induct_tac "evs" 1);
    3.30  by (ALLGOALS Asm_simp_tac);
    3.31 -by (fast_tac (!claset addDs [impOfSubs initState_subset]) 1);
    3.32 +by (blast_tac (!claset addDs [impOfSubs initState_subset]) 1);
    3.33  by (rtac conjI 1);
    3.34 -by (Fast_tac 2);
    3.35 +by (Blast_tac 2);
    3.36  by (event.induct_tac "a" 1);
    3.37  by (ALLGOALS (asm_simp_tac (!simpset addsimps [mem_if])));
    3.38 -by (ALLGOALS Fast_tac);
    3.39 +by (ALLGOALS Blast_tac);
    3.40  qed_spec_mp "seesD";
    3.41  
    3.42  Addsimps [sees_own, sees_Server, sees_Friend, sees_Spy];
    3.43 @@ -202,7 +202,7 @@
    3.44  
    3.45  goalw thy [used_def] "!!X. X: parts (sees lost B evs) ==> X: used evs";
    3.46  by (etac (impOfSubs parts_mono) 1);
    3.47 -by (Fast_tac 1);
    3.48 +by (Blast_tac 1);
    3.49  qed "usedI";
    3.50  
    3.51  AddIs [usedI];
    3.52 @@ -222,7 +222,7 @@
    3.53  
    3.54  (*A session key cannot clash with a long-term shared key*)
    3.55  goal thy "!!K. K ~: range shrK ==> shrK B ~= K";
    3.56 -by (Fast_tac 1);
    3.57 +by (Blast_tac 1);
    3.58  qed "shrK_neq";
    3.59  
    3.60  Addsimps [Key_not_used, shrK_neq, shrK_neq RS not_sym];
    3.61 @@ -264,7 +264,7 @@
    3.62  by (Step_tac 1);
    3.63  (*MPair case*)
    3.64  by (res_inst_tac [("x","Na+Nb")] exI 2);
    3.65 -by (fast_tac (!claset addSEs [add_leE]) 2);
    3.66 +by (blast_tac (!claset addSEs [add_leE]) 2);
    3.67  (*Nonce case*)
    3.68  by (res_inst_tac [("x","N + Suc nat")] exI 1);
    3.69  by (fast_tac (!claset addSEs [add_leE] addaltern trans_tac) 1);
    3.70 @@ -272,7 +272,7 @@
    3.71  
    3.72  goal thy "EX N. Nonce N ~: used evs";
    3.73  by (rtac (lemma RS exE) 1);
    3.74 -by (Fast_tac 1);
    3.75 +by (Blast_tac 1);
    3.76  qed "Nonce_supply1";
    3.77  
    3.78  goal thy "EX N N'. Nonce N ~: used evs & Nonce N' ~: used evs' & N ~= N'";
    3.79 @@ -307,14 +307,14 @@
    3.80  goal thy "Nonce (@ N. Nonce N ~: used evs) ~: used evs";
    3.81  by (rtac (lemma RS exE) 1);
    3.82  by (rtac selectI 1);
    3.83 -by (Fast_tac 1);
    3.84 +by (Blast_tac 1);
    3.85  qed "Nonce_supply";
    3.86  
    3.87  (*** Supply fresh keys for possibility theorems. ***)
    3.88  
    3.89  goal thy "EX K. Key K ~: used evs";
    3.90  by (rtac (Fin.emptyI RS Key_supply_ax RS exE) 1);
    3.91 -by (Fast_tac 1);
    3.92 +by (Blast_tac 1);
    3.93  qed "Key_supply1";
    3.94  
    3.95  val Fin_UNIV_insertI = UNIV_I RS Fin.insertI;
    3.96 @@ -344,7 +344,7 @@
    3.97  goal thy "Key (@ K. Key K ~: used evs) ~: used evs";
    3.98  by (rtac (Fin.emptyI RS Key_supply_ax RS exE) 1);
    3.99  by (rtac selectI 1);
   3.100 -by (Fast_tac 1);
   3.101 +by (Blast_tac 1);
   3.102  qed "Key_supply";
   3.103  
   3.104  (*** Tactics for possibility theorems ***)
   3.105 @@ -400,28 +400,23 @@
   3.106  val pushKey_newK = insComm thy "Key (newK ?evs)"  "Key (shrK ?C)";
   3.107  
   3.108  goal thy "!!A. A <= Compl (range shrK) ==> shrK x ~: A";
   3.109 -by (Fast_tac 1);
   3.110 +by (Blast_tac 1);
   3.111  qed "subset_Compl_range";
   3.112  
   3.113 -goal thy "insert (Key (f x)) (Key``(f``E) Un C) = \
   3.114 -\         Key `` (f `` (insert x E)) Un C";
   3.115 -by (Fast_tac 1);
   3.116 -qed "insert_Key_image";
   3.117 -
   3.118  goal thy "insert (Key K) H = Key `` {K} Un H";
   3.119 -by (Fast_tac 1);
   3.120 +by (Blast_tac 1);
   3.121  qed "insert_Key_singleton";
   3.122  
   3.123  goal thy "insert (Key K) (Key``KK Un C) = Key `` (insert K KK) Un C";
   3.124 -by (Fast_tac 1);
   3.125 -qed "insert_Key_image'";
   3.126 +by (Blast_tac 1);
   3.127 +qed "insert_Key_image";
   3.128  
   3.129  val analz_image_freshK_ss = 
   3.130       !simpset delsimps [image_insert, image_Un]
   3.131                addsimps ([image_insert RS sym, image_Un RS sym,
   3.132                           Key_not_used, 
   3.133                           insert_Key_singleton, subset_Compl_range,
   3.134 -                         insert_Key_image', Un_assoc RS sym]
   3.135 +                         insert_Key_image, Un_assoc RS sym]
   3.136                          @disj_comms)
   3.137                setloop split_tac [expand_if];
   3.138  
     4.1 --- a/src/HOL/Lambda/Eta.ML	Fri Apr 04 11:18:19 1997 +0200
     4.2 +++ b/src/HOL/Lambda/Eta.ML	Fri Apr 04 11:18:52 1997 +0200
     4.3 @@ -27,8 +27,8 @@
     4.4  goal Eta.thy "!i t u. ~free s i --> s[t/i] = s[u/i]";
     4.5  by (dB.induct_tac "s" 1);
     4.6  by (ALLGOALS(simp_tac (addsplit (!simpset))));
     4.7 -by (fast_tac HOL_cs 1);
     4.8 -by (fast_tac HOL_cs 1);
     4.9 +by (Blast_tac 1);
    4.10 +by (Blast_tac 1);
    4.11  qed_spec_mp "subst_not_free";
    4.12  Addsimps [subst_not_free RS eqTrueI];
    4.13  
    4.14 @@ -36,7 +36,7 @@
    4.15  \                   (i < k & free t i | k < i & free t (pred i))";
    4.16  by (dB.induct_tac "t" 1);
    4.17  by (ALLGOALS(asm_full_simp_tac (addsplit (!simpset) addcongs [conj_cong])));
    4.18 -by (fast_tac HOL_cs 2);
    4.19 +by (Blast_tac 2);
    4.20  by(simp_tac (!simpset addsimps [pred_def]
    4.21                        setloop (split_tac [expand_nat_case])) 1);
    4.22  by (safe_tac HOL_cs);
    4.23 @@ -48,7 +48,7 @@
    4.24  \              (free s k & free t i | free s (if i<k then i else Suc i))";
    4.25  by (dB.induct_tac "s" 1);
    4.26  by (Asm_simp_tac 2);
    4.27 -by (Fast_tac 2);
    4.28 +by (Blast_tac 2);
    4.29  by (asm_full_simp_tac (addsplit (!simpset)) 2);
    4.30  by(simp_tac (!simpset addsimps [pred_def,subst_Var]
    4.31                        setloop (split_tac [expand_if,expand_nat_case])) 1);
    4.32 @@ -94,17 +94,17 @@
    4.33  
    4.34  goal Eta.thy "!!s. s -e>> s' ==> Abs s -e>> Abs s'";
    4.35  by (etac rtrancl_induct 1);
    4.36 -by (ALLGOALS(fast_tac (!claset addIs [rtrancl_refl,rtrancl_into_rtrancl])));
    4.37 +by (ALLGOALS(blast_tac (!claset addIs [rtrancl_refl,rtrancl_into_rtrancl])));
    4.38  qed "rtrancl_eta_Abs";
    4.39  
    4.40  goal Eta.thy "!!s. s -e>> s' ==> s @ t -e>> s' @ t";
    4.41  by (etac rtrancl_induct 1);
    4.42 -by (ALLGOALS(fast_tac (!claset addIs [rtrancl_refl,rtrancl_into_rtrancl])));
    4.43 +by (ALLGOALS(blast_tac (!claset addIs [rtrancl_refl,rtrancl_into_rtrancl])));
    4.44  qed "rtrancl_eta_AppL";
    4.45  
    4.46  goal Eta.thy "!!s. t -e>> t' ==> s @ t -e>> s @ t'";
    4.47  by (etac rtrancl_induct 1);
    4.48 -by (ALLGOALS(fast_tac (!claset addIs [rtrancl_refl,rtrancl_into_rtrancl])));
    4.49 +by (ALLGOALS(blast_tac (!claset addIs [rtrancl_refl,rtrancl_into_rtrancl])));
    4.50  qed "rtrancl_eta_AppR";
    4.51  
    4.52  goal Eta.thy "!!s. [| s -e>> s'; t -e>> t' |] ==> s @ t -e>> s' @ t'";
    4.53 @@ -142,9 +142,9 @@
    4.54  goal Eta.thy "!s t i. s -e> t --> u[s/i] -e>> u[t/i]";
    4.55  by (dB.induct_tac "u" 1);
    4.56  by (ALLGOALS(asm_simp_tac (addsplit (!simpset))));
    4.57 -by (fast_tac (!claset addIs [r_into_rtrancl]) 1);
    4.58 -by (fast_tac (!claset addSIs [rtrancl_eta_App]) 1);
    4.59 -by (fast_tac (!claset addSIs [rtrancl_eta_Abs,eta_lift]) 1);
    4.60 +by (blast_tac (!claset addIs [r_into_rtrancl]) 1);
    4.61 +by (blast_tac (!claset addSIs [rtrancl_eta_App]) 1);
    4.62 +by (blast_tac (!claset addSIs [rtrancl_eta_Abs,eta_lift]) 1);
    4.63  qed_spec_mp "rtrancl_eta_subst";
    4.64  
    4.65  goalw Eta.thy [square_def] "square beta eta (eta^*) (beta^=)";
    4.66 @@ -179,7 +179,7 @@
    4.67    by (etac thin_rl 1);
    4.68    by (res_inst_tac [("dB","t")] dB_case_distinction 1);
    4.69      by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
    4.70 -    by (fast_tac (HOL_cs addDs [less_not_refl2]) 1);
    4.71 +    by (blast_tac (HOL_cs addDs [less_not_refl2]) 1);
    4.72     by (Simp_tac 1);
    4.73    by (Simp_tac 1);
    4.74   by (Asm_simp_tac 1);
    4.75 @@ -196,7 +196,7 @@
    4.76   by (res_inst_tac [("dB","t")] dB_case_distinction 1);
    4.77     by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
    4.78    by (Simp_tac 1);
    4.79 -  by (fast_tac HOL_cs 1);
    4.80 +  by (Blast_tac 1);
    4.81   by (Simp_tac 1);
    4.82  by (Asm_simp_tac 1);
    4.83  by (etac thin_rl 1);
    4.84 @@ -211,7 +211,7 @@
    4.85    by (simp_tac (!simpset setloop (split_tac [expand_if])) 1);
    4.86   by (Simp_tac 1);
    4.87  by (Simp_tac 1);
    4.88 -by (fast_tac HOL_cs 1);
    4.89 +by (Blast_tac 1);
    4.90  qed_spec_mp "not_free_iff_lifted";
    4.91  
    4.92  goal Eta.thy "(!s u. (~free s 0) --> R(Abs(s @ Var 0))(s[u/0])) = \
     5.1 --- a/src/HOL/Lambda/Lambda.ML	Fri Apr 04 11:18:19 1997 +0200
     5.2 +++ b/src/HOL/Lambda/Lambda.ML	Fri Apr 04 11:18:52 1997 +0200
     5.3 @@ -23,29 +23,30 @@
     5.4  
     5.5  goal Lambda.thy "!!s. s ->> s' ==> Abs s ->> Abs s'";
     5.6  by (etac rtrancl_induct 1);
     5.7 -by (ALLGOALS(fast_tac (!claset addIs [rtrancl_into_rtrancl])));
     5.8 +by (ALLGOALS (blast_tac (!claset addIs [rtrancl_into_rtrancl])));
     5.9  qed "rtrancl_beta_Abs";
    5.10  AddSIs [rtrancl_beta_Abs];
    5.11  
    5.12  goal Lambda.thy "!!s. s ->> s' ==> s @ t ->> s' @ t";
    5.13  by (etac rtrancl_induct 1);
    5.14 -by (ALLGOALS(fast_tac (!claset addIs [rtrancl_into_rtrancl])));
    5.15 +by (ALLGOALS (blast_tac (!claset addIs [rtrancl_into_rtrancl])));
    5.16  qed "rtrancl_beta_AppL";
    5.17  
    5.18  goal Lambda.thy "!!s. t ->> t' ==> s @ t ->> s @ t'";
    5.19  by (etac rtrancl_induct 1);
    5.20 -by (ALLGOALS(fast_tac (!claset addIs [rtrancl_into_rtrancl])));
    5.21 +by (ALLGOALS (blast_tac (!claset addIs [rtrancl_into_rtrancl])));
    5.22  qed "rtrancl_beta_AppR";
    5.23  
    5.24  goal Lambda.thy "!!s. [| s ->> s'; t ->> t' |] ==> s @ t ->> s' @ t'";
    5.25 -by (deepen_tac (!claset addSIs [rtrancl_beta_AppL,rtrancl_beta_AppR]
    5.26 +by (deepen_tac (!claset addSIs [rtrancl_beta_AppL, rtrancl_beta_AppR]
    5.27                          addIs  [rtrancl_trans]) 3 1);
    5.28  qed "rtrancl_beta_App";
    5.29  AddIs [rtrancl_beta_App];
    5.30  
    5.31  (*** subst and lift ***)
    5.32  
    5.33 -fun addsplit ss = ss addsimps [subst_Var] setloop (split_inside_tac [expand_if]);
    5.34 +fun addsplit ss = ss addsimps [subst_Var] 
    5.35 +                     setloop  (split_inside_tac [expand_if]);
    5.36  
    5.37  goal Lambda.thy "(Var k)[u/k] = u";
    5.38  by (asm_full_simp_tac(addsplit(!simpset)) 1);
    5.39 @@ -123,7 +124,7 @@
    5.40  goal Lambda.thy "!k. liftn (Suc n) t k = lift (liftn n t k) k";
    5.41  by (dB.induct_tac "t" 1);
    5.42  by (ALLGOALS(asm_simp_tac(addsplit(!simpset))));
    5.43 -by (fast_tac (HOL_cs addDs [add_lessD1]) 1);
    5.44 +by (blast_tac (!claset addDs [add_lessD1]) 1);
    5.45  qed "liftn_lift";
    5.46  Addsimps [liftn_lift];
    5.47  
     6.1 --- a/src/HOL/Lambda/ParRed.ML	Fri Apr 04 11:18:19 1997 +0200
     6.2 +++ b/src/HOL/Lambda/ParRed.ML	Fri Apr 04 11:18:52 1997 +0200
     6.3 @@ -21,7 +21,7 @@
     6.4  (*** beta <= par_beta <= beta^* ***)
     6.5  
     6.6  goal ParRed.thy "(Var n => t) = (t = Var n)";
     6.7 -by (Fast_tac 1);
     6.8 +by (Blast_tac 1);
     6.9  qed "par_beta_varL";
    6.10  Addsimps [par_beta_varL];
    6.11  
    6.12 @@ -36,7 +36,7 @@
    6.13  by (rtac subsetI 1);
    6.14  by (split_all_tac 1);
    6.15  by (etac beta.induct 1);
    6.16 -by (ALLGOALS(fast_tac (!claset addSIs [par_beta_refl])));
    6.17 +by (ALLGOALS(blast_tac (!claset addSIs [par_beta_refl])));
    6.18  qed "beta_subset_par_beta";
    6.19  
    6.20  goal ParRed.thy "par_beta <= beta^*";
    6.21 @@ -72,7 +72,7 @@
    6.22  goalw ParRed.thy [diamond_def,commute_def,square_def] "diamond(par_beta)";
    6.23  by (rtac (impI RS allI RS allI) 1);
    6.24  by (etac par_beta.induct 1);
    6.25 -by (ALLGOALS(fast_tac (!claset addSIs [par_beta_subst])));
    6.26 +by (ALLGOALS(Blast.depth_tac (!claset addSIs [par_beta_subst]) 7));
    6.27  qed "diamond_par_beta";
    6.28  
    6.29  
    6.30 @@ -83,16 +83,17 @@
    6.31    by (Simp_tac 1);
    6.32   by (etac rev_mp 1);
    6.33   by (dB.induct_tac "dB1" 1);
    6.34 - by (ALLGOALS(fast_tac (!claset addSIs [par_beta_subst] unsafe_addss (!simpset))));
    6.35 + by (ALLGOALS(fast_tac (!claset addSIs [par_beta_subst] 
    6.36 +                                unsafe_addss (!simpset))));
    6.37  qed_spec_mp "par_beta_cd";
    6.38  
    6.39  (*** Confluence (via cd) ***)
    6.40  
    6.41  goalw ParRed.thy [diamond_def,commute_def,square_def] "diamond(par_beta)";
    6.42 -by (fast_tac (HOL_cs addIs [par_beta_cd]) 1);
    6.43 +by (blast_tac (HOL_cs addIs [par_beta_cd]) 1);
    6.44  qed "diamond_par_beta2";
    6.45  
    6.46  goal ParRed.thy "confluent(beta)";
    6.47 -by (fast_tac (HOL_cs addIs [diamond_par_beta2,diamond_to_confluence,
    6.48 -                           par_beta_subset_beta,beta_subset_par_beta]) 1);
    6.49 +by (blast_tac (HOL_cs addIs [diamond_par_beta2, diamond_to_confluence,
    6.50 +			     par_beta_subset_beta, beta_subset_par_beta]) 1);
    6.51  qed"beta_confluent";
     7.1 --- a/src/HOL/List.ML	Fri Apr 04 11:18:19 1997 +0200
     7.2 +++ b/src/HOL/List.ML	Fri Apr 04 11:18:52 1997 +0200
     7.3 @@ -23,7 +23,6 @@
     7.4  by (list.induct_tac "xs" 1);
     7.5  by (Simp_tac 1);
     7.6  by (Asm_simp_tac 1);
     7.7 -by (REPEAT(resolve_tac [exI,refl,conjI] 1));
     7.8  qed "neq_Nil_conv";
     7.9  
    7.10  
    7.11 @@ -31,10 +30,10 @@
    7.12  
    7.13  goal List.thy
    7.14   "P(list_case a f xs) = ((xs=[] --> P(a)) & \
    7.15 -\                         (!y ys. xs=y#ys --> P(f y ys)))";
    7.16 +\                        (!y ys. xs=y#ys --> P(f y ys)))";
    7.17  by (list.induct_tac "xs" 1);
    7.18  by (ALLGOALS Asm_simp_tac);
    7.19 -by (Fast_tac 1);
    7.20 +by (Blast_tac 1);
    7.21  qed "expand_list_case";
    7.22  
    7.23  val prems = goal List.thy "[| P([]); !!x xs. P(x#xs) |] ==> P(xs)";
    7.24 @@ -44,8 +43,8 @@
    7.25  
    7.26  goal List.thy  "(xs=[] --> P([])) & (!y ys. xs=y#ys --> P(y#ys)) --> P(xs)";
    7.27  by (list.induct_tac "xs" 1);
    7.28 -by (Fast_tac 1);
    7.29 -by (Fast_tac 1);
    7.30 +by (Blast_tac 1);
    7.31 +by (Blast_tac 1);
    7.32  bind_thm("list_eq_cases",
    7.33    impI RSN (2,allI RSN (2,allI RSN (2,impI RS (conjI RS (result() RS mp))))));
    7.34  
    7.35 @@ -73,7 +72,7 @@
    7.36  goal List.thy "([] = xs@ys) = (xs=[] & ys=[])";
    7.37  by (list.induct_tac "xs" 1);
    7.38  by (ALLGOALS Asm_simp_tac);
    7.39 -by(Fast_tac 1);
    7.40 +by(Blast_tac 1);
    7.41  qed "Nil_is_append_conv";
    7.42  AddIffs [Nil_is_append_conv];
    7.43  
    7.44 @@ -175,19 +174,19 @@
    7.45  goal thy "set_of_list (xs@ys) = (set_of_list xs Un set_of_list ys)";
    7.46  by (list.induct_tac "xs" 1);
    7.47  by (ALLGOALS Asm_simp_tac);
    7.48 -by (Fast_tac 1);
    7.49 +by (Blast_tac 1);
    7.50  qed "set_of_list_append";
    7.51  Addsimps[set_of_list_append];
    7.52  
    7.53  goal thy "(x mem xs) = (x: set_of_list xs)";
    7.54  by (list.induct_tac "xs" 1);
    7.55  by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
    7.56 -by (Fast_tac 1);
    7.57 +by (Blast_tac 1);
    7.58  qed "set_of_list_mem_eq";
    7.59  
    7.60  goal List.thy "set_of_list l <= set_of_list (x#l)";
    7.61  by (Simp_tac 1);
    7.62 -by (Fast_tac 1);
    7.63 +by (Blast_tac 1);
    7.64  qed "set_of_list_subset_Cons";
    7.65  
    7.66  goal List.thy "(set_of_list xs = {}) = (xs = [])";
    7.67 @@ -199,7 +198,7 @@
    7.68  goal List.thy "set_of_list(rev xs) = set_of_list(xs)";
    7.69  by(list.induct_tac "xs" 1);
    7.70  by(ALLGOALS Asm_simp_tac);
    7.71 -by(Fast_tac 1);
    7.72 +by(Blast_tac 1);
    7.73  qed "set_of_list_rev";
    7.74  Addsimps [set_of_list_rev];
    7.75  
    7.76 @@ -227,7 +226,7 @@
    7.77  goal List.thy "list_all P xs = (!x. x mem xs --> P(x))";
    7.78  by (list.induct_tac "xs" 1);
    7.79  by (ALLGOALS (asm_simp_tac (!simpset setloop (split_tac [expand_if]))));
    7.80 -by (Fast_tac 1);
    7.81 +by (Blast_tac 1);
    7.82  qed "list_all_mem_conv";
    7.83  
    7.84  
    7.85 @@ -463,7 +462,7 @@
    7.86   by(ALLGOALS Asm_simp_tac);
    7.87  by(strip_tac 1);
    7.88  by(res_inst_tac [("n","n")] natE 1);
    7.89 - by(Fast_tac 1);
    7.90 + by(Blast_tac 1);
    7.91  by(res_inst_tac [("n","i")] natE 1);
    7.92  by(ALLGOALS (hyp_subst_tac THEN' Asm_full_simp_tac));
    7.93  qed_spec_mp "nth_take";
    7.94 @@ -486,7 +485,7 @@
    7.95  by(list.induct_tac "xs" 1);
    7.96   by(Simp_tac 1);
    7.97  by(asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1);
    7.98 -by(Fast_tac 1);
    7.99 +by(Blast_tac 1);
   7.100  bind_thm("takeWhile_append1", conjI RS (result() RS mp));
   7.101  Addsimps [takeWhile_append1];
   7.102  
   7.103 @@ -503,7 +502,7 @@
   7.104  by(list.induct_tac "xs" 1);
   7.105   by(Simp_tac 1);
   7.106  by(asm_full_simp_tac (!simpset setloop (split_tac[expand_if])) 1);
   7.107 -by(Fast_tac 1);
   7.108 +by(Blast_tac 1);
   7.109  bind_thm("dropWhile_append1", conjI RS (result() RS mp));
   7.110  Addsimps [dropWhile_append1];
   7.111  
     8.1 --- a/src/HOL/NatDef.ML	Fri Apr 04 11:18:19 1997 +0200
     8.2 +++ b/src/HOL/NatDef.ML	Fri Apr 04 11:18:52 1997 +0200
     8.3 @@ -28,7 +28,7 @@
     8.4      "[| i: Nat;  P(Zero_Rep);   \
     8.5  \       !!j. [| j: Nat; P(j) |] ==> P(Suc_Rep(j)) |]  ==> P(i)";
     8.6  by (rtac ([Nat_def, Nat_fun_mono, major] MRS def_induct) 1);
     8.7 -by (fast_tac (!claset addIs prems) 1);
     8.8 +by (blast_tac (!claset addIs prems) 1);
     8.9  qed "Nat_induct";
    8.10  
    8.11  val prems = goalw thy [Zero_def,Suc_def]
    8.12 @@ -65,7 +65,7 @@
    8.13  by (fast_tac (!claset addSEs prems) 1);
    8.14  by (nat_ind_tac "n" 1);
    8.15  by (rtac (refl RS disjI1) 1);
    8.16 -by (Fast_tac 1);
    8.17 +by (Blast_tac 1);
    8.18  qed "natE";
    8.19  
    8.20  (*** Isomorphisms: Abs_Nat and Rep_Nat ***)
    8.21 @@ -126,17 +126,17 @@
    8.22  (*** nat_case -- the selection operator for nat ***)
    8.23  
    8.24  goalw thy [nat_case_def] "nat_case a f 0 = a";
    8.25 -by (fast_tac (!claset addIs [select_equality]) 1);
    8.26 +by (blast_tac (!claset addIs [select_equality]) 1);
    8.27  qed "nat_case_0";
    8.28  
    8.29  goalw thy [nat_case_def] "nat_case a f (Suc k) = f(k)";
    8.30 -by (fast_tac (!claset addIs [select_equality]) 1);
    8.31 +by (blast_tac (!claset addIs [select_equality]) 1);
    8.32  qed "nat_case_Suc";
    8.33  
    8.34  (** Introduction rules for 'pred_nat' **)
    8.35  
    8.36  goalw thy [pred_nat_def] "(n, Suc(n)) : pred_nat";
    8.37 -by (Fast_tac 1);
    8.38 +by (Blast_tac 1);
    8.39  qed "pred_natI";
    8.40  
    8.41  val major::prems = goalw thy [pred_nat_def]
    8.42 @@ -149,8 +149,8 @@
    8.43  goalw thy [wf_def] "wf(pred_nat)";
    8.44  by (strip_tac 1);
    8.45  by (nat_ind_tac "x" 1);
    8.46 -by (fast_tac (!claset addSEs [mp, pred_natE]) 2);
    8.47 -by (fast_tac (!claset addSEs [mp, pred_natE]) 1);
    8.48 +by (blast_tac (!claset addSEs [mp, pred_natE]) 2);
    8.49 +by (blast_tac (!claset addSEs [mp, pred_natE]) 1);
    8.50  qed "wf_pred_nat";
    8.51  
    8.52  
    8.53 @@ -228,7 +228,7 @@
    8.54  (** Elimination properties **)
    8.55  
    8.56  val prems = goalw thy [less_def] "n<m ==> ~ m<(n::nat)";
    8.57 -by (fast_tac (!claset addIs ([wf_pred_nat, wf_trancl RS wf_asym]@prems))1);
    8.58 +by (blast_tac (!claset addIs ([wf_pred_nat, wf_trancl RS wf_asym]@prems))1);
    8.59  qed "less_not_sym";
    8.60  
    8.61  (* [| n<m; m<n |] ==> R *)
    8.62 @@ -243,7 +243,7 @@
    8.63  bind_thm ("less_irrefl", (less_not_refl RS notE));
    8.64  
    8.65  goal thy "!!m. n<m ==> m ~= (n::nat)";
    8.66 -by (fast_tac (!claset addEs [less_irrefl]) 1);
    8.67 +by (blast_tac (!claset addEs [less_irrefl]) 1);
    8.68  qed "less_not_refl2";
    8.69  
    8.70  
    8.71 @@ -272,14 +272,13 @@
    8.72      "[| m < Suc(n);  m<n ==> P;  m=n ==> P |] ==> P";
    8.73  by (rtac (major RS lessE) 1);
    8.74  by (rtac eq 1);
    8.75 -by (Fast_tac 1);
    8.76 +by (Blast_tac 1);
    8.77  by (rtac less 1);
    8.78 -by (Fast_tac 1);
    8.79 +by (Blast_tac 1);
    8.80  qed "less_SucE";
    8.81  
    8.82  goal thy "(m < Suc(n)) = (m < n | m = n)";
    8.83 -by (fast_tac (!claset addSIs [lessI]
    8.84 -                      addEs  [less_trans, less_SucE]) 1);
    8.85 +by (fast_tac (!claset addEs  [less_trans, less_SucE]) 1);
    8.86  qed "less_Suc_eq";
    8.87  
    8.88  val prems = goal thy "m<n ==> n ~= 0";
    8.89 @@ -316,14 +315,13 @@
    8.90  qed "Suc_lessE";
    8.91  
    8.92  goal thy "!!m n. Suc(m) < Suc(n) ==> m<n";
    8.93 -by (fast_tac (!claset addEs [lessE, Suc_lessD] addIs [lessI]) 1);
    8.94 +by (blast_tac (!claset addEs [lessE, make_elim Suc_lessD]) 1);
    8.95  qed "Suc_less_SucD";
    8.96  
    8.97  goal thy "!!m n. m<n ==> Suc(m) < Suc(n)";
    8.98  by (etac rev_mp 1);
    8.99  by (nat_ind_tac "n" 1);
   8.100 -by (ALLGOALS (fast_tac (!claset addSIs [lessI]
   8.101 -                                addEs  [less_trans, lessE])));
   8.102 +by (ALLGOALS (fast_tac (!claset addEs  [less_trans, lessE])));
   8.103  qed "Suc_mono";
   8.104  
   8.105  
   8.106 @@ -333,7 +331,7 @@
   8.107  Addsimps [Suc_less_eq];
   8.108  
   8.109  goal thy "~(Suc(n) < n)";
   8.110 -by (fast_tac (!claset addEs [Suc_lessD RS less_irrefl]) 1);
   8.111 +by (blast_tac (!claset addEs [Suc_lessD RS less_irrefl]) 1);
   8.112  qed "not_Suc_n_less_n";
   8.113  Addsimps [not_Suc_n_less_n];
   8.114  
   8.115 @@ -341,7 +339,7 @@
   8.116  by (nat_ind_tac "k" 1);
   8.117  by (ALLGOALS (asm_simp_tac (!simpset)));
   8.118  by (asm_simp_tac (!simpset addsimps [less_Suc_eq]) 1);
   8.119 -by (fast_tac (!claset addDs [Suc_lessD]) 1);
   8.120 +by (blast_tac (!claset addDs [Suc_lessD]) 1);
   8.121  qed_spec_mp "less_trans_Suc";
   8.122  
   8.123  (*"Less than" is a linear ordering*)
   8.124 @@ -350,7 +348,7 @@
   8.125  by (nat_ind_tac "n" 1);
   8.126  by (rtac (refl RS disjI1 RS disjI2) 1);
   8.127  by (rtac (zero_less_Suc RS disjI1) 1);
   8.128 -by (fast_tac (!claset addIs [lessI, Suc_mono, less_SucI] addEs [lessE]) 1);
   8.129 +by (fast_tac (!claset addIs [Suc_mono, less_SucI] addEs [lessE]) 1);
   8.130  qed "less_linear";
   8.131  
   8.132  qed_goal "nat_less_cases" thy 
   8.133 @@ -453,16 +451,16 @@
   8.134  val leE = make_elim leD;
   8.135  
   8.136  goal thy "(~n<m) = (m<=(n::nat))";
   8.137 -by (fast_tac (!claset addIs [leI] addEs [leE]) 1);
   8.138 +by (blast_tac (!claset addIs [leI] addEs [leE]) 1);
   8.139  qed "not_less_iff_le";
   8.140  
   8.141  goalw thy [le_def] "!!m. ~ m <= n ==> n<(m::nat)";
   8.142 -by (Fast_tac 1);
   8.143 +by (Blast_tac 1);
   8.144  qed "not_leE";
   8.145  
   8.146  goalw thy [le_def] "!!m. m < n ==> Suc(m) <= n";
   8.147  by (simp_tac (!simpset addsimps [less_Suc_eq]) 1);
   8.148 -by (fast_tac (!claset addEs [less_irrefl,less_asym]) 1);
   8.149 +by (blast_tac (!claset addEs [less_irrefl,less_asym]) 1);
   8.150  qed "lessD";
   8.151  
   8.152  goalw thy [le_def] "!!m. Suc(m) <= n ==> m <= n";
   8.153 @@ -474,32 +472,32 @@
   8.154          "!!m. Suc m <= n ==> m < n";
   8.155  by (asm_full_simp_tac (!simpset addsimps [less_Suc_eq]) 1);
   8.156  by (cut_facts_tac [less_linear] 1);
   8.157 -by (Fast_tac 1);
   8.158 +by (Blast_tac 1);
   8.159  qed "Suc_le_lessD";
   8.160  
   8.161  goal thy "(Suc m <= n) = (m < n)";
   8.162 -by (fast_tac (!claset addIs [lessD, Suc_le_lessD]) 1);
   8.163 +by (blast_tac (!claset addIs [lessD, Suc_le_lessD]) 1);
   8.164  qed "Suc_le_eq";
   8.165  
   8.166  goalw thy [le_def] "!!m. m <= n ==> m <= Suc n";
   8.167 -by (fast_tac (!claset addDs [Suc_lessD]) 1);
   8.168 +by (blast_tac (!claset addDs [Suc_lessD]) 1);
   8.169  qed "le_SucI";
   8.170  Addsimps[le_SucI];
   8.171  
   8.172  bind_thm ("le_Suc", not_Suc_n_less_n RS leI);
   8.173  
   8.174  goalw thy [le_def] "!!m. m < n ==> m <= (n::nat)";
   8.175 -by (fast_tac (!claset addEs [less_asym]) 1);
   8.176 +by (blast_tac (!claset addEs [less_asym]) 1);
   8.177  qed "less_imp_le";
   8.178  
   8.179  goalw thy [le_def] "!!m. m <= n ==> m < n | m=(n::nat)";
   8.180  by (cut_facts_tac [less_linear] 1);
   8.181 -by (fast_tac (!claset addEs [less_irrefl,less_asym]) 1);
   8.182 +by (blast_tac (!claset addEs [less_irrefl,less_asym]) 1);
   8.183  qed "le_imp_less_or_eq";
   8.184  
   8.185  goalw thy [le_def] "!!m. m<n | m=n ==> m <=(n::nat)";
   8.186  by (cut_facts_tac [less_linear] 1);
   8.187 -by (fast_tac (!claset addEs [less_irrefl,less_asym]) 1);
   8.188 +by (blast_tac (!claset addEs [less_irrefl,less_asym]) 1);
   8.189  by (flexflex_tac);
   8.190  qed "less_or_eq_imp_le";
   8.191  
   8.192 @@ -522,13 +520,16 @@
   8.193  qed "less_le_trans";
   8.194  
   8.195  goal thy "!!i. [| i <= j; j <= k |] ==> i <= (k::nat)";
   8.196 -by (EVERY1[dtac le_imp_less_or_eq, dtac le_imp_less_or_eq,
   8.197 -          rtac less_or_eq_imp_le, fast_tac (!claset addIs [less_trans])]);
   8.198 +by (EVERY1[dtac le_imp_less_or_eq, 
   8.199 +	   dtac le_imp_less_or_eq,
   8.200 +	   rtac less_or_eq_imp_le, 
   8.201 +	   fast_tac (!claset addIs [less_trans])]);
   8.202  qed "le_trans";
   8.203  
   8.204 -val prems = goal thy "!!m. [| m <= n; n <= m |] ==> m = (n::nat)";
   8.205 -by (EVERY1[dtac le_imp_less_or_eq, dtac le_imp_less_or_eq,
   8.206 -          fast_tac (!claset addEs [less_irrefl,less_asym])]);
   8.207 +goal thy "!!m. [| m <= n; n <= m |] ==> m = (n::nat)";
   8.208 +by (EVERY1[dtac le_imp_less_or_eq, 
   8.209 +	   dtac le_imp_less_or_eq,
   8.210 +	   blast_tac (!claset addEs [less_irrefl,less_asym])]);
   8.211  qed "le_anti_sym";
   8.212  
   8.213  goal thy "(Suc(n) <= Suc(m)) = (n <= m)";
   8.214 @@ -543,7 +544,7 @@
   8.215   br conjI 1;
   8.216    be less_imp_le 1;
   8.217   be (less_not_refl2 RS not_sym) 1;
   8.218 -by(fast_tac (!claset addSDs [le_imp_less_or_eq]) 1);
   8.219 +by(blast_tac (!claset addSDs [le_imp_less_or_eq]) 1);
   8.220  qed "nat_less_le";
   8.221  
   8.222  (** LEAST -- the least number operator **)
   8.223 @@ -551,9 +552,9 @@
   8.224  val [prem1,prem2] = goalw thy [Least_def]
   8.225      "[| P(k::nat);  !!x. x<k ==> ~P(x) |] ==> (LEAST x.P(x)) = k";
   8.226  by (rtac select_equality 1);
   8.227 -by (fast_tac (!claset addSIs [prem1,prem2]) 1);
   8.228 +by (blast_tac (!claset addSIs [prem1,prem2]) 1);
   8.229  by (cut_facts_tac [less_linear] 1);
   8.230 -by (fast_tac (!claset addSIs [prem1] addSDs [prem2]) 1);
   8.231 +by (blast_tac (!claset addSIs [prem1] addSDs [prem2]) 1);
   8.232  qed "Least_equality";
   8.233  
   8.234  val [prem] = goal thy "P(k::nat) ==> P(LEAST x.P(x))";
   8.235 @@ -564,7 +565,7 @@
   8.236  by (res_inst_tac [("s","n")] (Least_equality RS ssubst) 1);
   8.237  by (assume_tac 1);
   8.238  by (assume_tac 2);
   8.239 -by (Fast_tac 1);
   8.240 +by (Blast_tac 1);
   8.241  qed "LeastI";
   8.242  
   8.243  (*Proof is almost identical to the one above!*)
   8.244 @@ -576,7 +577,7 @@
   8.245  by (res_inst_tac [("s","n")] (Least_equality RS ssubst) 1);
   8.246  by (assume_tac 1);
   8.247  by (rtac le_refl 2);
   8.248 -by (fast_tac (!claset addIs [less_imp_le,le_trans]) 1);
   8.249 +by (blast_tac (!claset addIs [less_imp_le,le_trans]) 1);
   8.250  qed "Least_le";
   8.251  
   8.252  val [prem] = goal thy "k < (LEAST x.P(x)) ==> ~P(k::nat)";
   8.253 @@ -593,23 +594,23 @@
   8.254          safe_tac (!claset addSEs [LeastI]),
   8.255          rename_tac "j" 1,
   8.256          res_inst_tac [("n","j")] natE 1,
   8.257 -        Fast_tac 1,
   8.258 -        fast_tac (!claset addDs [Suc_less_SucD, not_less_Least]) 1,
   8.259 +        Blast_tac 1,
   8.260 +        blast_tac (!claset addDs [Suc_less_SucD, not_less_Least]) 1,
   8.261          rename_tac "k n" 1,
   8.262          res_inst_tac [("n","k")] natE 1,
   8.263 -        Fast_tac 1,
   8.264 +        Blast_tac 1,
   8.265          hyp_subst_tac 1,
   8.266          rewtac Least_def,
   8.267          rtac (select_equality RS arg_cong RS sym) 1,
   8.268          safe_tac (!claset),
   8.269          dtac Suc_mono 1,
   8.270 -        Fast_tac 1,
   8.271 +        Blast_tac 1,
   8.272          cut_facts_tac [less_linear] 1,
   8.273          safe_tac (!claset),
   8.274          atac 2,
   8.275 -        Fast_tac 2,
   8.276 +        Blast_tac 2,
   8.277          dtac Suc_mono 1,
   8.278 -        Fast_tac 1]);
   8.279 +        Blast_tac 1]);
   8.280  
   8.281  
   8.282  (*** Instantiation of transitivity prover ***)
   8.283 @@ -633,8 +634,8 @@
   8.284    (fn _ => [etac swap2 1, etac leD 1]);
   8.285  val eqI = prove_goal thy "!!m. [| m < Suc n; n < Suc m |] ==> m=n"
   8.286    (fn _ => [etac less_SucE 1,
   8.287 -            fast_tac (HOL_cs addSDs [Suc_less_SucD] addSEs [less_irrefl]
   8.288 -                             addDs [less_trans_Suc]) 1,
   8.289 +            fast_tac (!claset addSDs [Suc_less_SucD] addSEs [less_irrefl]
   8.290 +                              addDs [less_trans_Suc]) 1,
   8.291              atac 1]);
   8.292  val leD = le_eq_less_Suc RS iffD1;
   8.293  val not_lessD = nat_leI RS leD;
     9.1 --- a/src/HOL/Relation.ML	Fri Apr 04 11:18:19 1997 +0200
     9.2 +++ b/src/HOL/Relation.ML	Fri Apr 04 11:18:52 1997 +0200
     9.3 @@ -9,7 +9,7 @@
     9.4  (** Identity relation **)
     9.5  
     9.6  goalw Relation.thy [id_def] "(a,a) : id";  
     9.7 -by (Fast_tac 1);
     9.8 +by (Blast_tac 1);
     9.9  qed "idI";
    9.10  
    9.11  val major::prems = goalw Relation.thy [id_def]
    9.12 @@ -21,7 +21,7 @@
    9.13  qed "idE";
    9.14  
    9.15  goalw Relation.thy [id_def] "(a,b):id = (a=b)";
    9.16 -by (Fast_tac 1);
    9.17 +by (Blast_tac 1);
    9.18  qed "pair_in_id_conv";
    9.19  Addsimps [pair_in_id_conv];
    9.20  
    9.21 @@ -30,7 +30,7 @@
    9.22  
    9.23  goalw Relation.thy [comp_def]
    9.24      "!!r s. [| (a,b):s; (b,c):r |] ==> (a,c) : r O s";
    9.25 -by (Fast_tac 1);
    9.26 +by (Blast_tac 1);
    9.27  qed "compI";
    9.28  
    9.29  (*proof requires higher-level assumptions or a delaying of hyp_subst_tac*)
    9.30 @@ -55,12 +55,12 @@
    9.31  AddSEs [compE, idE];
    9.32  
    9.33  goal Relation.thy "!!r s. [| r'<=r; s'<=s |] ==> (r' O s') <= (r O s)";
    9.34 -by (Fast_tac 1);
    9.35 +by (Blast_tac 1);
    9.36  qed "comp_mono";
    9.37  
    9.38  goal Relation.thy
    9.39      "!!r s. [| s <= A Times B;  r <= B Times C |] ==> (r O s) <= A Times C";
    9.40 -by (Fast_tac 1);
    9.41 +by (Blast_tac 1);
    9.42  qed "comp_subset_Sigma";
    9.43  
    9.44  (** Natural deduction for trans(r) **)
    9.45 @@ -72,7 +72,7 @@
    9.46  
    9.47  goalw Relation.thy [trans_def]
    9.48      "!!r. [| trans(r);  (a,b):r;  (b,c):r |] ==> (a,c):r";
    9.49 -by (Fast_tac 1);
    9.50 +by (Blast_tac 1);
    9.51  qed "transD";
    9.52  
    9.53  (** Natural deduction for converse(r) **)
    9.54 @@ -88,7 +88,7 @@
    9.55  qed "converseI";
    9.56  
    9.57  goalw Relation.thy [converse_def] "!!a b r. (a,b) : converse(r) ==> (b,a) : r";
    9.58 -by (Fast_tac 1);
    9.59 +by (Blast_tac 1);
    9.60  qed "converseD";
    9.61  
    9.62  (*More general than converseD, as it "splits" the member of the relation*)
    9.63 @@ -104,14 +104,14 @@
    9.64  AddSEs [converseE];
    9.65  
    9.66  goalw Relation.thy [converse_def] "converse(converse R) = R";
    9.67 -by (Fast_tac 1);
    9.68 +by (Blast_tac 1);
    9.69  qed "converse_converse";
    9.70  
    9.71  (** Domain **)
    9.72  
    9.73  qed_goalw "Domain_iff" Relation.thy [Domain_def]
    9.74      "a: Domain(r) = (EX y. (a,y): r)"
    9.75 - (fn _=> [ (Fast_tac 1) ]);
    9.76 + (fn _=> [ (Blast_tac 1) ]);
    9.77  
    9.78  qed_goal "DomainI" Relation.thy "!!a b r. (a,b): r ==> a: Domain(r)"
    9.79   (fn _ => [ (etac (exI RS (Domain_iff RS iffD2)) 1) ]);
    9.80 @@ -144,16 +144,16 @@
    9.81  
    9.82  qed_goalw "Image_iff" Relation.thy [Image_def]
    9.83      "b : r^^A = (? x:A. (x,b):r)"
    9.84 - (fn _ => [ Fast_tac 1 ]);
    9.85 + (fn _ => [ Blast_tac 1 ]);
    9.86  
    9.87  qed_goal "Image_singleton_iff" Relation.thy
    9.88      "(b : r^^{a}) = ((a,b):r)"
    9.89   (fn _ => [ rtac (Image_iff RS trans) 1,
    9.90 -            Fast_tac 1 ]);
    9.91 +            Blast_tac 1 ]);
    9.92  
    9.93  qed_goalw "ImageI" Relation.thy [Image_def]
    9.94      "!!a b r. [| (a,b): r;  a:A |] ==> b : r^^A"
    9.95 - (fn _ => [ (Fast_tac 1)]);
    9.96 + (fn _ => [ (Blast_tac 1)]);
    9.97  
    9.98  qed_goalw "ImageE" Relation.thy [Image_def]
    9.99      "[| b: r^^A;  !!x.[| (x,b): r;  x:A |] ==> P |] ==> P"
    10.1 --- a/src/HOL/Set.ML	Fri Apr 04 11:18:19 1997 +0200
    10.2 +++ b/src/HOL/Set.ML	Fri Apr 04 11:18:52 1997 +0200
    10.3 @@ -151,10 +151,10 @@
    10.4  AddEs  [subsetD, subsetCE];
    10.5  
    10.6  qed_goal "subset_refl" Set.thy "A <= (A::'a set)"
    10.7 - (fn _=> [Fast_tac 1]);
    10.8 + (fn _=> [Blast_tac 1]);
    10.9  
   10.10  val prems = goal Set.thy "!!B. [| A<=B;  B<=C |] ==> A<=(C::'a set)";
   10.11 -by (Fast_tac 1);
   10.12 +by (Blast_tac 1);
   10.13  qed "subset_trans";
   10.14  
   10.15  
   10.16 @@ -206,7 +206,7 @@
   10.17  section "The empty set -- {}";
   10.18  
   10.19  qed_goalw "empty_iff" Set.thy [empty_def] "(c : {}) = False"
   10.20 - (fn _ => [ (Fast_tac 1) ]);
   10.21 + (fn _ => [ (Blast_tac 1) ]);
   10.22  
   10.23  Addsimps [empty_iff];
   10.24  
   10.25 @@ -216,14 +216,14 @@
   10.26  AddSEs [emptyE];
   10.27  
   10.28  qed_goal "empty_subsetI" Set.thy "{} <= A"
   10.29 - (fn _ => [ (Fast_tac 1) ]);
   10.30 + (fn _ => [ (Blast_tac 1) ]);
   10.31  
   10.32  qed_goal "equals0I" Set.thy "[| !!y. y:A ==> False |] ==> A={}"
   10.33   (fn [prem]=>
   10.34    [ (fast_tac (!claset addIs [prem RS FalseE]) 1) ]);
   10.35  
   10.36  qed_goal "equals0D" Set.thy "!!a. [| A={};  a:A |] ==> P"
   10.37 - (fn _ => [ (Fast_tac 1) ]);
   10.38 + (fn _ => [ (Blast_tac 1) ]);
   10.39  
   10.40  goal Set.thy "Ball {} P = True";
   10.41  by (simp_tac (HOL_ss addsimps [mem_Collect_eq, Ball_def, empty_def]) 1);
   10.42 @@ -235,13 +235,13 @@
   10.43  Addsimps [ball_empty, bex_empty];
   10.44  
   10.45  goalw Set.thy [Ball_def] "(!x:A.False) = (A = {})";
   10.46 -by(Fast_tac 1);
   10.47 +by(Blast_tac 1);
   10.48  qed "ball_False";
   10.49  Addsimps [ball_False];
   10.50  
   10.51  (* The dual is probably not helpful:
   10.52  goal Set.thy "(? x:A.True) = (A ~= {})";
   10.53 -by(Fast_tac 1);
   10.54 +by(Blast_tac 1);
   10.55  qed "bex_True";
   10.56  Addsimps [bex_True];
   10.57  *)
   10.58 @@ -267,7 +267,7 @@
   10.59  section "Set complement -- Compl";
   10.60  
   10.61  qed_goalw "Compl_iff" Set.thy [Compl_def] "(c : Compl(A)) = (c~:A)"
   10.62 - (fn _ => [ (Fast_tac 1) ]);
   10.63 + (fn _ => [ (Blast_tac 1) ]);
   10.64  
   10.65  Addsimps [Compl_iff];
   10.66  
   10.67 @@ -293,7 +293,7 @@
   10.68  section "Binary union -- Un";
   10.69  
   10.70  qed_goalw "Un_iff" Set.thy [Un_def] "(c : A Un B) = (c:A | c:B)"
   10.71 - (fn _ => [ Fast_tac 1 ]);
   10.72 + (fn _ => [ Blast_tac 1 ]);
   10.73  
   10.74  Addsimps [Un_iff];
   10.75  
   10.76 @@ -324,7 +324,7 @@
   10.77  section "Binary intersection -- Int";
   10.78  
   10.79  qed_goalw "Int_iff" Set.thy [Int_def] "(c : A Int B) = (c:A & c:B)"
   10.80 - (fn _ => [ (Fast_tac 1) ]);
   10.81 + (fn _ => [ (Blast_tac 1) ]);
   10.82  
   10.83  Addsimps [Int_iff];
   10.84  
   10.85 @@ -353,7 +353,7 @@
   10.86  section "Set difference";
   10.87  
   10.88  qed_goalw "Diff_iff" Set.thy [set_diff_def] "(c : A-B) = (c:A & c~:B)"
   10.89 - (fn _ => [ (Fast_tac 1) ]);
   10.90 + (fn _ => [ (Blast_tac 1) ]);
   10.91  
   10.92  Addsimps [Diff_iff];
   10.93  
   10.94 @@ -378,7 +378,7 @@
   10.95  section "Augmenting a set -- insert";
   10.96  
   10.97  qed_goalw "insert_iff" Set.thy [insert_def] "a : insert b A = (a=b | a:A)"
   10.98 - (fn _ => [Fast_tac 1]);
   10.99 + (fn _ => [Blast_tac 1]);
  10.100  
  10.101  Addsimps [insert_iff];
  10.102  
  10.103 @@ -409,13 +409,13 @@
  10.104   (fn _=> [ (rtac insertI1 1) ]);
  10.105  
  10.106  goal Set.thy "!!a. b : {a} ==> b=a";
  10.107 -by (Fast_tac 1);
  10.108 +by (Blast_tac 1);
  10.109  qed "singletonD";
  10.110  
  10.111  bind_thm ("singletonE", make_elim singletonD);
  10.112  
  10.113  qed_goal "singleton_iff" thy "(b : {a}) = (b=a)" 
  10.114 -(fn _ => [Fast_tac 1]);
  10.115 +(fn _ => [Blast_tac 1]);
  10.116  
  10.117  goal Set.thy "!!a b. {a}={b} ==> a=b";
  10.118  by (fast_tac (!claset addEs [equalityE]) 1);
  10.119 @@ -439,7 +439,7 @@
  10.120  section "Unions of families -- UNION x:A. B(x) is Union(B``A)";
  10.121  
  10.122  goalw Set.thy [UNION_def] "(b: (UN x:A. B(x))) = (EX x:A. b: B(x))";
  10.123 -by (Fast_tac 1);
  10.124 +by (Blast_tac 1);
  10.125  qed "UN_iff";
  10.126  
  10.127  Addsimps [UN_iff];
  10.128 @@ -507,7 +507,7 @@
  10.129  
  10.130  goalw Set.thy [UNION1_def] "(b: (UN x. B(x))) = (EX x. b: B(x))";
  10.131  by (Simp_tac 1);
  10.132 -by (Fast_tac 1);
  10.133 +by (Blast_tac 1);
  10.134  qed "UN1_iff";
  10.135  
  10.136  Addsimps [UN1_iff];
  10.137 @@ -531,7 +531,7 @@
  10.138  
  10.139  goalw Set.thy [INTER1_def] "(b: (INT x. B(x))) = (ALL x. b: B(x))";
  10.140  by (Simp_tac 1);
  10.141 -by (Fast_tac 1);
  10.142 +by (Blast_tac 1);
  10.143  qed "INT1_iff";
  10.144  
  10.145  Addsimps [INT1_iff];
  10.146 @@ -552,7 +552,7 @@
  10.147  section "Union";
  10.148  
  10.149  goalw Set.thy [Union_def] "(A : Union(C)) = (EX X:C. A:X)";
  10.150 -by (Fast_tac 1);
  10.151 +by (Blast_tac 1);
  10.152  qed "Union_iff";
  10.153  
  10.154  Addsimps [Union_iff];
  10.155 @@ -575,7 +575,7 @@
  10.156  section "Inter";
  10.157  
  10.158  goalw Set.thy [Inter_def] "(A : Inter(C)) = (ALL X:C. A:X)";
  10.159 -by (Fast_tac 1);
  10.160 +by (Blast_tac 1);
  10.161  qed "Inter_iff";
  10.162  
  10.163  Addsimps [Inter_iff];
    11.1 --- a/src/HOL/Sum.ML	Fri Apr 04 11:18:19 1997 +0200
    11.2 +++ b/src/HOL/Sum.ML	Fri Apr 04 11:18:52 1997 +0200
    11.3 @@ -53,12 +53,12 @@
    11.4  
    11.5  val [major] = goalw Sum.thy [Inl_Rep_def] "Inl_Rep(a) = Inl_Rep(c) ==> a=c";
    11.6  by (rtac (major RS fun_cong RS fun_cong RS fun_cong RS iffE) 1);
    11.7 -by (Fast_tac 1);
    11.8 +by (Blast_tac 1);
    11.9  qed "Inl_Rep_inject";
   11.10  
   11.11  val [major] = goalw Sum.thy [Inr_Rep_def] "Inr_Rep(b) = Inr_Rep(d) ==> b=d";
   11.12  by (rtac (major RS fun_cong RS fun_cong RS fun_cong RS iffE) 1);
   11.13 -by (Fast_tac 1);
   11.14 +by (Blast_tac 1);
   11.15  qed "Inr_Rep_inject";
   11.16  
   11.17  goalw Sum.thy [Inl_def] "inj(Inl)";
   11.18 @@ -78,11 +78,11 @@
   11.19  val Inr_inject = inj_Inr RS injD;
   11.20  
   11.21  goal Sum.thy "(Inl(x)=Inl(y)) = (x=y)";
   11.22 -by (fast_tac (!claset addSEs [Inl_inject]) 1);
   11.23 +by (blast_tac (!claset addSDs [Inl_inject]) 1);
   11.24  qed "Inl_eq";
   11.25  
   11.26  goal Sum.thy "(Inr(x)=Inr(y)) = (x=y)";
   11.27 -by (fast_tac (!claset addSEs [Inr_inject]) 1);
   11.28 +by (blast_tac (!claset addSDs [Inr_inject]) 1);
   11.29  qed "Inr_eq";
   11.30  
   11.31  AddIffs [Inl_eq, Inr_eq];
   11.32 @@ -92,11 +92,11 @@
   11.33  (** Introduction rules for the injections **)
   11.34  
   11.35  goalw Sum.thy [sum_def] "!!a A B. a : A ==> Inl(a) : A Plus B";
   11.36 -by (Fast_tac 1);
   11.37 +by (Blast_tac 1);
   11.38  qed "InlI";
   11.39  
   11.40  goalw Sum.thy [sum_def] "!!b A B. b : B ==> Inr(b) : A Plus B";
   11.41 -by (Fast_tac 1);
   11.42 +by (Blast_tac 1);
   11.43  qed "InrI";
   11.44  
   11.45  (** Elimination rules **)
   11.46 @@ -119,7 +119,7 @@
   11.47  (** sum_case -- the selection operator for sums **)
   11.48  
   11.49  goalw Sum.thy [sum_case_def] "sum_case f g (Inl x) = f(x)";
   11.50 -by (fast_tac (!claset addIs [select_equality]) 1);
   11.51 +by (blast_tac (!claset addIs [select_equality]) 1);
   11.52  qed "sum_case_Inl";
   11.53  
   11.54  goalw Sum.thy [sum_case_def] "sum_case f g (Inr x) = g(x)";
   11.55 @@ -163,7 +163,7 @@
   11.56  
   11.57  goalw Sum.thy [Part_def]
   11.58      "!!a b A h. [| a : A;  a=h(b) |] ==> a : Part A h";
   11.59 -by (Fast_tac 1);
   11.60 +by (Blast_tac 1);
   11.61  qed "Part_eqI";
   11.62  
   11.63  val PartI = refl RSN (2,Part_eqI);
   11.64 @@ -177,12 +177,15 @@
   11.65  by (REPEAT (ares_tac prems 1));
   11.66  qed "PartE";
   11.67  
   11.68 +AddIs  [Part_eqI];
   11.69 +AddSEs [PartE];
   11.70 +
   11.71  goalw Sum.thy [Part_def] "Part A h <= A";
   11.72  by (rtac Int_lower1 1);
   11.73  qed "Part_subset";
   11.74  
   11.75  goal Sum.thy "!!A B. A<=B ==> Part A h <= Part B h";
   11.76 -by (fast_tac (!claset addSIs [PartI] addSEs [PartE]) 1);
   11.77 +by (Fast_tac 1);
   11.78  qed "Part_mono";
   11.79  
   11.80  val basic_monos = basic_monos @ [Part_mono];
   11.81 @@ -192,14 +195,14 @@
   11.82  qed "PartD1";
   11.83  
   11.84  goal Sum.thy "Part A (%x.x) = A";
   11.85 -by (fast_tac (!claset addIs [PartI] addSEs [PartE]) 1);
   11.86 +by (Blast_tac 1);
   11.87  qed "Part_id";
   11.88  
   11.89  goal Sum.thy "Part (A Int B) h = (Part A h) Int (Part B h)";
   11.90 -by (fast_tac (!claset addIs [PartI] addSEs [PartE]) 1);
   11.91 +by (Fast_tac 1);
   11.92  qed "Part_Int";
   11.93  
   11.94  (*For inductive definitions*)
   11.95  goal Sum.thy "Part (A Int {x.P x}) h = (Part A h) Int {x.P x}";
   11.96 -by (fast_tac (!claset addIs [PartI] addSEs [PartE]) 1);
   11.97 +by (Fast_tac 1);
   11.98  qed "Part_Collect";
    12.1 --- a/src/HOL/Trancl.ML	Fri Apr 04 11:18:19 1997 +0200
    12.2 +++ b/src/HOL/Trancl.ML	Fri Apr 04 11:18:52 1997 +0200
    12.3 @@ -20,7 +20,7 @@
    12.4  (*Reflexivity of rtrancl*)
    12.5  goal Trancl.thy "(a,a) : r^*";
    12.6  by (stac rtrancl_unfold 1);
    12.7 -by (Fast_tac 1);
    12.8 +by (Blast_tac 1);
    12.9  qed "rtrancl_refl";
   12.10  
   12.11  Addsimps [rtrancl_refl];
   12.12 @@ -30,7 +30,7 @@
   12.13  (*Closure under composition with r*)
   12.14  goal Trancl.thy "!!r. [| (a,b) : r^*;  (b,c) : r |] ==> (a,c) : r^*";
   12.15  by (stac rtrancl_unfold 1);
   12.16 -by (Fast_tac 1);
   12.17 +by (Blast_tac 1);
   12.18  qed "rtrancl_into_rtrancl";
   12.19  
   12.20  (*rtrancl of r contains r*)
   12.21 @@ -64,7 +64,7 @@
   12.22  (*by induction on this formula*)
   12.23  by (subgoal_tac "! y. (a::'a,b) = (a,y) --> P(y)" 1);
   12.24  (*now solve first subgoal: this formula is sufficient*)
   12.25 -by (Fast_tac 1);
   12.26 +by (Blast_tac 1);
   12.27  (*now do the induction*)
   12.28  by (resolve_tac [major RS rtrancl_full_induct] 1);
   12.29  by (fast_tac (!claset addIs prems) 1);
   12.30 @@ -124,7 +124,7 @@
   12.31  by (dtac rtrancl_mono 1);
   12.32  by (dtac rtrancl_mono 1);
   12.33  by (Asm_full_simp_tac 1);
   12.34 -by (Fast_tac 1);
   12.35 +by (Blast_tac 1);
   12.36  qed "rtrancl_subset";
   12.37  
   12.38  goal Trancl.thy "!!R. (R^* Un S^*)^* = (R Un S)^*";
   12.39 @@ -165,7 +165,7 @@
   12.40  \     ==> P(a)";
   12.41  by (rtac ((major RS converseI RS rtrancl_converseI) RS rtrancl_induct) 1);
   12.42  by (resolve_tac prems 1);
   12.43 -by (fast_tac (!claset addIs prems addSEs[converseD]addSDs[rtrancl_converseD])1);
   12.44 +by (fast_tac (!claset addIs prems addSDs[rtrancl_converseD])1);
   12.45  qed "converse_rtrancl_induct";
   12.46  
   12.47  val prems = goal Trancl.thy
   12.48 @@ -225,7 +225,7 @@
   12.49  (*by induction on this formula*)
   12.50  by (subgoal_tac "ALL z. (y,z) : r --> P(z)" 1);
   12.51  (*now solve first subgoal: this formula is sufficient*)
   12.52 -by (Fast_tac 1);
   12.53 +by (Blast_tac 1);
   12.54  by (etac rtrancl_induct 1);
   12.55  by (ALLGOALS (fast_tac (!claset addIs (rtrancl_into_trancl1::prems))));
   12.56  qed "trancl_induct";
   12.57 @@ -240,7 +240,7 @@
   12.58  by (REPEAT (eresolve_tac ([asm_rl,disjE,exE,conjE]@prems) 1));
   12.59  by (rtac (rewrite_rule [trancl_def] major RS compEpair) 1);
   12.60  by (etac rtranclE 1);
   12.61 -by (Fast_tac 1);
   12.62 +by (Blast_tac 1);
   12.63  by (fast_tac (!claset addSIs [rtrancl_into_trancl1]) 1);
   12.64  qed "tranclE";
   12.65  
   12.66 @@ -268,11 +268,11 @@
   12.67  by (cut_facts_tac prems 1);
   12.68  by (rtac (major RS rtrancl_induct) 1);
   12.69  by (rtac (refl RS disjI1) 1);
   12.70 -by (fast_tac (!claset addSEs [SigmaE2]) 1);
   12.71 +by (Blast_tac 1);
   12.72  val lemma = result();
   12.73  
   12.74  goalw Trancl.thy [trancl_def]
   12.75      "!!r. r <= A Times A ==> r^+ <= A Times A";
   12.76 -by (fast_tac (!claset addSDs [lemma]) 1);
   12.77 +by (blast_tac (!claset addSDs [lemma]) 1);
   12.78  qed "trancl_subset_Sigma";
   12.79  
    13.1 --- a/src/HOL/Univ.ML	Fri Apr 04 11:18:19 1997 +0200
    13.2 +++ b/src/HOL/Univ.ML	Fri Apr 04 11:18:52 1997 +0200
    13.3 @@ -69,12 +69,12 @@
    13.4  (*** Introduction rules for Node ***)
    13.5  
    13.6  goalw Univ.thy [Node_def] "(%k. 0,a) : Node";
    13.7 -by (Fast_tac 1);
    13.8 +by (Blast_tac 1);
    13.9  qed "Node_K0_I";
   13.10  
   13.11  goalw Univ.thy [Node_def,Push_def]
   13.12      "!!p. p: Node ==> apfst (Push i) p : Node";
   13.13 -by (fast_tac (!claset addSIs [apfst_conv, nat_case_Suc RS trans]) 1);
   13.14 +by (blast_tac (!claset addSIs [apfst_conv, nat_case_Suc RS trans]) 1);
   13.15  qed "Node_Push_I";
   13.16  
   13.17  
   13.18 @@ -98,12 +98,12 @@
   13.19  (** Atomic nodes **)
   13.20  
   13.21  goalw Univ.thy [Atom_def, inj_def] "inj(Atom)";
   13.22 -by (fast_tac (!claset addSIs [Node_K0_I] addSDs [Abs_Node_inject]) 1);
   13.23 +by (blast_tac (!claset addSIs [Node_K0_I] addSDs [Abs_Node_inject]) 1);
   13.24  qed "inj_Atom";
   13.25  val Atom_inject = inj_Atom RS injD;
   13.26  
   13.27  goal Univ.thy "(Atom(a)=Atom(b)) = (a=b)";
   13.28 -by (fast_tac (!claset addSEs [Atom_inject]) 1);
   13.29 +by (blast_tac (!claset addSDs [Atom_inject]) 1);
   13.30  qed "Atom_Atom_eq";
   13.31  AddIffs [Atom_Atom_eq];
   13.32  
   13.33 @@ -142,14 +142,12 @@
   13.34  
   13.35  (** Injectiveness of Scons **)
   13.36  
   13.37 -val [major] = goalw Univ.thy [Scons_def] "M$N <= M'$N' ==> M<=M'";
   13.38 -by (cut_facts_tac [major] 1);
   13.39 -by (fast_tac (!claset addSEs [Push_Node_inject]) 1);
   13.40 +goalw Univ.thy [Scons_def] "!!M. M$N <= M'$N' ==> M<=M'";
   13.41 +by (blast_tac (!claset addSDs [Push_Node_inject]) 1);
   13.42  qed "Scons_inject_lemma1";
   13.43  
   13.44 -val [major] = goalw Univ.thy [Scons_def] "M$N <= M'$N' ==> N<=N'";
   13.45 -by (cut_facts_tac [major] 1);
   13.46 -by (fast_tac (!claset addSEs [Push_Node_inject]) 1);
   13.47 +goalw Univ.thy [Scons_def] "!!M. M$N <= M'$N' ==> N<=N'";
   13.48 +by (fast_tac (!claset addSDs [Push_Node_inject]) 1);
   13.49  qed "Scons_inject_lemma2";
   13.50  
   13.51  val [major] = goal Univ.thy "M$N = M'$N' ==> M=M'";
   13.52 @@ -171,7 +169,7 @@
   13.53  AddSDs [Scons_inject];
   13.54  
   13.55  goal Univ.thy "(M$N = M'$N') = (M=M' & N=N')";
   13.56 -by (fast_tac (!claset addSEs [Scons_inject]) 1);
   13.57 +by (blast_tac (!claset addSEs [Scons_inject]) 1);
   13.58  qed "Scons_Scons_eq";
   13.59  
   13.60  (*** Distinctness involving Leaf and Numb ***)
   13.61 @@ -244,7 +242,7 @@
   13.62  (*** ntrunc applied to the various node sets ***)
   13.63  
   13.64  goalw Univ.thy [ntrunc_def] "ntrunc 0 M = {}";
   13.65 -by (Fast_tac 1);
   13.66 +by (Blast_tac 1);
   13.67  qed "ntrunc_0";
   13.68  
   13.69  goalw Univ.thy [Atom_def,ntrunc_def] "ntrunc (Suc k) (Atom a) = Atom(a)";
   13.70 @@ -261,7 +259,7 @@
   13.71  
   13.72  goalw Univ.thy [Scons_def,ntrunc_def]
   13.73      "ntrunc (Suc k) (M$N) = ntrunc k M $ ntrunc k N";
   13.74 -by (safe_tac ((claset_of "Fun") addSIs [equalityI,imageI]));
   13.75 +by (safe_tac (!claset addSIs [equalityI, imageI]));
   13.76  by (REPEAT (stac ndepth_Push_Node 3 THEN etac Suc_mono 3));
   13.77  by (REPEAT (rtac Suc_less_SucD 1 THEN 
   13.78              rtac (ndepth_Push_Node RS subst) 1 THEN 
   13.79 @@ -273,7 +271,7 @@
   13.80  goalw Univ.thy [In0_def] "ntrunc (Suc 0) (In0 M) = {}";
   13.81  by (simp_tac (!simpset addsimps [ntrunc_Scons,ntrunc_0]) 1);
   13.82  by (rewtac Scons_def);
   13.83 -by (Fast_tac 1);
   13.84 +by (Blast_tac 1);
   13.85  qed "ntrunc_one_In0";
   13.86  
   13.87  goalw Univ.thy [In0_def]
   13.88 @@ -284,7 +282,7 @@
   13.89  goalw Univ.thy [In1_def] "ntrunc (Suc 0) (In1 M) = {}";
   13.90  by (simp_tac (!simpset addsimps [ntrunc_Scons,ntrunc_0]) 1);
   13.91  by (rewtac Scons_def);
   13.92 -by (Fast_tac 1);
   13.93 +by (Blast_tac 1);
   13.94  qed "ntrunc_one_In1";
   13.95  
   13.96  goalw Univ.thy [In1_def]
   13.97 @@ -321,11 +319,11 @@
   13.98  (*** Disjoint Sum ***)
   13.99  
  13.100  goalw Univ.thy [usum_def] "!!M. M:A ==> In0(M) : A<+>B";
  13.101 -by (Fast_tac 1);
  13.102 +by (Blast_tac 1);
  13.103  qed "usum_In0I";
  13.104  
  13.105  goalw Univ.thy [usum_def] "!!N. N:B ==> In1(N) : A<+>B";
  13.106 -by (Fast_tac 1);
  13.107 +by (Blast_tac 1);
  13.108  qed "usum_In1I";
  13.109  
  13.110  val major::prems = goalw Univ.thy [usum_def]
  13.111 @@ -363,12 +361,12 @@
  13.112  (*** proving equality of sets and functions using ntrunc ***)
  13.113  
  13.114  goalw Univ.thy [ntrunc_def] "ntrunc k M <= M";
  13.115 -by (Fast_tac 1);
  13.116 +by (Blast_tac 1);
  13.117  qed "ntrunc_subsetI";
  13.118  
  13.119  val [major] = goalw Univ.thy [ntrunc_def]
  13.120      "(!!k. ntrunc k M <= N) ==> M<=N";
  13.121 -by (fast_tac (!claset addIs [less_add_Suc1, less_add_Suc2, 
  13.122 +by (blast_tac (!claset addIs [less_add_Suc1, less_add_Suc2, 
  13.123                              major RS subsetD]) 1);
  13.124  qed "ntrunc_subsetD";
  13.125  
  13.126 @@ -390,15 +388,15 @@
  13.127  (*** Monotonicity ***)
  13.128  
  13.129  goalw Univ.thy [uprod_def] "!!A B. [| A<=A';  B<=B' |] ==> A<*>B <= A'<*>B'";
  13.130 -by (Fast_tac 1);
  13.131 +by (Blast_tac 1);
  13.132  qed "uprod_mono";
  13.133  
  13.134  goalw Univ.thy [usum_def] "!!A B. [| A<=A';  B<=B' |] ==> A<+>B <= A'<+>B'";
  13.135 -by (Fast_tac 1);
  13.136 +by (Blast_tac 1);
  13.137  qed "usum_mono";
  13.138  
  13.139  goalw Univ.thy [Scons_def] "!!M N. [| M<=M';  N<=N' |] ==> M$N <= M'$N'";
  13.140 -by (Fast_tac 1);
  13.141 +by (Blast_tac 1);
  13.142  qed "Scons_mono";
  13.143  
  13.144  goalw Univ.thy [In0_def] "!!M N. M<=N ==> In0(M) <= In0(N)";
  13.145 @@ -413,29 +411,29 @@
  13.146  (*** Split and Case ***)
  13.147  
  13.148  goalw Univ.thy [Split_def] "Split c (M$N) = c M N";
  13.149 -by (fast_tac (!claset addIs [select_equality]) 1);
  13.150 +by (blast_tac (!claset addIs [select_equality]) 1);
  13.151  qed "Split";
  13.152  
  13.153  goalw Univ.thy [Case_def] "Case c d (In0 M) = c(M)";
  13.154 -by (fast_tac (!claset addIs [select_equality]) 1);
  13.155 +by (blast_tac (!claset addIs [select_equality]) 1);
  13.156  qed "Case_In0";
  13.157  
  13.158  goalw Univ.thy [Case_def] "Case c d (In1 N) = d(N)";
  13.159 -by (fast_tac (!claset addIs [select_equality]) 1);
  13.160 +by (blast_tac (!claset addIs [select_equality]) 1);
  13.161  qed "Case_In1";
  13.162  
  13.163  (**** UN x. B(x) rules ****)
  13.164  
  13.165  goalw Univ.thy [ntrunc_def] "ntrunc k (UN x.f(x)) = (UN x. ntrunc k (f x))";
  13.166 -by (Fast_tac 1);
  13.167 +by (Blast_tac 1);
  13.168  qed "ntrunc_UN1";
  13.169  
  13.170  goalw Univ.thy [Scons_def] "(UN x.f(x)) $ M = (UN x. f(x) $ M)";
  13.171 -by (Fast_tac 1);
  13.172 +by (Blast_tac 1);
  13.173  qed "Scons_UN1_x";
  13.174  
  13.175  goalw Univ.thy [Scons_def] "M $ (UN x.f(x)) = (UN x. M $ f(x))";
  13.176 -by (Fast_tac 1);
  13.177 +by (Blast_tac 1);
  13.178  qed "Scons_UN1_y";
  13.179  
  13.180  goalw Univ.thy [In0_def] "In0(UN x.f(x)) = (UN x. In0(f(x)))";
  13.181 @@ -450,7 +448,7 @@
  13.182  (*** Equality : the diagonal relation ***)
  13.183  
  13.184  goalw Univ.thy [diag_def] "!!a A. [| a=b;  a:A |] ==> (a,b) : diag(A)";
  13.185 -by (Fast_tac 1);
  13.186 +by (Blast_tac 1);
  13.187  qed "diag_eqI";
  13.188  
  13.189  val diagI = refl RS diag_eqI |> standard;
  13.190 @@ -468,7 +466,7 @@
  13.191  
  13.192  goalw Univ.thy [dprod_def]
  13.193      "!!r s. [| (M,M'):r;  (N,N'):s |] ==> (M$N, M'$N') : r<**>s";
  13.194 -by (Fast_tac 1);
  13.195 +by (Blast_tac 1);
  13.196  qed "dprodI";
  13.197  
  13.198  (*The general elimination rule*)
  13.199 @@ -485,11 +483,11 @@
  13.200  (*** Equality for Disjoint Sum ***)
  13.201  
  13.202  goalw Univ.thy [dsum_def]  "!!r. (M,M'):r ==> (In0(M), In0(M')) : r<++>s";
  13.203 -by (Fast_tac 1);
  13.204 +by (Blast_tac 1);
  13.205  qed "dsum_In0I";
  13.206  
  13.207  goalw Univ.thy [dsum_def]  "!!r. (N,N'):s ==> (In1(N), In1(N')) : r<++>s";
  13.208 -by (Fast_tac 1);
  13.209 +by (Blast_tac 1);
  13.210  qed "dsum_In1I";
  13.211  
  13.212  val major::prems = goalw Univ.thy [dsum_def]
  13.213 @@ -510,22 +508,22 @@
  13.214  (*** Monotonicity ***)
  13.215  
  13.216  goal Univ.thy "!!r s. [| r<=r';  s<=s' |] ==> r<**>s <= r'<**>s'";
  13.217 -by (Fast_tac 1);
  13.218 +by (Blast_tac 1);
  13.219  qed "dprod_mono";
  13.220  
  13.221  goal Univ.thy "!!r s. [| r<=r';  s<=s' |] ==> r<++>s <= r'<++>s'";
  13.222 -by (Fast_tac 1);
  13.223 +by (Blast_tac 1);
  13.224  qed "dsum_mono";
  13.225  
  13.226  
  13.227  (*** Bounding theorems ***)
  13.228  
  13.229  goal Univ.thy "diag(A) <= A Times A";
  13.230 -by (Fast_tac 1);
  13.231 +by (Blast_tac 1);
  13.232  qed "diag_subset_Sigma";
  13.233  
  13.234  goal Univ.thy "((A Times B) <**> (C Times D)) <= (A<*>C) Times (B<*>D)";
  13.235 -by (Fast_tac 1);
  13.236 +by (Blast_tac 1);
  13.237  qed "dprod_Sigma";
  13.238  
  13.239  val dprod_subset_Sigma = [dprod_mono, dprod_Sigma] MRS subset_trans |>standard;
  13.240 @@ -535,11 +533,11 @@
  13.241      "(Sigma A B <**> Sigma C D) <= Sigma (A<*>C) (Split(%x y. B(x)<*>D(y)))";
  13.242  by (safe_tac (!claset));
  13.243  by (stac Split 1);
  13.244 -by (Fast_tac 1);
  13.245 +by (Blast_tac 1);
  13.246  qed "dprod_subset_Sigma2";
  13.247  
  13.248  goal Univ.thy "(A Times B <++> C Times D) <= (A<+>C) Times (B<+>D)";
  13.249 -by (Fast_tac 1);
  13.250 +by (Blast_tac 1);
  13.251  qed "dsum_Sigma";
  13.252  
  13.253  val dsum_subset_Sigma = [dsum_mono, dsum_Sigma] MRS subset_trans |> standard;
  13.254 @@ -548,15 +546,15 @@
  13.255  (*** Domain ***)
  13.256  
  13.257  goal Univ.thy "fst `` diag(A) = A";
  13.258 -by (Fast_tac 1);
  13.259 +by (Blast_tac 1);
  13.260  qed "fst_image_diag";
  13.261  
  13.262  goal Univ.thy "fst `` (r<**>s) = (fst``r) <*> (fst``s)";
  13.263 -by (Fast_tac 1);
  13.264 +by (Blast_tac 1);
  13.265  qed "fst_image_dprod";
  13.266  
  13.267  goal Univ.thy "fst `` (r<++>s) = (fst``r) <+> (fst``s)";
  13.268 -by (Fast_tac 1);
  13.269 +by (Blast_tac 1);
  13.270  qed "fst_image_dsum";
  13.271  
  13.272  Addsimps [fst_image_diag, fst_image_dprod, fst_image_dsum];
    14.1 --- a/src/HOL/equalities.ML	Fri Apr 04 11:18:19 1997 +0200
    14.2 +++ b/src/HOL/equalities.ML	Fri Apr 04 11:18:52 1997 +0200
    14.3 @@ -13,12 +13,12 @@
    14.4  section "{}";
    14.5  
    14.6  goal Set.thy "{x.False} = {}";
    14.7 -by (Fast_tac 1);
    14.8 +by (Blast_tac 1);
    14.9  qed "Collect_False_empty";
   14.10  Addsimps [Collect_False_empty];
   14.11  
   14.12  goal Set.thy "(A <= {}) = (A = {})";
   14.13 -by (Fast_tac 1);
   14.14 +by (Blast_tac 1);
   14.15  qed "subset_empty";
   14.16  Addsimps [subset_empty];
   14.17  
   14.18 @@ -26,7 +26,7 @@
   14.19  
   14.20  (*NOT SUITABLE FOR REWRITING since {a} == insert a {}*)
   14.21  goal Set.thy "insert a A = {a} Un A";
   14.22 -by (Fast_tac 1);
   14.23 +by (Blast_tac 1);
   14.24  qed "insert_is_Un";
   14.25  
   14.26  goal Set.thy "insert a A ~= {}";
   14.27 @@ -38,55 +38,55 @@
   14.28  Addsimps[empty_not_insert];
   14.29  
   14.30  goal Set.thy "!!a. a:A ==> insert a A = A";
   14.31 -by (Fast_tac 1);
   14.32 +by (Blast_tac 1);
   14.33  qed "insert_absorb";
   14.34  
   14.35  goal Set.thy "insert x (insert x A) = insert x A";
   14.36 -by (Fast_tac 1);
   14.37 +by (Blast_tac 1);
   14.38  qed "insert_absorb2";
   14.39  Addsimps [insert_absorb2];
   14.40  
   14.41  goal Set.thy "insert x (insert y A) = insert y (insert x A)";
   14.42 -by (Fast_tac 1);
   14.43 +by (Blast_tac 1);
   14.44  qed "insert_commute";
   14.45  
   14.46  goal Set.thy "(insert x A <= B) = (x:B & A <= B)";
   14.47 -by (Fast_tac 1);
   14.48 +by (Blast_tac 1);
   14.49  qed "insert_subset";
   14.50  Addsimps[insert_subset];
   14.51  
   14.52  (* use new B rather than (A-{a}) to avoid infinite unfolding *)
   14.53  goal Set.thy "!!a. a:A ==> ? B. A = insert a B & a ~: B";
   14.54  by (res_inst_tac [("x","A-{a}")] exI 1);
   14.55 -by (Fast_tac 1);
   14.56 +by (Blast_tac 1);
   14.57  qed "mk_disjoint_insert";
   14.58  
   14.59  goal Set.thy
   14.60      "!!A. A~={} ==> (UN x:A. insert a (B x)) = insert a (UN x:A. B x)";
   14.61 -by (Fast_tac 1);
   14.62 +by (Blast_tac 1);
   14.63  qed "UN_insert_distrib";
   14.64  
   14.65  goal Set.thy "(UN x. insert a (B x)) = insert a (UN x. B x)";
   14.66 -by (Fast_tac 1);
   14.67 +by (Blast_tac 1);
   14.68  qed "UN1_insert_distrib";
   14.69  
   14.70  section "``";
   14.71  
   14.72  goal Set.thy "f``{} = {}";
   14.73 -by (Fast_tac 1);
   14.74 +by (Blast_tac 1);
   14.75  qed "image_empty";
   14.76  Addsimps[image_empty];
   14.77  
   14.78  goal Set.thy "f``insert a B = insert (f a) (f``B)";
   14.79 -by (Fast_tac 1);
   14.80 +by (Blast_tac 1);
   14.81  qed "image_insert";
   14.82  Addsimps[image_insert];
   14.83  
   14.84  qed_goal "ball_image" Set.thy "(!y:F``S. P y) = (!x:S. P (F x))"
   14.85 - (fn _ => [Fast_tac 1]);
   14.86 + (fn _ => [Blast_tac 1]);
   14.87  
   14.88  goal Set.thy "!!x. x:A ==> insert (f x) (f``A) = f``A";
   14.89 -by (Fast_tac 1);
   14.90 +by (Blast_tac 1);
   14.91  qed "insert_image";
   14.92  Addsimps [insert_image];
   14.93  
   14.94 @@ -94,7 +94,7 @@
   14.95  "(%x. if P x then f x else g x) `` S                    \
   14.96  \ = (f `` ({x.x:S & P x})) Un (g `` ({x.x:S & ~(P x)}))";
   14.97  by (split_tac [expand_if] 1);
   14.98 -by (Fast_tac 1);
   14.99 +by (Blast_tac 1);
  14.100  qed "if_image_distrib";
  14.101  Addsimps[if_image_distrib];
  14.102  
  14.103 @@ -102,53 +102,53 @@
  14.104  section "range";
  14.105  
  14.106  qed_goal "ball_range" Set.thy "(!y:range f. P y) = (!x. P (f x))"
  14.107 - (fn _ => [Fast_tac 1]);
  14.108 + (fn _ => [Blast_tac 1]);
  14.109  
  14.110  qed_goalw "image_range" Set.thy [image_def]
  14.111   "f``range g = range (%x. f (g x))" 
  14.112 - (fn _ => [rtac Collect_cong 1, Fast_tac 1]);
  14.113 + (fn _ => [rtac Collect_cong 1, Blast_tac 1]);
  14.114  
  14.115  section "Int";
  14.116  
  14.117  goal Set.thy "A Int A = A";
  14.118 -by (Fast_tac 1);
  14.119 +by (Blast_tac 1);
  14.120  qed "Int_absorb";
  14.121  Addsimps[Int_absorb];
  14.122  
  14.123  goal Set.thy "A Int B  =  B Int A";
  14.124 -by (Fast_tac 1);
  14.125 +by (Blast_tac 1);
  14.126  qed "Int_commute";
  14.127  
  14.128  goal Set.thy "(A Int B) Int C  =  A Int (B Int C)";
  14.129 -by (Fast_tac 1);
  14.130 +by (Blast_tac 1);
  14.131  qed "Int_assoc";
  14.132  
  14.133  goal Set.thy "{} Int B = {}";
  14.134 -by (Fast_tac 1);
  14.135 +by (Blast_tac 1);
  14.136  qed "Int_empty_left";
  14.137  Addsimps[Int_empty_left];
  14.138  
  14.139  goal Set.thy "A Int {} = {}";
  14.140 -by (Fast_tac 1);
  14.141 +by (Blast_tac 1);
  14.142  qed "Int_empty_right";
  14.143  Addsimps[Int_empty_right];
  14.144  
  14.145  goal Set.thy "UNIV Int B = B";
  14.146 -by (Fast_tac 1);
  14.147 +by (Blast_tac 1);
  14.148  qed "Int_UNIV_left";
  14.149  Addsimps[Int_UNIV_left];
  14.150  
  14.151  goal Set.thy "A Int UNIV = A";
  14.152 -by (Fast_tac 1);
  14.153 +by (Blast_tac 1);
  14.154  qed "Int_UNIV_right";
  14.155  Addsimps[Int_UNIV_right];
  14.156  
  14.157  goal Set.thy "A Int (B Un C)  =  (A Int B) Un (A Int C)";
  14.158 -by (Fast_tac 1);
  14.159 +by (Blast_tac 1);
  14.160  qed "Int_Un_distrib";
  14.161  
  14.162  goal Set.thy "(B Un C) Int A =  (B Int A) Un (C Int A)";
  14.163 -by (Fast_tac 1);
  14.164 +by (Blast_tac 1);
  14.165  qed "Int_Un_distrib2";
  14.166  
  14.167  goal Set.thy "(A<=B) = (A Int B = A)";
  14.168 @@ -163,53 +163,53 @@
  14.169  section "Un";
  14.170  
  14.171  goal Set.thy "A Un A = A";
  14.172 -by (Fast_tac 1);
  14.173 +by (Blast_tac 1);
  14.174  qed "Un_absorb";
  14.175  Addsimps[Un_absorb];
  14.176  
  14.177  goal Set.thy "A Un B  =  B Un A";
  14.178 -by (Fast_tac 1);
  14.179 +by (Blast_tac 1);
  14.180  qed "Un_commute";
  14.181  
  14.182  goal Set.thy "(A Un B) Un C  =  A Un (B Un C)";
  14.183 -by (Fast_tac 1);
  14.184 +by (Blast_tac 1);
  14.185  qed "Un_assoc";
  14.186  
  14.187  goal Set.thy "{} Un B = B";
  14.188 -by (Fast_tac 1);
  14.189 +by (Blast_tac 1);
  14.190  qed "Un_empty_left";
  14.191  Addsimps[Un_empty_left];
  14.192  
  14.193  goal Set.thy "A Un {} = A";
  14.194 -by (Fast_tac 1);
  14.195 +by (Blast_tac 1);
  14.196  qed "Un_empty_right";
  14.197  Addsimps[Un_empty_right];
  14.198  
  14.199  goal Set.thy "UNIV Un B = UNIV";
  14.200 -by (Fast_tac 1);
  14.201 +by (Blast_tac 1);
  14.202  qed "Un_UNIV_left";
  14.203  Addsimps[Un_UNIV_left];
  14.204  
  14.205  goal Set.thy "A Un UNIV = UNIV";
  14.206 -by (Fast_tac 1);
  14.207 +by (Blast_tac 1);
  14.208  qed "Un_UNIV_right";
  14.209  Addsimps[Un_UNIV_right];
  14.210  
  14.211  goal Set.thy "(insert a B) Un C = insert a (B Un C)";
  14.212 -by (Fast_tac 1);
  14.213 +by (Blast_tac 1);
  14.214  qed "Un_insert_left";
  14.215  
  14.216  goal Set.thy "A Un (insert a B) = insert a (A Un B)";
  14.217 -by (Fast_tac 1);
  14.218 +by (Blast_tac 1);
  14.219  qed "Un_insert_right";
  14.220  
  14.221  goal Set.thy "(A Int B) Un C  =  (A Un C) Int (B Un C)";
  14.222 -by (Fast_tac 1);
  14.223 +by (Blast_tac 1);
  14.224  qed "Un_Int_distrib";
  14.225  
  14.226  goal Set.thy
  14.227   "(A Int B) Un (B Int C) Un (C Int A) = (A Un B) Int (B Un C) Int (C Un A)";
  14.228 -by (Fast_tac 1);
  14.229 +by (Blast_tac 1);
  14.230  qed "Un_Int_crazy";
  14.231  
  14.232  goal Set.thy "(A<=B) = (A Un B = B)";
  14.233 @@ -217,7 +217,7 @@
  14.234  qed "subset_Un_eq";
  14.235  
  14.236  goal Set.thy "(A <= insert b C) = (A <= C | b:A & A-{b} <= C)";
  14.237 -by (Fast_tac 1);
  14.238 +by (Blast_tac 1);
  14.239  qed "subset_insert_iff";
  14.240  
  14.241  goal Set.thy "(A Un B = {}) = (A = {} & B = {})";
  14.242 @@ -228,33 +228,33 @@
  14.243  section "Compl";
  14.244  
  14.245  goal Set.thy "A Int Compl(A) = {}";
  14.246 -by (Fast_tac 1);
  14.247 +by (Blast_tac 1);
  14.248  qed "Compl_disjoint";
  14.249  Addsimps[Compl_disjoint];
  14.250  
  14.251  goal Set.thy "A Un Compl(A) = UNIV";
  14.252 -by (Fast_tac 1);
  14.253 +by (Blast_tac 1);
  14.254  qed "Compl_partition";
  14.255  
  14.256  goal Set.thy "Compl(Compl(A)) = A";
  14.257 -by (Fast_tac 1);
  14.258 +by (Blast_tac 1);
  14.259  qed "double_complement";
  14.260  Addsimps[double_complement];
  14.261  
  14.262  goal Set.thy "Compl(A Un B) = Compl(A) Int Compl(B)";
  14.263 -by (Fast_tac 1);
  14.264 +by (Blast_tac 1);
  14.265  qed "Compl_Un";
  14.266  
  14.267  goal Set.thy "Compl(A Int B) = Compl(A) Un Compl(B)";
  14.268 -by (Fast_tac 1);
  14.269 +by (Blast_tac 1);
  14.270  qed "Compl_Int";
  14.271  
  14.272  goal Set.thy "Compl(UN x:A. B(x)) = (INT x:A. Compl(B(x)))";
  14.273 -by (Fast_tac 1);
  14.274 +by (Blast_tac 1);
  14.275  qed "Compl_UN";
  14.276  
  14.277  goal Set.thy "Compl(INT x:A. B(x)) = (UN x:A. Compl(B(x)))";
  14.278 -by (Fast_tac 1);
  14.279 +by (Blast_tac 1);
  14.280  qed "Compl_INT";
  14.281  
  14.282  (*Halmos, Naive Set Theory, page 16.*)
  14.283 @@ -267,27 +267,27 @@
  14.284  section "Union";
  14.285  
  14.286  goal Set.thy "Union({}) = {}";
  14.287 -by (Fast_tac 1);
  14.288 +by (Blast_tac 1);
  14.289  qed "Union_empty";
  14.290  Addsimps[Union_empty];
  14.291  
  14.292  goal Set.thy "Union(UNIV) = UNIV";
  14.293 -by (Fast_tac 1);
  14.294 +by (Blast_tac 1);
  14.295  qed "Union_UNIV";
  14.296  Addsimps[Union_UNIV];
  14.297  
  14.298  goal Set.thy "Union(insert a B) = a Un Union(B)";
  14.299 -by (Fast_tac 1);
  14.300 +by (Blast_tac 1);
  14.301  qed "Union_insert";
  14.302  Addsimps[Union_insert];
  14.303  
  14.304  goal Set.thy "Union(A Un B) = Union(A) Un Union(B)";
  14.305 -by (Fast_tac 1);
  14.306 +by (Blast_tac 1);
  14.307  qed "Union_Un_distrib";
  14.308  Addsimps[Union_Un_distrib];
  14.309  
  14.310  goal Set.thy "Union(A Int B) <= Union(A) Int Union(B)";
  14.311 -by (Fast_tac 1);
  14.312 +by (Blast_tac 1);
  14.313  qed "Union_Int_subset";
  14.314  
  14.315  val prems = goal Set.thy
  14.316 @@ -298,26 +298,26 @@
  14.317  section "Inter";
  14.318  
  14.319  goal Set.thy "Inter({}) = UNIV";
  14.320 -by (Fast_tac 1);
  14.321 +by (Blast_tac 1);
  14.322  qed "Inter_empty";
  14.323  Addsimps[Inter_empty];
  14.324  
  14.325  goal Set.thy "Inter(UNIV) = {}";
  14.326 -by (Fast_tac 1);
  14.327 +by (Blast_tac 1);
  14.328  qed "Inter_UNIV";
  14.329  Addsimps[Inter_UNIV];
  14.330  
  14.331  goal Set.thy "Inter(insert a B) = a Int Inter(B)";
  14.332 -by (Fast_tac 1);
  14.333 +by (Blast_tac 1);
  14.334  qed "Inter_insert";
  14.335  Addsimps[Inter_insert];
  14.336  
  14.337  goal Set.thy "Inter(A) Un Inter(B) <= Inter(A Int B)";
  14.338 -by (Fast_tac 1);
  14.339 +by (Blast_tac 1);
  14.340  qed "Inter_Un_subset";
  14.341  
  14.342  goal Set.thy "Inter(A Un B) = Inter(A) Int Inter(B)";
  14.343 -by (best_tac (!claset) 1);
  14.344 +by (Blast_tac 1);
  14.345  qed "Inter_Un_distrib";
  14.346  
  14.347  section "UN and INT";
  14.348 @@ -325,134 +325,134 @@
  14.349  (*Basic identities*)
  14.350  
  14.351  goal Set.thy "(UN x:{}. B x) = {}";
  14.352 -by (Fast_tac 1);
  14.353 +by (Blast_tac 1);
  14.354  qed "UN_empty";
  14.355  Addsimps[UN_empty];
  14.356  
  14.357  goal Set.thy "(UN x:UNIV. B x) = (UN x. B x)";
  14.358 -by (Fast_tac 1);
  14.359 +by (Blast_tac 1);
  14.360  qed "UN_UNIV";
  14.361  Addsimps[UN_UNIV];
  14.362  
  14.363  goal Set.thy "(INT x:{}. B x) = UNIV";
  14.364 -by (Fast_tac 1);
  14.365 +by (Blast_tac 1);
  14.366  qed "INT_empty";
  14.367  Addsimps[INT_empty];
  14.368  
  14.369  goal Set.thy "(INT x:UNIV. B x) = (INT x. B x)";
  14.370 -by (Fast_tac 1);
  14.371 +by (Blast_tac 1);
  14.372  qed "INT_UNIV";
  14.373  Addsimps[INT_UNIV];
  14.374  
  14.375  goal Set.thy "(UN x:insert a A. B x) = B a Un UNION A B";
  14.376 -by (Fast_tac 1);
  14.377 +by (Blast_tac 1);
  14.378  qed "UN_insert";
  14.379  Addsimps[UN_insert];
  14.380  
  14.381  goal Set.thy "(INT x:insert a A. B x) = B a Int INTER A B";
  14.382 -by (Fast_tac 1);
  14.383 +by (Blast_tac 1);
  14.384  qed "INT_insert";
  14.385  Addsimps[INT_insert];
  14.386  
  14.387  goal Set.thy
  14.388      "!!A. A~={} ==> (INT x:A. insert a (B x)) = insert a (INT x:A. B x)";
  14.389 -by (Fast_tac 1);
  14.390 +by (Blast_tac 1);
  14.391  qed "INT_insert_distrib";
  14.392  
  14.393  goal Set.thy "(INT x. insert a (B x)) = insert a (INT x. B x)";
  14.394 -by (Fast_tac 1);
  14.395 +by (Blast_tac 1);
  14.396  qed "INT1_insert_distrib";
  14.397  
  14.398  goal Set.thy "Union(range(f)) = (UN x.f(x))";
  14.399 -by (Fast_tac 1);
  14.400 +by (Blast_tac 1);
  14.401  qed "Union_range_eq";
  14.402  
  14.403  goal Set.thy "Inter(range(f)) = (INT x.f(x))";
  14.404 -by (Fast_tac 1);
  14.405 +by (Blast_tac 1);
  14.406  qed "Inter_range_eq";
  14.407  
  14.408  goal Set.thy "Union(B``A) = (UN x:A. B(x))";
  14.409 -by (Fast_tac 1);
  14.410 +by (Blast_tac 1);
  14.411  qed "Union_image_eq";
  14.412  
  14.413  goal Set.thy "Inter(B``A) = (INT x:A. B(x))";
  14.414 -by (Fast_tac 1);
  14.415 +by (Blast_tac 1);
  14.416  qed "Inter_image_eq";
  14.417  
  14.418  goal Set.thy "!!A. a: A ==> (UN y:A. c) = c";
  14.419 -by (Fast_tac 1);
  14.420 +by (Blast_tac 1);
  14.421  qed "UN_constant";
  14.422  
  14.423  goal Set.thy "!!A. a: A ==> (INT y:A. c) = c";
  14.424 -by (Fast_tac 1);
  14.425 +by (Blast_tac 1);
  14.426  qed "INT_constant";
  14.427  
  14.428  goal Set.thy "(UN x.B) = B";
  14.429 -by (Fast_tac 1);
  14.430 +by (Blast_tac 1);
  14.431  qed "UN1_constant";
  14.432  Addsimps[UN1_constant];
  14.433  
  14.434  goal Set.thy "(INT x.B) = B";
  14.435 -by (Fast_tac 1);
  14.436 +by (Blast_tac 1);
  14.437  qed "INT1_constant";
  14.438  Addsimps[INT1_constant];
  14.439  
  14.440  goal Set.thy "(UN x:A. B(x)) = Union({Y. ? x:A. Y=B(x)})";
  14.441 -by (Fast_tac 1);
  14.442 +by (Blast_tac 1);
  14.443  qed "UN_eq";
  14.444  
  14.445  (*Look: it has an EXISTENTIAL quantifier*)
  14.446  goal Set.thy "(INT x:A. B(x)) = Inter({Y. ? x:A. Y=B(x)})";
  14.447 -by (Fast_tac 1);
  14.448 +by (Blast_tac 1);
  14.449  qed "INT_eq";
  14.450  
  14.451  (*Distributive laws...*)
  14.452  
  14.453  goal Set.thy "A Int Union(B) = (UN C:B. A Int C)";
  14.454 -by (Fast_tac 1);
  14.455 +by (Blast_tac 1);
  14.456  qed "Int_Union";
  14.457  
  14.458  (* Devlin, Fundamentals of Contemporary Set Theory, page 12, exercise 5: 
  14.459     Union of a family of unions **)
  14.460  goal Set.thy "(UN x:C. A(x) Un B(x)) = Union(A``C)  Un  Union(B``C)";
  14.461 -by (Fast_tac 1);
  14.462 +by (Blast_tac 1);
  14.463  qed "Un_Union_image";
  14.464  
  14.465  (*Equivalent version*)
  14.466  goal Set.thy "(UN i:I. A(i) Un B(i)) = (UN i:I. A(i))  Un  (UN i:I. B(i))";
  14.467 -by (Fast_tac 1);
  14.468 +by (Blast_tac 1);
  14.469  qed "UN_Un_distrib";
  14.470  
  14.471  goal Set.thy "A Un Inter(B) = (INT C:B. A Un C)";
  14.472 -by (Fast_tac 1);
  14.473 +by (Blast_tac 1);
  14.474  qed "Un_Inter";
  14.475  
  14.476  goal Set.thy "(INT x:C. A(x) Int B(x)) = Inter(A``C) Int Inter(B``C)";
  14.477 -by (best_tac (!claset) 1);
  14.478 +by (Blast_tac 1);
  14.479  qed "Int_Inter_image";
  14.480  
  14.481  (*Equivalent version*)
  14.482  goal Set.thy "(INT i:I. A(i) Int B(i)) = (INT i:I. A(i)) Int (INT i:I. B(i))";
  14.483 -by (Fast_tac 1);
  14.484 +by (Blast_tac 1);
  14.485  qed "INT_Int_distrib";
  14.486  
  14.487  (*Halmos, Naive Set Theory, page 35.*)
  14.488  goal Set.thy "B Int (UN i:I. A(i)) = (UN i:I. B Int A(i))";
  14.489 -by (Fast_tac 1);
  14.490 +by (Blast_tac 1);
  14.491  qed "Int_UN_distrib";
  14.492  
  14.493  goal Set.thy "B Un (INT i:I. A(i)) = (INT i:I. B Un A(i))";
  14.494 -by (Fast_tac 1);
  14.495 +by (Blast_tac 1);
  14.496  qed "Un_INT_distrib";
  14.497  
  14.498  goal Set.thy
  14.499      "(UN i:I. A(i)) Int (UN j:J. B(j)) = (UN i:I. UN j:J. A(i) Int B(j))";
  14.500 -by (Fast_tac 1);
  14.501 +by (Blast_tac 1);
  14.502  qed "Int_UN_distrib2";
  14.503  
  14.504  goal Set.thy
  14.505      "(INT i:I. A(i)) Un (INT j:J. B(j)) = (INT i:I. INT j:J. A(i) Un B(j))";
  14.506 -by (Fast_tac 1);
  14.507 +by (Blast_tac 1);
  14.508  qed "Un_INT_distrib2";
  14.509  
  14.510  
  14.511 @@ -462,58 +462,58 @@
  14.512      body and (b) there are no similar rules for Int. **)
  14.513  
  14.514  goal Set.thy "(ALL x:A Un B.P x) = ((ALL x:A.P x) & (ALL x:B.P x))";
  14.515 -by (Fast_tac 1);
  14.516 +by (Blast_tac 1);
  14.517  qed "ball_Un";
  14.518  
  14.519  goal Set.thy "(EX x:A Un B.P x) = ((EX x:A.P x) | (EX x:B.P x))";
  14.520 -by (Fast_tac 1);
  14.521 +by (Blast_tac 1);
  14.522  qed "bex_Un";
  14.523  
  14.524  
  14.525  section "-";
  14.526  
  14.527  goal Set.thy "A-A = {}";
  14.528 -by (Fast_tac 1);
  14.529 +by (Blast_tac 1);
  14.530  qed "Diff_cancel";
  14.531  Addsimps[Diff_cancel];
  14.532  
  14.533  goal Set.thy "{}-A = {}";
  14.534 -by (Fast_tac 1);
  14.535 +by (Blast_tac 1);
  14.536  qed "empty_Diff";
  14.537  Addsimps[empty_Diff];
  14.538  
  14.539  goal Set.thy "A-{} = A";
  14.540 -by (Fast_tac 1);
  14.541 +by (Blast_tac 1);
  14.542  qed "Diff_empty";
  14.543  Addsimps[Diff_empty];
  14.544  
  14.545  goal Set.thy "A-UNIV = {}";
  14.546 -by (Fast_tac 1);
  14.547 +by (Blast_tac 1);
  14.548  qed "Diff_UNIV";
  14.549  Addsimps[Diff_UNIV];
  14.550  
  14.551  goal Set.thy "!!x. x~:A ==> A - insert x B = A-B";
  14.552 -by (Fast_tac 1);
  14.553 +by (Blast_tac 1);
  14.554  qed "Diff_insert0";
  14.555  Addsimps [Diff_insert0];
  14.556  
  14.557  (*NOT SUITABLE FOR REWRITING since {a} == insert a 0*)
  14.558  goal Set.thy "A - insert a B = A - B - {a}";
  14.559 -by (Fast_tac 1);
  14.560 +by (Blast_tac 1);
  14.561  qed "Diff_insert";
  14.562  
  14.563  (*NOT SUITABLE FOR REWRITING since {a} == insert a 0*)
  14.564  goal Set.thy "A - insert a B = A - {a} - B";
  14.565 -by (Fast_tac 1);
  14.566 +by (Blast_tac 1);
  14.567  qed "Diff_insert2";
  14.568  
  14.569  goal Set.thy "insert x A - B = (if x:B then A-B else insert x (A-B))";
  14.570  by (simp_tac (!simpset setloop split_tac[expand_if]) 1);
  14.571 -by (Fast_tac 1);
  14.572 +by (Blast_tac 1);
  14.573  qed "insert_Diff_if";
  14.574  
  14.575  goal Set.thy "!!x. x:B ==> insert x A - B = A-B";
  14.576 -by (Fast_tac 1);
  14.577 +by (Blast_tac 1);
  14.578  qed "insert_Diff1";
  14.579  Addsimps [insert_Diff1];
  14.580  
  14.581 @@ -522,24 +522,24 @@
  14.582  qed "insert_Diff";
  14.583  
  14.584  goal Set.thy "A Int (B-A) = {}";
  14.585 -by (Fast_tac 1);
  14.586 +by (Blast_tac 1);
  14.587  qed "Diff_disjoint";
  14.588  Addsimps[Diff_disjoint];
  14.589  
  14.590  goal Set.thy "!!A. A<=B ==> A Un (B-A) = B";
  14.591 -by (Fast_tac 1);
  14.592 +by (Blast_tac 1);
  14.593  qed "Diff_partition";
  14.594  
  14.595  goal Set.thy "!!A. [| A<=B; B<= C |] ==> (B - (C - A)) = (A :: 'a set)";
  14.596 -by (Fast_tac 1);
  14.597 +by (Blast_tac 1);
  14.598  qed "double_diff";
  14.599  
  14.600  goal Set.thy "A - (B Un C) = (A-B) Int (A-C)";
  14.601 -by (Fast_tac 1);
  14.602 +by (Blast_tac 1);
  14.603  qed "Diff_Un";
  14.604  
  14.605  goal Set.thy "A - (B Int C) = (A-B) Un (A-C)";
  14.606 -by (Fast_tac 1);
  14.607 +by (Blast_tac 1);
  14.608  qed "Diff_Int";
  14.609  
  14.610  Addsimps[subset_UNIV, empty_subsetI, subset_refl];
  14.611 @@ -547,7 +547,7 @@
  14.612  
  14.613  (** Miniscoping: pushing in big Unions and Intersections **)
  14.614  local
  14.615 -  fun prover s = prove_goal Set.thy s (fn _ => [Fast_tac 1])
  14.616 +  fun prover s = prove_goal Set.thy s (fn _ => [Blast_tac 1])
  14.617  in
  14.618  val UN1_simps = map prover 
  14.619                  ["(UN x. insert a (B x)) = insert a (UN x. B x)",
    15.1 --- a/src/HOL/ex/Mutil.ML	Fri Apr 04 11:18:19 1997 +0200
    15.2 +++ b/src/HOL/ex/Mutil.ML	Fri Apr 04 11:18:52 1997 +0200
    15.3 @@ -16,8 +16,8 @@
    15.4  \              u: tiling A --> t <= Compl u --> t Un u : tiling A";
    15.5  by (etac tiling.induct 1);
    15.6  by (Simp_tac 1);
    15.7 -by (fast_tac (!claset addIs tiling.intrs
    15.8 -                      addss (!simpset addsimps [Un_assoc])) 1);
    15.9 +by (simp_tac (!simpset addsimps [Un_assoc]) 1);
   15.10 +by (blast_tac (!claset addIs tiling.intrs) 1);
   15.11  qed_spec_mp "tiling_UnI";
   15.12  
   15.13  
   15.14 @@ -29,19 +29,19 @@
   15.15  goal thy "ALL i. (i: below k) = (i<k)";
   15.16  by (nat_ind_tac "k" 1);
   15.17  by (ALLGOALS (asm_simp_tac (!simpset addsimps [less_Suc_eq])));
   15.18 -by (Fast_tac 1);
   15.19 +by (Blast_tac 1);
   15.20  qed_spec_mp "below_less_iff";
   15.21  
   15.22  Addsimps [below_less_iff];
   15.23  
   15.24  goal thy "below(Suc n) Times B = ({n} Times B) Un ((below n) Times B)";
   15.25  by (Simp_tac 1);
   15.26 -by (Fast_tac 1);
   15.27 +by (Blast_tac 1);
   15.28  qed "Sigma_Suc1";
   15.29  
   15.30  goal thy "A Times below(Suc n) = (A Times {n}) Un (A Times (below n))";
   15.31  by (Simp_tac 1);
   15.32 -by (Fast_tac 1);
   15.33 +by (Blast_tac 1);
   15.34  qed "Sigma_Suc2";
   15.35  
   15.36  (*Deletion is essential to allow use of Sigma_Suc1,2*)
   15.37 @@ -55,17 +55,17 @@
   15.38  by (subgoal_tac    (*seems the easiest way of turning one to the other*)
   15.39      "({i} Times {Suc(n1+n1)}) Un ({i} Times {n1+n1}) = \
   15.40  \    {(i, n1+n1), (i, Suc(n1+n1))}" 1);
   15.41 -by (Fast_tac 2);
   15.42 +by (Blast_tac 2);
   15.43  by (asm_simp_tac (!simpset addsimps [domino.horiz]) 1);
   15.44 -by (fast_tac (!claset addEs  [less_asym]
   15.45 -                      addSDs [below_less_iff RS iffD1]) 1);
   15.46 +by (blast_tac (!claset addEs  [less_irrefl, less_asym]
   15.47 +                       addSDs [below_less_iff RS iffD1]) 1);
   15.48  qed "dominoes_tile_row";
   15.49  
   15.50  goal thy "(below m) Times below(n + n) : tiling domino";
   15.51  by (nat_ind_tac "m" 1);
   15.52  by (ALLGOALS (asm_simp_tac (!simpset addsimps [Sigma_Suc1])));
   15.53 -by (fast_tac (!claset addIs [equalityI, tiling_UnI, dominoes_tile_row] 
   15.54 -                      addEs [below_less_iff RS iffD1 RS less_irrefl]) 1);
   15.55 +by (blast_tac (!claset addSIs [tiling_UnI, dominoes_tile_row]
   15.56 +                      addSEs [below_less_iff RS iffD1 RS less_irrefl]) 1);
   15.57  qed "dominoes_tile_matrix";
   15.58  
   15.59  
   15.60 @@ -83,11 +83,11 @@
   15.61  bind_thm("finite_evnodd", evnodd_subset RS finite_subset);
   15.62  
   15.63  goalw thy [evnodd_def] "evnodd (A Un B) b = evnodd A b Un evnodd B b";
   15.64 -by (Fast_tac 1);
   15.65 +by (Blast_tac 1);
   15.66  qed "evnodd_Un";
   15.67  
   15.68  goalw thy [evnodd_def] "evnodd (A - B) b = evnodd A b - evnodd B b";
   15.69 -by (Fast_tac 1);
   15.70 +by (Blast_tac 1);
   15.71  qed "evnodd_Diff";
   15.72  
   15.73  goalw thy [evnodd_def] "evnodd {} b = {}";
   15.74 @@ -113,12 +113,12 @@
   15.75  by (REPEAT (asm_full_simp_tac (!simpset addsimps
   15.76                            [less_Suc_eq, evnodd_insert, evnodd_empty, mod_Suc] 
   15.77                            setloop split_tac [expand_if]) 1
   15.78 -           THEN Fast_tac 1));
   15.79 +           THEN Blast_tac 1));
   15.80  qed "domino_singleton";
   15.81  
   15.82  goal thy "!!d. d:domino ==> finite d";
   15.83 -by (fast_tac (!claset addSIs [finite_insertI, finite_emptyI] 
   15.84 -                      addEs [domino.elim]) 1);
   15.85 +by (blast_tac (!claset addSIs [finite_insertI, finite_emptyI] 
   15.86 +                      addSEs [domino.elim]) 1);
   15.87  qed "domino_finite";
   15.88  
   15.89  
   15.90 @@ -127,7 +127,7 @@
   15.91  goal thy "!!t. t:tiling domino ==> finite t";
   15.92  by (eresolve_tac [tiling.induct] 1);
   15.93  by (rtac finite_emptyI 1);
   15.94 -by (fast_tac (!claset addIs [domino_finite, finite_UnI]) 1);
   15.95 +by (blast_tac (!claset addSIs [finite_UnI] addIs [domino_finite]) 1);
   15.96  qed "tiling_domino_finite";
   15.97  
   15.98  goal thy "!!t. t: tiling domino ==> card(evnodd t 0) = card(evnodd t 1)";
   15.99 @@ -143,7 +143,7 @@
  15.100                                       tiling_domino_finite,
  15.101                                       evnodd_subset RS finite_subset,
  15.102                                       card_insert_disjoint]) 1);
  15.103 -by (fast_tac (!claset addSDs [evnodd_subset RS subsetD] addEs [equalityE]) 1);
  15.104 +by (blast_tac (!claset addSDs [evnodd_subset RS subsetD] addEs [equalityE]) 1);
  15.105  qed "tiling_domino_0_1";
  15.106  
  15.107  goal thy "!!m n. [| t = below(Suc m + Suc m) Times below(Suc n + Suc n);   \
    16.1 --- a/src/HOL/ex/cla.ML	Fri Apr 04 11:18:19 1997 +0200
    16.2 +++ b/src/HOL/ex/cla.ML	Fri Apr 04 11:18:52 1997 +0200
    16.3 @@ -13,17 +13,17 @@
    16.4  set_current_thy "HOL";  (*Boosts efficiency by omitting redundant rules*)
    16.5  
    16.6  goal HOL.thy "(P --> Q | R) --> (P-->Q) | (P-->R)";
    16.7 -by (Fast_tac 1);
    16.8 +by (Blast_tac 1);
    16.9  result();
   16.10  
   16.11  (*If and only if*)
   16.12  
   16.13  goal HOL.thy "(P=Q) = (Q=P::bool)";
   16.14 -by (Fast_tac 1);
   16.15 +by (Blast_tac 1);
   16.16  result();
   16.17  
   16.18  goal HOL.thy "~ (P = (~P))";
   16.19 -by (Fast_tac 1);
   16.20 +by (Blast_tac 1);
   16.21  result();
   16.22  
   16.23  
   16.24 @@ -40,112 +40,112 @@
   16.25  writeln"Pelletier's examples";
   16.26  (*1*)
   16.27  goal HOL.thy "(P-->Q)  =  (~Q --> ~P)";
   16.28 -by (Fast_tac 1);
   16.29 +by (Blast_tac 1);
   16.30  result();
   16.31  
   16.32  (*2*)
   16.33  goal HOL.thy "(~ ~ P) =  P";
   16.34 -by (Fast_tac 1);
   16.35 +by (Blast_tac 1);
   16.36  result();
   16.37  
   16.38  (*3*)
   16.39  goal HOL.thy "~(P-->Q) --> (Q-->P)";
   16.40 -by (Fast_tac 1);
   16.41 +by (Blast_tac 1);
   16.42  result();
   16.43  
   16.44  (*4*)
   16.45  goal HOL.thy "(~P-->Q)  =  (~Q --> P)";
   16.46 -by (Fast_tac 1);
   16.47 +by (Blast_tac 1);
   16.48  result();
   16.49  
   16.50  (*5*)
   16.51  goal HOL.thy "((P|Q)-->(P|R)) --> (P|(Q-->R))";
   16.52 -by (Fast_tac 1);
   16.53 +by (Blast_tac 1);
   16.54  result();
   16.55  
   16.56  (*6*)
   16.57  goal HOL.thy "P | ~ P";
   16.58 -by (Fast_tac 1);
   16.59 +by (Blast_tac 1);
   16.60  result();
   16.61  
   16.62  (*7*)
   16.63  goal HOL.thy "P | ~ ~ ~ P";
   16.64 -by (Fast_tac 1);
   16.65 +by (Blast_tac 1);
   16.66  result();
   16.67  
   16.68  (*8.  Peirce's law*)
   16.69  goal HOL.thy "((P-->Q) --> P)  -->  P";
   16.70 -by (Fast_tac 1);
   16.71 +by (Blast_tac 1);
   16.72  result();
   16.73  
   16.74  (*9*)
   16.75  goal HOL.thy "((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)";
   16.76 -by (Fast_tac 1);
   16.77 +by (Blast_tac 1);
   16.78  result();
   16.79  
   16.80  (*10*)
   16.81  goal HOL.thy "(Q-->R) & (R-->P&Q) & (P-->Q|R) --> (P=Q)";
   16.82 -by (Fast_tac 1);
   16.83 +by (Blast_tac 1);
   16.84  result();
   16.85  
   16.86  (*11.  Proved in each direction (incorrectly, says Pelletier!!)  *)
   16.87  goal HOL.thy "P=P::bool";
   16.88 -by (Fast_tac 1);
   16.89 +by (Blast_tac 1);
   16.90  result();
   16.91  
   16.92  (*12.  "Dijkstra's law"*)
   16.93  goal HOL.thy "((P = Q) = R) = (P = (Q = R))";
   16.94 -by (Fast_tac 1);
   16.95 +by (Blast_tac 1);
   16.96  result();
   16.97  
   16.98  (*13.  Distributive law*)
   16.99  goal HOL.thy "(P | (Q & R)) = ((P | Q) & (P | R))";
  16.100 -by (Fast_tac 1);
  16.101 +by (Blast_tac 1);
  16.102  result();
  16.103  
  16.104  (*14*)
  16.105  goal HOL.thy "(P = Q) = ((Q | ~P) & (~Q|P))";
  16.106 -by (Fast_tac 1);
  16.107 +by (Blast_tac 1);
  16.108  result();
  16.109  
  16.110  (*15*)
  16.111  goal HOL.thy "(P --> Q) = (~P | Q)";
  16.112 -by (Fast_tac 1);
  16.113 +by (Blast_tac 1);
  16.114  result();
  16.115  
  16.116  (*16*)
  16.117  goal HOL.thy "(P-->Q) | (Q-->P)";
  16.118 -by (Fast_tac 1);
  16.119 +by (Blast_tac 1);
  16.120  result();
  16.121  
  16.122  (*17*)
  16.123  goal HOL.thy "((P & (Q-->R))-->S)  =  ((~P | Q | S) & (~P | ~R | S))";
  16.124 -by (Fast_tac 1);
  16.125 +by (Blast_tac 1);
  16.126  result();
  16.127  
  16.128  writeln"Classical Logic: examples with quantifiers";
  16.129  
  16.130  goal HOL.thy "(! x. P(x) & Q(x)) = ((! x. P(x)) & (! x. Q(x)))";
  16.131 -by (Fast_tac 1);
  16.132 +by (Blast_tac 1);
  16.133  result(); 
  16.134  
  16.135  goal HOL.thy "(? x. P-->Q(x))  =  (P --> (? x.Q(x)))";
  16.136 -by (Fast_tac 1);
  16.137 +by (Blast_tac 1);
  16.138  result(); 
  16.139  
  16.140  goal HOL.thy "(? x.P(x)-->Q) = ((! x.P(x)) --> Q)";
  16.141 -by (Fast_tac 1);
  16.142 +by (Blast_tac 1);
  16.143  result(); 
  16.144  
  16.145  goal HOL.thy "((! x.P(x)) | Q)  =  (! x. P(x) | Q)";
  16.146 -by (Fast_tac 1);
  16.147 +by (Blast_tac 1);
  16.148  result(); 
  16.149  
  16.150  (*From Wishnu Prasetya*)
  16.151  goal HOL.thy
  16.152     "(!s. q(s) --> r(s)) & ~r(s) & (!s. ~r(s) & ~q(s) --> p(t) | q(t)) \
  16.153  \   --> p(t) | r(t)";
  16.154 -by (Fast_tac 1);
  16.155 +by (Blast_tac 1);
  16.156  result(); 
  16.157  
  16.158  
  16.159 @@ -153,60 +153,60 @@
  16.160  
  16.161  (*Needs multiple instantiation of the quantifier.*)
  16.162  goal HOL.thy "(! x. P(x)-->P(f(x)))  &  P(d)-->P(f(f(f(d))))";
  16.163 -by (Deepen_tac 1 1);
  16.164 +by (Blast_tac 1);
  16.165  result();
  16.166  
  16.167  (*Needs double instantiation of the quantifier*)
  16.168  goal HOL.thy "? x. P(x) --> P(a) & P(b)";
  16.169 -by (Deepen_tac 1 1);
  16.170 +by (Blast_tac 1);
  16.171  result();
  16.172  
  16.173  goal HOL.thy "? z. P(z) --> (! x. P(x))";
  16.174 -by (Deepen_tac 1 1);
  16.175 +by (Blast_tac 1);
  16.176  result();
  16.177  
  16.178  goal HOL.thy "? x. (? y. P(y)) --> P(x)";
  16.179 -by (Deepen_tac 1 1);
  16.180 +by (Blast_tac 1);
  16.181  result();
  16.182  
  16.183  writeln"Hard examples with quantifiers";
  16.184  
  16.185  writeln"Problem 18";
  16.186  goal HOL.thy "? y. ! x. P(y)-->P(x)";
  16.187 -by (Deepen_tac 1 1);
  16.188 +by (Blast_tac 1);
  16.189  result(); 
  16.190  
  16.191  writeln"Problem 19";
  16.192  goal HOL.thy "? x. ! y z. (P(y)-->Q(z)) --> (P(x)-->Q(x))";
  16.193 -by (Deepen_tac 1 1);
  16.194 +by (Blast_tac 1);
  16.195  result();
  16.196  
  16.197  writeln"Problem 20";
  16.198  goal HOL.thy "(! x y. ? z. ! w. (P(x)&Q(y)-->R(z)&S(w)))     \
  16.199  \   --> (? x y. P(x) & Q(y)) --> (? z. R(z))";
  16.200 -by (Fast_tac 1); 
  16.201 +by (Blast_tac 1); 
  16.202  result();
  16.203  
  16.204  writeln"Problem 21";
  16.205  goal HOL.thy "(? x. P-->Q(x)) & (? x. Q(x)-->P) --> (? x. P=Q(x))";
  16.206 -by (Deepen_tac 1 1); 
  16.207 +by (Blast_tac 1); 
  16.208  result();
  16.209  
  16.210  writeln"Problem 22";
  16.211  goal HOL.thy "(! x. P = Q(x))  -->  (P = (! x. Q(x)))";
  16.212 -by (Fast_tac 1); 
  16.213 +by (Blast_tac 1); 
  16.214  result();
  16.215  
  16.216  writeln"Problem 23";
  16.217  goal HOL.thy "(! x. P | Q(x))  =  (P | (! x. Q(x)))";
  16.218 -by (Best_tac 1);  
  16.219 +by (Blast_tac 1);  
  16.220  result();
  16.221  
  16.222  writeln"Problem 24";
  16.223  goal HOL.thy "~(? x. S(x)&Q(x)) & (! x. P(x) --> Q(x)|R(x)) &  \
  16.224  \    (~(? x.P(x)) --> (? x.Q(x))) & (! x. Q(x)|R(x) --> S(x))  \
  16.225  \   --> (? x. P(x)&R(x))";
  16.226 -by (Fast_tac 1); 
  16.227 +by (Blast_tac 1); 
  16.228  result();
  16.229  
  16.230  writeln"Problem 25";
  16.231 @@ -215,14 +215,14 @@
  16.232  \       (! x. P(x) --> (M(x) & L(x))) &   \
  16.233  \       ((! x. P(x)-->Q(x)) | (? x. P(x)&R(x)))  \
  16.234  \   --> (? x. Q(x)&P(x))";
  16.235 -by (Best_tac 1); 
  16.236 +by (Blast_tac 1); 
  16.237  result();
  16.238  
  16.239  writeln"Problem 26";
  16.240  goal HOL.thy "((? x. p(x)) = (? x. q(x))) &     \
  16.241  \     (! x. ! y. p(x) & q(y) --> (r(x) = s(y))) \
  16.242  \ --> ((! x. p(x)-->r(x)) = (! x. q(x)-->s(x)))";
  16.243 -by (Fast_tac 1);
  16.244 +by (Blast_tac 1);
  16.245  result();
  16.246  
  16.247  writeln"Problem 27";
  16.248 @@ -231,7 +231,7 @@
  16.249  \             (! x. M(x) & L(x) --> P(x)) &   \
  16.250  \             ((? x. R(x) & ~ Q(x)) --> (! x. L(x) --> ~ R(x)))  \
  16.251  \         --> (! x. M(x) --> ~L(x))";
  16.252 -by (Fast_tac 1); 
  16.253 +by (Blast_tac 1); 
  16.254  result();
  16.255  
  16.256  writeln"Problem 28.  AMENDED";
  16.257 @@ -239,21 +239,21 @@
  16.258  \       ((! x. Q(x)|R(x)) --> (? x. Q(x)&S(x))) &  \
  16.259  \       ((? x.S(x)) --> (! x. L(x) --> M(x)))  \
  16.260  \   --> (! x. P(x) & L(x) --> M(x))";
  16.261 -by (Fast_tac 1);  
  16.262 +by (Blast_tac 1);  
  16.263  result();
  16.264  
  16.265  writeln"Problem 29.  Essentially the same as Principia Mathematica *11.71";
  16.266  goal HOL.thy "(? x. F(x)) & (? y. G(y))  \
  16.267  \   --> ( ((! x. F(x)-->H(x)) & (! y. G(y)-->J(y)))  =   \
  16.268  \         (! x y. F(x) & G(y) --> H(x) & J(y)))";
  16.269 -by (Fast_tac 1); 
  16.270 +by (Blast_tac 1); 
  16.271  result();
  16.272  
  16.273  writeln"Problem 30";
  16.274  goal HOL.thy "(! x. P(x) | Q(x) --> ~ R(x)) & \
  16.275  \       (! x. (Q(x) --> ~ S(x)) --> P(x) & R(x))  \
  16.276  \   --> (! x. S(x))";
  16.277 -by (Fast_tac 1);  
  16.278 +by (Blast_tac 1);  
  16.279  result();
  16.280  
  16.281  writeln"Problem 31";
  16.282 @@ -261,7 +261,7 @@
  16.283  \       (? x. L(x) & P(x)) & \
  16.284  \       (! x. ~ R(x) --> M(x))  \
  16.285  \   --> (? x. L(x) & M(x))";
  16.286 -by (Fast_tac 1);
  16.287 +by (Blast_tac 1);
  16.288  result();
  16.289  
  16.290  writeln"Problem 32";
  16.291 @@ -269,13 +269,13 @@
  16.292  \       (! x. S(x) & R(x) --> L(x)) & \
  16.293  \       (! x. M(x) --> R(x))  \
  16.294  \   --> (! x. P(x) & M(x) --> L(x))";
  16.295 -by (Best_tac 1);
  16.296 +by (Blast_tac 1);
  16.297  result();
  16.298  
  16.299  writeln"Problem 33";
  16.300  goal HOL.thy "(! x. P(a) & (P(x)-->P(b))-->P(c))  =    \
  16.301  \    (! x. (~P(a) | P(x) | P(c)) & (~P(a) | ~P(b) | P(c)))";
  16.302 -by (Best_tac 1);
  16.303 +by (Blast_tac 1);
  16.304  result();
  16.305  
  16.306  writeln"Problem 34  AMENDED (TWICE!!)";
  16.307 @@ -284,13 +284,13 @@
  16.308  \                   ((? x. q(x)) = (! y. p(y))))   =    \
  16.309  \                  ((? x. ! y. q(x) = q(y))  =          \
  16.310  \                   ((? x. p(x)) = (! y. q(y))))";
  16.311 -by (Deepen_tac 3 1);
  16.312 +by (Blast_tac 1);
  16.313  (*slower with smaller bounds*)
  16.314  result();
  16.315  
  16.316  writeln"Problem 35";
  16.317  goal HOL.thy "? x y. P x y -->  (! u v. P u v)";
  16.318 -by (Deepen_tac 1 1);
  16.319 +by (Blast_tac 1);
  16.320  result();
  16.321  
  16.322  writeln"Problem 36";
  16.323 @@ -299,7 +299,7 @@
  16.324  \       (! x y. J x y | G x y -->       \
  16.325  \       (! z. J y z | G y z --> H x z))   \
  16.326  \   --> (! x. ? y. H x y)";
  16.327 -by (Fast_tac 1);
  16.328 +by (Blast_tac 1);
  16.329  result();
  16.330  
  16.331  writeln"Problem 37";
  16.332 @@ -308,7 +308,7 @@
  16.333  \       (! x z. ~(P x z) --> (? y. Q y z)) & \
  16.334  \       ((? x y. Q x y) --> (! x. R x x))  \
  16.335  \   --> (! x. ? y. R x y)";
  16.336 -by (Fast_tac 1);
  16.337 +by (Blast_tac 1);
  16.338  result();
  16.339  
  16.340  writeln"Problem 38";
  16.341 @@ -318,35 +318,36 @@
  16.342  \    (! x. (~p(a) | p(x) | (? z. ? w. p(z) & r x w & r w z)) &  \
  16.343  \          (~p(a) | ~(? y. p(y) & r x y) |                      \
  16.344  \           (? z. ? w. p(z) & r x w & r w z)))";
  16.345 -by (Deepen_tac 0 1);  (*beats fast_tac!*)
  16.346 +by (Blast_tac 1);  (*beats fast_tac!*)
  16.347  result();
  16.348  
  16.349  writeln"Problem 39";
  16.350  goal HOL.thy "~ (? x. ! y. F y x = (~ F y y))";
  16.351 -by (Fast_tac 1);
  16.352 +by (Blast_tac 1);
  16.353  result();
  16.354  
  16.355  writeln"Problem 40.  AMENDED";
  16.356  goal HOL.thy "(? y. ! x. F x y = F x x)  \
  16.357  \       -->  ~ (! x. ? y. ! z. F z y = (~ F z x))";
  16.358 -by (Fast_tac 1);
  16.359 +by (Blast_tac 1);
  16.360  result();
  16.361  
  16.362  writeln"Problem 41";
  16.363  goal HOL.thy "(! z. ? y. ! x. f x y = (f x z & ~ f x x))        \
  16.364  \              --> ~ (? z. ! x. f x z)";
  16.365 -by (Best_tac 1);
  16.366 +by (Blast_tac 1);
  16.367  result();
  16.368  
  16.369  writeln"Problem 42";
  16.370  goal HOL.thy "~ (? y. ! x. p x y = (~ (? z. p x z & p z x)))";
  16.371 -by (Deepen_tac 3 1);
  16.372 +by (Blast_tac 1);
  16.373  result();
  16.374  
  16.375 -writeln"Problem 43  NOT PROVED AUTOMATICALLY";
  16.376 +writeln"Problem 43!!";
  16.377  goal HOL.thy
  16.378      "(! x::'a. ! y::'a. q x y = (! z. p z x = (p z y::bool)))   \
  16.379  \ --> (! x. (! y. q x y = (q y x::bool)))";
  16.380 +by (Blast_tac 1);
  16.381  
  16.382  
  16.383  writeln"Problem 44";
  16.384 @@ -354,7 +355,7 @@
  16.385  \             (? y. g(y) & h x y & (? y. g(y) & ~ h x y)))  &   \
  16.386  \             (? x. j(x) & (! y. g(y) --> h x y))               \
  16.387  \             --> (? x. j(x) & ~f(x))";
  16.388 -by (Fast_tac 1);
  16.389 +by (Blast_tac 1);
  16.390  result();
  16.391  
  16.392  writeln"Problem 45";
  16.393 @@ -365,7 +366,7 @@
  16.394  \    (? x. f(x) & (! y. h x y --> l(y))                         \
  16.395  \               & (! y. g(y) & h x y --> j x y))                \
  16.396  \     --> (? x. f(x) & ~ (? y. g(y) & h x y))";
  16.397 -by (Best_tac 1); 
  16.398 +by (Blast_tac 1); 
  16.399  result();
  16.400  
  16.401  
  16.402 @@ -373,7 +374,7 @@
  16.403  
  16.404  writeln"Problem 48";
  16.405  goal HOL.thy "(a=b | c=d) & (a=c | b=d) --> a=d | b=c";
  16.406 -by (Fast_tac 1);
  16.407 +by (Blast_tac 1);
  16.408  result();
  16.409  
  16.410  writeln"Problem 49  NOT PROVED AUTOMATICALLY";
  16.411 @@ -386,20 +387,20 @@
  16.412  by (assume_tac 1);
  16.413  by (res_inst_tac [("x","b")] allE 1);
  16.414  by (assume_tac 1);
  16.415 -by (Fast_tac 1);
  16.416 +by (Blast_tac 1);
  16.417  result();
  16.418  
  16.419  writeln"Problem 50";  
  16.420  (*What has this to do with equality?*)
  16.421  goal HOL.thy "(! x. P a x | (! y.P x y)) --> (? x. ! y.P x y)";
  16.422 -by (Deepen_tac 1 1);
  16.423 +by (Blast_tac 1);
  16.424  result();
  16.425  
  16.426  writeln"Problem 51";
  16.427  goal HOL.thy
  16.428      "(? z w. ! x y. P x y = (x=z & y=w)) -->  \
  16.429  \    (? z. ! x. ? w. (! y. P x y = (y=w)) = (x=z))";
  16.430 -by (Best_tac 1);
  16.431 +by (Blast_tac 1);
  16.432  result();
  16.433  
  16.434  writeln"Problem 52";
  16.435 @@ -407,7 +408,7 @@
  16.436  goal HOL.thy
  16.437      "(? z w. ! x y. P x y = (x=z & y=w)) -->  \
  16.438  \    (? w. ! y. ? z. (! x. P x y = (x=z)) = (y=w))";
  16.439 -by (Best_tac 1);
  16.440 +by (Blast_tac 1);
  16.441  result();
  16.442  
  16.443  writeln"Problem 55";
  16.444 @@ -423,20 +424,20 @@
  16.445  \  (!x. hates agatha x --> hates butler x) & \
  16.446  \  (!x. ~hates x agatha | ~hates x butler | ~hates x charles) --> \
  16.447  \   killed ?who agatha";
  16.448 -by (Fast_tac 1);
  16.449 +by (Blast_tac 1);
  16.450  result();
  16.451  
  16.452  writeln"Problem 56";
  16.453  goal HOL.thy
  16.454      "(! x. (? y. P(y) & x=f(y)) --> P(x)) = (! x. P(x) --> P(f(x)))";
  16.455 -by (Fast_tac 1);
  16.456 +by (Blast_tac 1);
  16.457  result();
  16.458  
  16.459  writeln"Problem 57";
  16.460  goal HOL.thy
  16.461      "P (f a b) (f b c) & P (f b c) (f a c) & \
  16.462  \    (! x y z. P x y & P y z --> P x z)    -->   P (f a b) (f a c)";
  16.463 -by (Fast_tac 1);
  16.464 +by (Blast_tac 1);
  16.465  result();
  16.466  
  16.467  writeln"Problem 58  NOT PROVED AUTOMATICALLY";
  16.468 @@ -447,13 +448,13 @@
  16.469  
  16.470  writeln"Problem 59";
  16.471  goal HOL.thy "(! x. P(x) = (~P(f(x)))) --> (? x. P(x) & ~P(f(x)))";
  16.472 -by (Deepen_tac 1 1);
  16.473 +by (Blast_tac 1);
  16.474  result();
  16.475  
  16.476  writeln"Problem 60";
  16.477  goal HOL.thy
  16.478      "! x. P x (f x) = (? y. (! z. P z y --> P z (f x)) & P x y)";
  16.479 -by (Fast_tac 1);
  16.480 +by (Blast_tac 1);
  16.481  result();
  16.482  
  16.483  writeln"Problem 62 as corrected in JAR 18 (1997), page 135";
  16.484 @@ -461,7 +462,7 @@
  16.485      "(ALL x. p a & (p x --> p(f x)) --> p(f(f x)))  =   \
  16.486  \    (ALL x. (~ p a | p x | p(f(f x))) &                        \
  16.487  \            (~ p a | ~ p(f x) | p(f(f x))))";
  16.488 -by (Fast_tac 1);
  16.489 +by (Blast_tac 1);
  16.490  result();
  16.491  
  16.492  (*From Rudnicki, Obvious Inferences, JAR 3 (1987), 383-393.  
  16.493 @@ -470,14 +471,14 @@
  16.494      "(ALL x. F(x) & ~G(x) --> (EX y. H(x,y) & J(y))) &        \
  16.495  \    (EX x. K(x) & F(x) & (ALL y. H(x,y) --> K(y)))  &        \
  16.496  \    (ALL x. K(x) --> ~G(x))   -->   (EX x. K(x) --> ~G(x))";
  16.497 -by (Fast_tac 1);
  16.498 +by (Blast_tac 1);
  16.499  result();
  16.500  
  16.501  goal Prod.thy
  16.502      "(ALL x y. R(x,y) | R(y,x)) &                \
  16.503  \    (ALL x y. S(x,y) & S(y,x) --> x=y) &        \
  16.504  \    (ALL x y. R(x,y) --> S(x,y))    -->   (ALL x y. S(x,y) --> R(x,y))";
  16.505 -by (Fast_tac 1);
  16.506 +by (Blast_tac 1);
  16.507  result();
  16.508  
  16.509