1.1 --- a/src/ZF/ex/Comb.ML	Tue Apr 15 10:23:17 1997 +0200
     1.2 +++ b/src/ZF/ex/Comb.ML	Tue Apr 15 10:23:38 1997 +0200
     1.3 @@ -29,7 +29,7 @@
     1.4  val contract_combD2 = contract.dom_subset RS subsetD RS SigmaD2;
     1.5  
     1.6  goal Comb.thy "field(contract) = comb";
     1.7 -by (fast_tac (!claset addIs [contract.K] addSEs [contract_combE2]) 1);
     1.8 +by (blast_tac (!claset addIs [contract.K] addSEs [contract_combE2]) 1);
     1.9  qed "field_contract_eq";
    1.10  
    1.11  bind_thm ("reduction_refl",
    1.12 @@ -67,18 +67,18 @@
    1.13  AddSEs comb.free_SEs;
    1.14  
    1.15  goalw Comb.thy [I_def] "!!r. I -1-> r ==> P";
    1.16 -by (Fast_tac 1);
    1.17 +by (Blast_tac 1);
    1.18  qed "I_contract_E";
    1.19  
    1.20  goal Comb.thy "!!p r. K#p -1-> r ==> (EX q. r = K#q & p -1-> q)";
    1.21 -by (Fast_tac 1);
    1.22 +by (Blast_tac 1);
    1.23  qed "K1_contractD";
    1.24  
    1.25  goal Comb.thy "!!p r. [| p ---> q;  r: comb |] ==> p#r ---> q#r";
    1.26  by (forward_tac [rtrancl_type RS subsetD RS SigmaD1] 1);
    1.27  by (dtac (field_contract_eq RS equalityD1 RS subsetD) 1);
    1.28  by (etac rtrancl_induct 1);
    1.29 -by (fast_tac (!claset addIs reduction_rls) 1);
    1.30 +by (blast_tac (!claset addIs reduction_rls) 1);
    1.31  by (etac (trans_rtrancl RS transD) 1);
    1.32  by (fast_tac (!claset addIs reduction_rls) 1);
    1.33  qed "Ap_reduce1";
    1.34 @@ -87,7 +87,7 @@
    1.35  by (forward_tac [rtrancl_type RS subsetD RS SigmaD1] 1);
    1.36  by (dtac (field_contract_eq RS equalityD1 RS subsetD) 1);
    1.37  by (etac rtrancl_induct 1);
    1.38 -by (fast_tac (!claset addIs reduction_rls) 1);
    1.39 +by (blast_tac (!claset addIs reduction_rls) 1);
    1.40  by (etac (trans_rtrancl RS transD) 1);
    1.41  by (fast_tac (!claset addIs reduction_rls) 1);
    1.42  qed "Ap_reduce2";
    1.43 @@ -107,7 +107,7 @@
    1.44  qed "KIII_contract3";
    1.45  
    1.46  goalw Comb.thy [diamond_def] "~ diamond(contract)";
    1.47 -by (fast_tac (!claset addIs [KIII_contract1,KIII_contract2,KIII_contract3]
    1.48 +by (blast_tac (!claset addIs [KIII_contract1,KIII_contract2,KIII_contract3]
    1.49                      addSEs [I_contract_E]) 1);
    1.50  qed "not_diamond_contract";
    1.51  
    1.52 @@ -121,7 +121,7 @@
    1.53  val parcontract_combD2 = parcontract.dom_subset RS subsetD RS SigmaD2;
    1.54  
    1.55  goal Comb.thy "field(parcontract) = comb";
    1.56 -by (fast_tac (!claset addIs [parcontract.K] 
    1.57 +by (blast_tac (!claset addIs [parcontract.K] 
    1.58                        addSEs [parcontract_combE2]) 1);
    1.59  qed "field_parcontract_eq";
    1.60  
    1.61 @@ -139,16 +139,16 @@
    1.62  (*** Basic properties of parallel contraction ***)
    1.63  
    1.64  goal Comb.thy "!!p r. K#p =1=> r ==> (EX p'. r = K#p' & p =1=> p')";
    1.65 -by (Fast_tac 1);
    1.66 +by (Blast_tac 1);
    1.67  qed "K1_parcontractD";
    1.68  
    1.69  goal Comb.thy "!!p r. S#p =1=> r ==> (EX p'. r = S#p' & p =1=> p')";
    1.70 -by (Fast_tac 1);
    1.71 +by (Blast_tac 1);
    1.72  qed "S1_parcontractD";
    1.73  
    1.74  goal Comb.thy
    1.75   "!!p q r. S#p#q =1=> r ==> (EX p' q'. r = S#p'#q' & p =1=> p' & q =1=> q')";
    1.76 -by (fast_tac (!claset addSDs [S1_parcontractD]) 1);
    1.77 +by (blast_tac (!claset addSDs [S1_parcontractD]) 1);
    1.78  qed "S2_parcontractD";
    1.79  
    1.80  (*Church-Rosser property for parallel contraction*)
    1.81 @@ -165,9 +165,9 @@
    1.82      "!!x y r. [| diamond(r);  <x,y>:r^+ |] ==> \
    1.83  \    ALL y'. <x,y'>:r --> (EX z. <y',z>: r^+ & <y,z>: r)";
    1.84  by (etac trancl_induct 1);
    1.85 -by (fast_tac (!claset addIs [r_into_trancl]) 1);
    1.86 +by (blast_tac (!claset addIs [r_into_trancl]) 1);
    1.87  by (slow_best_tac (!claset addSDs [spec RS mp]
    1.88 -                         addIs  [r_into_trancl, trans_trancl RS transD]) 1);
    1.89 +                           addIs  [r_into_trancl, trans_trancl RS transD]) 1);
    1.90  val diamond_strip_lemmaE = result() RS spec RS mp RS exE;
    1.91  
    1.92  val [major] = goal Comb.thy "diamond(r) ==> diamond(r^+)";
    1.93 @@ -184,29 +184,29 @@
    1.94  
    1.95  goal Comb.thy "!!p q. p-1->q ==> p=1=>q";
    1.96  by (etac contract.induct 1);
    1.97 -by (ALLGOALS (fast_tac (!claset)));
    1.98 +by (ALLGOALS Blast_tac);
    1.99  qed "contract_imp_parcontract";
   1.100  
   1.101  goal Comb.thy "!!p q. p--->q ==> p===>q";
   1.102  by (forward_tac [rtrancl_type RS subsetD RS SigmaD1] 1);
   1.103  by (dtac (field_contract_eq RS equalityD1 RS subsetD) 1);
   1.104  by (etac rtrancl_induct 1);
   1.105 -by (fast_tac (!claset addIs [r_into_trancl]) 1);
   1.106 -by (fast_tac (!claset addIs [contract_imp_parcontract, 
   1.107 -                           r_into_trancl, trans_trancl RS transD]) 1);
   1.108 +by (blast_tac (!claset addIs [r_into_trancl]) 1);
   1.109 +by (blast_tac (!claset addIs [contract_imp_parcontract, 
   1.110 +			      r_into_trancl, trans_trancl RS transD]) 1);
   1.111  qed "reduce_imp_parreduce";
   1.112  
   1.113  
   1.114  goal Comb.thy "!!p q. p=1=>q ==> p--->q";
   1.115  by (etac parcontract.induct 1);
   1.116 -by (fast_tac (!claset addIs reduction_rls) 1);
   1.117 -by (fast_tac (!claset addIs reduction_rls) 1);
   1.118 -by (fast_tac (!claset addIs reduction_rls) 1);
   1.119 +by (blast_tac (!claset addIs reduction_rls) 1);
   1.120 +by (blast_tac (!claset addIs reduction_rls) 1);
   1.121 +by (blast_tac (!claset addIs reduction_rls) 1);
   1.122  by (rtac (trans_rtrancl RS transD) 1);
   1.123  by (ALLGOALS 
   1.124 -    (fast_tac 
   1.125 -     (!claset addIs [Ap_reduce1, Ap_reduce2]
   1.126 -                  addSEs [parcontract_combD1,parcontract_combD2])));
   1.127 +    (blast_tac 
   1.128 +     (!claset addIs [Ap_reduce1, Ap_reduce2, parcontract_combD1,
   1.129 +		     parcontract_combD2])));
   1.130  qed "parcontract_imp_reduce";
   1.131  
   1.132  goal Comb.thy "!!p q. p===>q ==> p--->q";