Ran expandshort
authorpaulson
Wed Mar 06 12:52:11 1996 +0100 (1996-03-06)
changeset 15526f71b5d46700
parent 1551 4a617e14d12c
child 1553 4eb4a9c7d736
Ran expandshort
src/HOL/Arith.ML
src/HOL/Lfp.ML
src/HOL/List.ML
src/HOL/Nat.ML
src/HOL/Prod.ML
src/HOL/RelPow.ML
src/HOL/Relation.ML
src/HOL/Set.ML
src/HOL/Trancl.ML
src/HOL/WF.ML
src/HOL/subset.ML
     1.1 --- a/src/HOL/Arith.ML	Wed Mar 06 12:19:16 1996 +0100
     1.2 +++ b/src/HOL/Arith.ML	Wed Mar 06 12:52:11 1996 +0100
     1.3 @@ -19,9 +19,9 @@
     1.4  (** pred **)
     1.5  
     1.6  val prems = goal Arith.thy "n ~= 0 ==> Suc(pred n) = n";
     1.7 -by(res_inst_tac [("n","n")] natE 1);
     1.8 -by(cut_facts_tac prems 1);
     1.9 -by(ALLGOALS Asm_full_simp_tac);
    1.10 +by (res_inst_tac [("n","n")] natE 1);
    1.11 +by (cut_facts_tac prems 1);
    1.12 +by (ALLGOALS Asm_full_simp_tac);
    1.13  qed "Suc_pred";
    1.14  Addsimps [Suc_pred];
    1.15  
    1.16 @@ -205,12 +205,12 @@
    1.17  
    1.18  goal Arith.thy "!!m. m<n ==> m mod n = m";
    1.19  by (rtac (mod_def1 RS wf_less_trans) 1);
    1.20 -by(Asm_simp_tac 1);
    1.21 +by (Asm_simp_tac 1);
    1.22  qed "mod_less";
    1.23  
    1.24  goal Arith.thy "!!m. [| 0<n;  ~m<n |] ==> m mod n = (m-n) mod n";
    1.25  by (rtac (mod_def1 RS wf_less_trans) 1);
    1.26 -by(asm_simp_tac (!simpset addsimps [diff_less, cut_apply, less_eq]) 1);
    1.27 +by (asm_simp_tac (!simpset addsimps [diff_less, cut_apply, less_eq]) 1);
    1.28  qed "mod_geq";
    1.29  
    1.30  
    1.31 @@ -223,12 +223,12 @@
    1.32  
    1.33  goal Arith.thy "!!m. m<n ==> m div n = 0";
    1.34  by (rtac (div_def1 RS wf_less_trans) 1);
    1.35 -by(Asm_simp_tac 1);
    1.36 +by (Asm_simp_tac 1);
    1.37  qed "div_less";
    1.38  
    1.39  goal Arith.thy "!!M. [| 0<n;  ~m<n |] ==> m div n = Suc((m-n) div n)";
    1.40  by (rtac (div_def1 RS wf_less_trans) 1);
    1.41 -by(asm_simp_tac (!simpset addsimps [diff_less, cut_apply, less_eq]) 1);
    1.42 +by (asm_simp_tac (!simpset addsimps [diff_less, cut_apply, less_eq]) 1);
    1.43  qed "div_geq";
    1.44  
    1.45  (*Main Result about quotient and remainder.*)
    1.46 @@ -268,7 +268,7 @@
    1.47  qed "Suc_diff_n";
    1.48  
    1.49  goal Arith.thy "Suc(m)-n = (if m<n then 0 else Suc(m-n))";
    1.50 -by(simp_tac (!simpset addsimps [less_imp_diff_is_0, not_less_eq, Suc_diff_n]
    1.51 +by (simp_tac (!simpset addsimps [less_imp_diff_is_0, not_less_eq, Suc_diff_n]
    1.52                      setloop (split_tac [expand_if])) 1);
    1.53  qed "if_Suc_diff_n";
    1.54  
    1.55 @@ -326,20 +326,20 @@
    1.56  bind_thm ("trans_less_add2", le_add2 RSN (2,less_le_trans));
    1.57  
    1.58  goal Arith.thy "!!i. i+j < (k::nat) ==> i<k";
    1.59 -be rev_mp 1;
    1.60 -by(nat_ind_tac "j" 1);
    1.61 +by (etac rev_mp 1);
    1.62 +by (nat_ind_tac "j" 1);
    1.63  by (ALLGOALS Asm_simp_tac);
    1.64 -by(fast_tac (HOL_cs addDs [Suc_lessD]) 1);
    1.65 +by (fast_tac (HOL_cs addDs [Suc_lessD]) 1);
    1.66  qed "add_lessD1";
    1.67  
    1.68  goal Arith.thy "!!k::nat. m <= n ==> m <= n+k";
    1.69 -by (eresolve_tac [le_trans] 1);
    1.70 -by (resolve_tac [le_add1] 1);
    1.71 +by (etac le_trans 1);
    1.72 +by (rtac le_add1 1);
    1.73  qed "le_imp_add_le";
    1.74  
    1.75  goal Arith.thy "!!k::nat. m < n ==> m < n+k";
    1.76 -by (eresolve_tac [less_le_trans] 1);
    1.77 -by (resolve_tac [le_add1] 1);
    1.78 +by (etac less_le_trans 1);
    1.79 +by (rtac le_add1 1);
    1.80  qed "less_imp_add_less";
    1.81  
    1.82  goal Arith.thy "m+k<=n --> m<=(n::nat)";
    1.83 @@ -353,7 +353,7 @@
    1.84  by (asm_full_simp_tac
    1.85      (!simpset delsimps [add_Suc_right]
    1.86                  addsimps ([add_Suc_right RS sym, add_left_cancel] @add_ac)) 1);
    1.87 -by (eresolve_tac [subst] 1);
    1.88 +by (etac subst 1);
    1.89  by (simp_tac (!simpset addsimps [less_add_Suc1]) 1);
    1.90  qed "less_add_eq_less";
    1.91  
    1.92 @@ -389,7 +389,7 @@
    1.93  (*non-strict, in 1st argument*)
    1.94  goal Arith.thy "!!i j k::nat. i<=j ==> i + k <= j + k";
    1.95  by (res_inst_tac [("f", "%j.j+k")] less_mono_imp_le_mono 1);
    1.96 -by (eresolve_tac [add_less_mono1] 1);
    1.97 +by (etac add_less_mono1 1);
    1.98  by (assume_tac 1);
    1.99  qed "add_le_mono1";
   1.100  
   1.101 @@ -398,5 +398,5 @@
   1.102  by (etac (add_le_mono1 RS le_trans) 1);
   1.103  by (simp_tac (!simpset addsimps [add_commute]) 1);
   1.104  (*j moves to the end because it is free while k, l are bound*)
   1.105 -by (eresolve_tac [add_le_mono1] 1);
   1.106 +by (etac add_le_mono1 1);
   1.107  qed "add_le_mono";
     2.1 --- a/src/HOL/Lfp.ML	Wed Mar 06 12:19:16 1996 +0100
     2.2 +++ b/src/HOL/Lfp.ML	Wed Mar 06 12:52:11 1996 +0100
     2.3 @@ -54,18 +54,18 @@
     2.4  val major::prems = goal Lfp.thy
     2.5    "[| (a,b) : lfp f; mono f; \
     2.6  \     !!a b. (a,b) : f(lfp f Int Collect(split P)) ==> P a b |] ==> P a b";
     2.7 -by(res_inst_tac [("c1","P")] (split RS subst) 1);
     2.8 +by (res_inst_tac [("c1","P")] (split RS subst) 1);
     2.9  by (rtac (major RS induct) 1);
    2.10  by (resolve_tac prems 1);
    2.11 -by(res_inst_tac[("p","x")]PairE 1);
    2.12 -by(hyp_subst_tac 1);
    2.13 -by(asm_simp_tac (!simpset addsimps prems) 1);
    2.14 +by (res_inst_tac[("p","x")]PairE 1);
    2.15 +by (hyp_subst_tac 1);
    2.16 +by (asm_simp_tac (!simpset addsimps prems) 1);
    2.17  qed"induct2";
    2.18  
    2.19  (*** Fixpoint induction a la David Park ***)
    2.20  goal Lfp.thy "!!f. [| mono f; f A <= A |] ==> lfp(f) <= A";
    2.21  by (rtac subsetI 1);
    2.22 -by(EVERY[etac induct 1, atac 1, etac subsetD 1, rtac subsetD 1,
    2.23 +by (EVERY[etac induct 1, atac 1, etac subsetD 1, rtac subsetD 1,
    2.24                  atac 2, fast_tac (set_cs addSEs [monoD]) 1]);
    2.25  qed "Park_induct";
    2.26  
     3.1 --- a/src/HOL/List.ML	Wed Mar 06 12:19:16 1996 +0100
     3.2 +++ b/src/HOL/List.ML	Wed Mar 06 12:52:11 1996 +0100
     3.3 @@ -193,7 +193,7 @@
     3.4  qed "drop_0";
     3.5  
     3.6  goal thy "drop (Suc n) (x#xs) = drop n xs";
     3.7 -by(Simp_tac 1);
     3.8 +by (Simp_tac 1);
     3.9  qed "drop_Suc_Cons";
    3.10  
    3.11  Delsimps [drop_Cons];
    3.12 @@ -207,7 +207,7 @@
    3.13  qed "take_0";
    3.14  
    3.15  goal thy "take (Suc n) (x#xs) = x # take n xs";
    3.16 -by(Simp_tac 1);
    3.17 +by (Simp_tac 1);
    3.18  qed "take_Suc_Cons";
    3.19  
    3.20  Delsimps [take_Cons];
     4.1 --- a/src/HOL/Nat.ML	Wed Mar 06 12:19:16 1996 +0100
     4.2 +++ b/src/HOL/Nat.ML	Wed Mar 06 12:52:11 1996 +0100
     4.3 @@ -231,7 +231,7 @@
     4.4  (** Elimination properties **)
     4.5  
     4.6  val prems = goalw Nat.thy [less_def] "n<m ==> ~ m<(n::nat)";
     4.7 -by(fast_tac (HOL_cs addIs ([wf_pred_nat, wf_trancl RS wf_asym]@prems))1);
     4.8 +by (fast_tac (HOL_cs addIs ([wf_pred_nat, wf_trancl RS wf_asym]@prems))1);
     4.9  qed "less_not_sym";
    4.10  
    4.11  (* [| n(m; m(n |] ==> R *)
    4.12 @@ -246,7 +246,7 @@
    4.13  bind_thm ("less_anti_refl", (less_not_refl RS notE));
    4.14  
    4.15  goal Nat.thy "!!m. n<m ==> m ~= (n::nat)";
    4.16 -by(fast_tac (HOL_cs addEs [less_anti_refl]) 1);
    4.17 +by (fast_tac (HOL_cs addEs [less_anti_refl]) 1);
    4.18  qed "less_not_refl2";
    4.19  
    4.20  
    4.21 @@ -285,9 +285,9 @@
    4.22  qed "less_Suc_eq";
    4.23  
    4.24  val prems = goal Nat.thy "m<n ==> n ~= 0";
    4.25 -by(res_inst_tac [("n","n")] natE 1);
    4.26 -by(cut_facts_tac prems 1);
    4.27 -by(ALLGOALS Asm_full_simp_tac);
    4.28 +by (res_inst_tac [("n","n")] natE 1);
    4.29 +by (cut_facts_tac prems 1);
    4.30 +by (ALLGOALS Asm_full_simp_tac);
    4.31  qed "gr_implies_not0";
    4.32  Addsimps [gr_implies_not0];
    4.33  
    4.34 @@ -335,14 +335,14 @@
    4.35  Addsimps [Suc_less_eq];
    4.36  
    4.37  goal Nat.thy "~(Suc(n) < n)";
    4.38 -by(fast_tac (HOL_cs addEs [Suc_lessD RS less_anti_refl]) 1);
    4.39 +by (fast_tac (HOL_cs addEs [Suc_lessD RS less_anti_refl]) 1);
    4.40  qed "not_Suc_n_less_n";
    4.41  Addsimps [not_Suc_n_less_n];
    4.42  
    4.43  goal Nat.thy "!!i. i<j ==> j<k --> Suc i < k";
    4.44 -by(nat_ind_tac "k" 1);
    4.45 -by(ALLGOALS (asm_simp_tac (!simpset addsimps [less_Suc_eq])));
    4.46 -by(fast_tac (HOL_cs addDs [Suc_lessD]) 1);
    4.47 +by (nat_ind_tac "k" 1);
    4.48 +by (ALLGOALS (asm_simp_tac (!simpset addsimps [less_Suc_eq])));
    4.49 +by (fast_tac (HOL_cs addDs [Suc_lessD]) 1);
    4.50  qed_spec_mp "less_trans_Suc";
    4.51  
    4.52  (*"Less than" is a linear ordering*)
    4.53 @@ -357,7 +357,7 @@
    4.54  (*Can be used with less_Suc_eq to get n=m | n<m *)
    4.55  goal Nat.thy "(~ m < n) = (n < Suc(m))";
    4.56  by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
    4.57 -by(ALLGOALS Asm_simp_tac);
    4.58 +by (ALLGOALS Asm_simp_tac);
    4.59  qed "not_less_eq";
    4.60  
    4.61  (*Complete induction, aka course-of-values induction*)
    4.62 @@ -375,12 +375,12 @@
    4.63  qed "le0";
    4.64  
    4.65  goalw Nat.thy [le_def] "~ Suc n <= n";
    4.66 -by(Simp_tac 1);
    4.67 +by (Simp_tac 1);
    4.68  qed "Suc_n_not_le_n";
    4.69  
    4.70  goalw Nat.thy [le_def] "(i <= 0) = (i = 0)";
    4.71 -by(nat_ind_tac "i" 1);
    4.72 -by(ALLGOALS Asm_simp_tac);
    4.73 +by (nat_ind_tac "i" 1);
    4.74 +by (ALLGOALS Asm_simp_tac);
    4.75  qed "le_0";
    4.76  
    4.77  Addsimps [less_not_refl,
    4.78 @@ -413,13 +413,13 @@
    4.79  qed "not_leE";
    4.80  
    4.81  goalw Nat.thy [le_def] "!!m. m < n ==> Suc(m) <= n";
    4.82 -by(Simp_tac 1);
    4.83 +by (Simp_tac 1);
    4.84  by (fast_tac (HOL_cs addEs [less_anti_refl,less_asym]) 1);
    4.85  qed "lessD";
    4.86  
    4.87  goalw Nat.thy [le_def] "!!m. Suc(m) <= n ==> m <= n";
    4.88 -by(Asm_full_simp_tac 1);
    4.89 -by(fast_tac HOL_cs 1);
    4.90 +by (Asm_full_simp_tac 1);
    4.91 +by (fast_tac HOL_cs 1);
    4.92  qed "Suc_leD";
    4.93  
    4.94  goalw Nat.thy [le_def] "!!m. m <= n ==> m <= Suc n";
    4.95 @@ -447,7 +447,7 @@
    4.96  qed "le_eq_less_or_eq";
    4.97  
    4.98  goal Nat.thy "n <= (n::nat)";
    4.99 -by(simp_tac (!simpset addsimps [le_eq_less_or_eq]) 1);
   4.100 +by (simp_tac (!simpset addsimps [le_eq_less_or_eq]) 1);
   4.101  qed "le_refl";
   4.102  
   4.103  val prems = goal Nat.thy "!!i. [| i <= j; j < k |] ==> i < (k::nat)";
     5.1 --- a/src/HOL/Prod.ML	Wed Mar 06 12:19:16 1996 +0100
     5.2 +++ b/src/HOL/Prod.ML	Wed Mar 06 12:52:11 1996 +0100
     5.3 @@ -78,7 +78,7 @@
     5.4  end;
     5.5  
     5.6  goal Prod.thy "(!x. P x) = (!a b. P(a,b))";
     5.7 -by(fast_tac (HOL_cs addbefore split_all_tac 1) 1);
     5.8 +by (fast_tac (HOL_cs addbefore split_all_tac 1) 1);
     5.9  qed "split_paired_All";
    5.10  
    5.11  goalw Prod.thy [split_def] "split c (a,b) = c a b";
    5.12 @@ -123,7 +123,7 @@
    5.13    Could instead call simp_tac/asm_full_simp_tac using split as rewrite.*)
    5.14  
    5.15  goal Prod.thy "!!p. [| !!a b. p=(a,b) ==> c a b |] ==> split c p";
    5.16 -by(split_all_tac 1);
    5.17 +by (split_all_tac 1);
    5.18  by (Asm_simp_tac 1);
    5.19  qed "splitI2";
    5.20  
    5.21 @@ -145,7 +145,7 @@
    5.22  qed "mem_splitI";
    5.23  
    5.24  goal Prod.thy "!!p. [| !!a b. p=(a,b) ==> z: c a b |] ==> z: split c p";
    5.25 -by(split_all_tac 1);
    5.26 +by (split_all_tac 1);
    5.27  by (Asm_simp_tac 1);
    5.28  qed "mem_splitI2";
    5.29  
     6.1 --- a/src/HOL/RelPow.ML	Wed Mar 06 12:19:16 1996 +0100
     6.2 +++ b/src/HOL/RelPow.ML	Wed Mar 06 12:52:11 1996 +0100
     6.3 @@ -10,85 +10,85 @@
     6.4  Addsimps [rel_pow_0];
     6.5  
     6.6  goal RelPow.thy "(x,x) : R^0";
     6.7 -by(Simp_tac 1);
     6.8 +by (Simp_tac 1);
     6.9  qed "rel_pow_0_I";
    6.10  
    6.11  goal RelPow.thy "!!R. [| (x,y) : R^n; (y,z):R |] ==> (x,z):R^(Suc n)";
    6.12 -by(simp_tac (!simpset addsimps [rel_pow_Suc]) 1);
    6.13 -by(fast_tac comp_cs 1);
    6.14 +by (simp_tac (!simpset addsimps [rel_pow_Suc]) 1);
    6.15 +by (fast_tac comp_cs 1);
    6.16  qed "rel_pow_Suc_I";
    6.17  
    6.18  goal RelPow.thy "!z. (x,y) : R --> (y,z):R^n -->  (x,z):R^(Suc n)";
    6.19 -by(nat_ind_tac "n" 1);
    6.20 -by(simp_tac (!simpset addsimps [rel_pow_Suc]) 1);
    6.21 -by(fast_tac comp_cs 1);
    6.22 -by(asm_full_simp_tac (!simpset addsimps [rel_pow_Suc]) 1);
    6.23 -by(fast_tac comp_cs 1);
    6.24 +by (nat_ind_tac "n" 1);
    6.25 +by (simp_tac (!simpset addsimps [rel_pow_Suc]) 1);
    6.26 +by (fast_tac comp_cs 1);
    6.27 +by (asm_full_simp_tac (!simpset addsimps [rel_pow_Suc]) 1);
    6.28 +by (fast_tac comp_cs 1);
    6.29  qed_spec_mp "rel_pow_Suc_I2";
    6.30  
    6.31  goal RelPow.thy "!!R. [| (x,y) : R^0; x=y ==> P |] ==> P";
    6.32 -by(Asm_full_simp_tac 1);
    6.33 +by (Asm_full_simp_tac 1);
    6.34  qed "rel_pow_0_E";
    6.35  
    6.36  val [major,minor] = goal RelPow.thy
    6.37    "[| (x,z) : R^(Suc n);  !!y. [| (x,y) : R^n; (y,z) : R |] ==> P |] ==> P";
    6.38 -by(cut_facts_tac [major] 1);
    6.39 -by(asm_full_simp_tac (!simpset addsimps [rel_pow_Suc]) 1);
    6.40 -by(fast_tac (comp_cs addIs [minor]) 1);
    6.41 +by (cut_facts_tac [major] 1);
    6.42 +by (asm_full_simp_tac (!simpset addsimps [rel_pow_Suc]) 1);
    6.43 +by (fast_tac (comp_cs addIs [minor]) 1);
    6.44  qed "rel_pow_Suc_E";
    6.45  
    6.46  val [p1,p2,p3] = goal RelPow.thy
    6.47      "[| (x,z) : R^n;  [| n=0; x = z |] ==> P;        \
    6.48  \       !!y m. [| n = Suc m; (x,y) : R^m; (y,z) : R |] ==> P  \
    6.49  \    |] ==> P";
    6.50 -by(res_inst_tac [("n","n")] natE 1);
    6.51 -by(cut_facts_tac [p1] 1);
    6.52 -by(asm_full_simp_tac (!simpset addsimps [p2]) 1);
    6.53 -by(cut_facts_tac [p1] 1);
    6.54 -by(Asm_full_simp_tac 1);
    6.55 -be rel_pow_Suc_E 1;
    6.56 -by(REPEAT(ares_tac [p3] 1));
    6.57 +by (res_inst_tac [("n","n")] natE 1);
    6.58 +by (cut_facts_tac [p1] 1);
    6.59 +by (asm_full_simp_tac (!simpset addsimps [p2]) 1);
    6.60 +by (cut_facts_tac [p1] 1);
    6.61 +by (Asm_full_simp_tac 1);
    6.62 +by (etac rel_pow_Suc_E 1);
    6.63 +by (REPEAT(ares_tac [p3] 1));
    6.64  qed "rel_pow_E";
    6.65  
    6.66  goal RelPow.thy "!x z. (x,z):R^(Suc n) --> (? y. (x,y):R & (y,z):R^n)";
    6.67 -by(nat_ind_tac "n" 1);
    6.68 -by(fast_tac (HOL_cs addIs [rel_pow_0_I] addEs [rel_pow_0_E,rel_pow_Suc_E]) 1);
    6.69 -by(fast_tac (HOL_cs addIs [rel_pow_Suc_I] addEs[rel_pow_0_E,rel_pow_Suc_E]) 1);
    6.70 +by (nat_ind_tac "n" 1);
    6.71 +by (fast_tac (HOL_cs addIs [rel_pow_0_I] addEs [rel_pow_0_E,rel_pow_Suc_E]) 1);
    6.72 +by (fast_tac (HOL_cs addIs [rel_pow_Suc_I] addEs[rel_pow_0_E,rel_pow_Suc_E]) 1);
    6.73  qed_spec_mp "rel_pow_Suc_D2";
    6.74  
    6.75  val [p1,p2,p3] = goal RelPow.thy
    6.76      "[| (x,z) : R^n;  [| n=0; x = z |] ==> P;        \
    6.77  \       !!y m. [| n = Suc m; (x,y) : R; (y,z) : R^m |] ==> P  \
    6.78  \    |] ==> P";
    6.79 -by(res_inst_tac [("n","n")] natE 1);
    6.80 -by(cut_facts_tac [p1] 1);
    6.81 -by(asm_full_simp_tac (!simpset addsimps [p2]) 1);
    6.82 -by(cut_facts_tac [p1] 1);
    6.83 -by(Asm_full_simp_tac 1);
    6.84 -bd rel_pow_Suc_D2 1;
    6.85 -be exE 1;
    6.86 -be p3 1;
    6.87 -be conjunct1 1;
    6.88 -be conjunct2 1;
    6.89 +by (res_inst_tac [("n","n")] natE 1);
    6.90 +by (cut_facts_tac [p1] 1);
    6.91 +by (asm_full_simp_tac (!simpset addsimps [p2]) 1);
    6.92 +by (cut_facts_tac [p1] 1);
    6.93 +by (Asm_full_simp_tac 1);
    6.94 +by (dtac rel_pow_Suc_D2 1);
    6.95 +by (etac exE 1);
    6.96 +by (etac p3 1);
    6.97 +by (etac conjunct1 1);
    6.98 +by (etac conjunct2 1);
    6.99  qed "rel_pow_E2";
   6.100  
   6.101  goal RelPow.thy "!!p. p:R^* ==> p : (UN n. R^n)";
   6.102 -by(split_all_tac 1);
   6.103 -be rtrancl_induct 1;
   6.104 -by(ALLGOALS (fast_tac (rel_cs addIs [rel_pow_0_I,rel_pow_Suc_I])));
   6.105 +by (split_all_tac 1);
   6.106 +by (etac rtrancl_induct 1);
   6.107 +by (ALLGOALS (fast_tac (rel_cs addIs [rel_pow_0_I,rel_pow_Suc_I])));
   6.108  qed "rtrancl_imp_UN_rel_pow";
   6.109  
   6.110  goal RelPow.thy "!y. (x,y):R^n --> (x,y):R^*";
   6.111 -by(nat_ind_tac "n" 1);
   6.112 -by(fast_tac (HOL_cs addIs [rtrancl_refl] addEs [rel_pow_0_E]) 1);
   6.113 -by(fast_tac (trancl_cs addEs [rel_pow_Suc_E,rtrancl_into_rtrancl]) 1);
   6.114 +by (nat_ind_tac "n" 1);
   6.115 +by (fast_tac (HOL_cs addIs [rtrancl_refl] addEs [rel_pow_0_E]) 1);
   6.116 +by (fast_tac (trancl_cs addEs [rel_pow_Suc_E,rtrancl_into_rtrancl]) 1);
   6.117  val lemma = result() RS spec RS mp;
   6.118  
   6.119  goal RelPow.thy "!!p. p:R^n ==> p:R^*";
   6.120 -by(split_all_tac 1);
   6.121 -be lemma 1;
   6.122 +by (split_all_tac 1);
   6.123 +by (etac lemma 1);
   6.124  qed "rel_pow_imp_rtrancl";
   6.125  
   6.126  goal RelPow.thy "R^* = (UN n. R^n)";
   6.127 -by(fast_tac (eq_cs addIs [rtrancl_imp_UN_rel_pow,rel_pow_imp_rtrancl]) 1);
   6.128 +by (fast_tac (eq_cs addIs [rtrancl_imp_UN_rel_pow,rel_pow_imp_rtrancl]) 1);
   6.129  qed "rtrancl_is_UN_rel_pow";
     7.1 --- a/src/HOL/Relation.ML	Wed Mar 06 12:19:16 1996 +0100
     7.2 +++ b/src/HOL/Relation.ML	Wed Mar 06 12:52:11 1996 +0100
     7.3 @@ -27,7 +27,7 @@
     7.4  qed "idE";
     7.5  
     7.6  goalw Relation.thy [id_def] "(a,b):id = (a=b)";
     7.7 -by(fast_tac prod_cs 1);
     7.8 +by (fast_tac prod_cs 1);
     7.9  qed "pair_in_id_conv";
    7.10  
    7.11  
     8.1 --- a/src/HOL/Set.ML	Wed Mar 06 12:19:16 1996 +0100
     8.2 +++ b/src/HOL/Set.ML	Wed Mar 06 12:52:11 1996 +0100
     8.3 @@ -311,7 +311,7 @@
     8.4      (REPEAT (eresolve_tac (prems @ [emptyE]) 1)) ]);
     8.5  
     8.6  goalw Set.thy [insert_def] "!!a. b : {a} ==> b=a";
     8.7 -by(fast_tac (HOL_cs addSEs [emptyE,CollectE,UnE]) 1);
     8.8 +by (fast_tac (HOL_cs addSEs [emptyE,CollectE,UnE]) 1);
     8.9  qed "singletonD";
    8.10  
    8.11  val singletonE = make_elim singletonD;
     9.1 --- a/src/HOL/Trancl.ML	Wed Mar 06 12:19:16 1996 +0100
     9.2 +++ b/src/HOL/Trancl.ML	Wed Mar 06 12:52:11 1996 +0100
     9.3 @@ -32,13 +32,13 @@
     9.4  
     9.5  (*rtrancl of r contains r*)
     9.6  goal Trancl.thy "!!p. p : r ==> p : r^*";
     9.7 -by(split_all_tac 1);
     9.8 +by (split_all_tac 1);
     9.9  by (etac (rtrancl_refl RS rtrancl_into_rtrancl) 1);
    9.10  qed "r_into_rtrancl";
    9.11  
    9.12  (*monotonicity of rtrancl*)
    9.13  goalw Trancl.thy [rtrancl_def] "!!r s. r <= s ==> r^* <= s^*";
    9.14 -by(REPEAT(ares_tac [lfp_mono,Un_mono,comp_mono,subset_refl] 1));
    9.15 +by (REPEAT(ares_tac [lfp_mono,Un_mono,comp_mono,subset_refl] 1));
    9.16  qed "rtrancl_mono";
    9.17  
    9.18  (** standard induction rule **)
    9.19 @@ -71,7 +71,7 @@
    9.20  (*transitivity of transitive closure!! -- by induction.*)
    9.21  goal Trancl.thy "!!r. [| (a,b):r^*; (b,c):r^* |] ==> (a,c):r^*";
    9.22  by (eres_inst_tac [("b","c")] rtrancl_induct 1);
    9.23 -by(ALLGOALS(fast_tac (HOL_cs addIs [rtrancl_into_rtrancl])));
    9.24 +by (ALLGOALS(fast_tac (HOL_cs addIs [rtrancl_into_rtrancl])));
    9.25  qed "rtrancl_trans";
    9.26  
    9.27  (*elimination of rtrancl -- by induction on a special formula*)
    9.28 @@ -87,13 +87,13 @@
    9.29  qed "rtranclE";
    9.30  
    9.31  goal Trancl.thy "!!R. (y,z):R^* ==> !x. (x,y):R --> (x,z):R^*";
    9.32 -be rtrancl_induct 1;
    9.33 -by(fast_tac (HOL_cs addIs [r_into_rtrancl]) 1);
    9.34 -by(fast_tac (HOL_cs addEs [rtrancl_into_rtrancl]) 1);
    9.35 +by (etac rtrancl_induct 1);
    9.36 +by (fast_tac (HOL_cs addIs [r_into_rtrancl]) 1);
    9.37 +by (fast_tac (HOL_cs addEs [rtrancl_into_rtrancl]) 1);
    9.38  val lemma = result();
    9.39  
    9.40  goal Trancl.thy  "!!R. [| (x,y) : R;  (y,z) : R^* |] ==> (x,z) : R^*";
    9.41 -by(fast_tac (HOL_cs addDs [lemma]) 1);
    9.42 +by (fast_tac (HOL_cs addDs [lemma]) 1);
    9.43  qed "rtrancl_into_rtrancl2";
    9.44  
    9.45  
    9.46 @@ -163,12 +163,12 @@
    9.47  
    9.48  goal Trancl.thy "(r^*)^* = r^*";
    9.49  by (rtac set_ext 1);
    9.50 -by(res_inst_tac [("p","x")] PairE 1);
    9.51 -by(hyp_subst_tac 1);
    9.52 +by (res_inst_tac [("p","x")] PairE 1);
    9.53 +by (hyp_subst_tac 1);
    9.54  by (rtac iffI 1);
    9.55  by (etac rtrancl_induct 1);
    9.56  by (rtac rtrancl_refl 1);
    9.57 -by(fast_tac (HOL_cs addEs [rtrancl_trans]) 1);
    9.58 +by (fast_tac (HOL_cs addEs [rtrancl_trans]) 1);
    9.59  by (etac r_into_rtrancl 1);
    9.60  qed "rtrancl_idemp";
    9.61  Addsimps [rtrancl_idemp];
    9.62 @@ -176,17 +176,17 @@
    9.63  goal Trancl.thy "!!R. [| R <= S; S <= R^* |] ==> S^* = R^*";
    9.64  by (dtac rtrancl_mono 1);
    9.65  by (dtac rtrancl_mono 1);
    9.66 -by(Asm_full_simp_tac 1);
    9.67 -by(fast_tac eq_cs 1);
    9.68 +by (Asm_full_simp_tac 1);
    9.69 +by (fast_tac eq_cs 1);
    9.70  qed "rtrancl_subset";
    9.71  
    9.72  goal Trancl.thy "!!R. (R^* Un S^*)^* = (R Un S)^*";
    9.73 -by(best_tac (set_cs addIs [rtrancl_subset,r_into_rtrancl,
    9.74 +by (best_tac (set_cs addIs [rtrancl_subset,r_into_rtrancl,
    9.75                             rtrancl_mono RS subsetD]) 1);
    9.76  qed "trancl_Un_trancl";
    9.77  
    9.78  goal Trancl.thy "(R^=)^* = R^*";
    9.79 -by(fast_tac (rel_cs addIs [rtrancl_refl,rtrancl_subset,r_into_rtrancl]) 1);
    9.80 +by (fast_tac (rel_cs addIs [rtrancl_refl,rtrancl_subset,r_into_rtrancl]) 1);
    9.81  qed "rtrancl_reflcl";
    9.82  Addsimps [rtrancl_reflcl];
    9.83  
    9.84 @@ -194,20 +194,20 @@
    9.85  by (rtac converseI 1);
    9.86  by (etac rtrancl_induct 1);
    9.87  by (rtac rtrancl_refl 1);
    9.88 -by(fast_tac (rel_cs addIs [r_into_rtrancl,rtrancl_trans]) 1);
    9.89 +by (fast_tac (rel_cs addIs [r_into_rtrancl,rtrancl_trans]) 1);
    9.90  qed "rtrancl_converseD";
    9.91  
    9.92  goal Trancl.thy "!!r. (x,y) : converse(r^*) ==> (x,y) : (converse r)^*";
    9.93  by (dtac converseD 1);
    9.94  by (etac rtrancl_induct 1);
    9.95  by (rtac rtrancl_refl 1);
    9.96 -by(fast_tac (rel_cs addIs [r_into_rtrancl,rtrancl_trans]) 1);
    9.97 +by (fast_tac (rel_cs addIs [r_into_rtrancl,rtrancl_trans]) 1);
    9.98  qed "rtrancl_converseI";
    9.99  
   9.100  goal Trancl.thy "(converse r)^* = converse(r^*)";
   9.101 -by(safe_tac (rel_eq_cs addSIs [rtrancl_converseI]));
   9.102 -by(res_inst_tac [("p","x")] PairE 1);
   9.103 -by(hyp_subst_tac 1);
   9.104 +by (safe_tac (rel_eq_cs addSIs [rtrancl_converseI]));
   9.105 +by (res_inst_tac [("p","x")] PairE 1);
   9.106 +by (hyp_subst_tac 1);
   9.107  by (etac rtrancl_converseD 1);
   9.108  qed "rtrancl_converse";
   9.109  
    10.1 --- a/src/HOL/WF.ML	Wed Mar 06 12:19:16 1996 +0100
    10.2 +++ b/src/HOL/WF.ML	Wed Mar 06 12:52:11 1996 +0100
    10.3 @@ -69,12 +69,12 @@
    10.4    H_cong to expose the equality*)
    10.5  goalw WF.thy [cut_def]
    10.6      "(cut f r x = cut g r x) = (!y. (y,x):r --> f(y)=g(y))";
    10.7 -by(simp_tac (HOL_ss addsimps [expand_fun_eq]
    10.8 +by (simp_tac (HOL_ss addsimps [expand_fun_eq]
    10.9                      setloop (split_tac [expand_if])) 1);
   10.10  qed "cuts_eq";
   10.11  
   10.12  goalw WF.thy [cut_def] "!!x. (x,a):r ==> (cut f r a)(x) = f(x)";
   10.13 -by(asm_simp_tac HOL_ss 1);
   10.14 +by (asm_simp_tac HOL_ss 1);
   10.15  qed "cut_apply";
   10.16  
   10.17  (*** is_recfun ***)
   10.18 @@ -82,7 +82,7 @@
   10.19  goalw WF.thy [is_recfun_def,cut_def]
   10.20      "!!f. [| is_recfun r H a f;  ~(b,a):r |] ==> f(b) = (@z.True)";
   10.21  by (etac ssubst 1);
   10.22 -by(asm_simp_tac HOL_ss 1);
   10.23 +by (asm_simp_tac HOL_ss 1);
   10.24  qed "is_recfun_undef";
   10.25  
   10.26  (*** NOTE! some simplifications need a different finish_tac!! ***)
   10.27 @@ -129,7 +129,7 @@
   10.28    by (wf_ind_tac "a" prems 1);
   10.29    by (res_inst_tac [("f","cut (%y. H (the_recfun r H y) y) r a1")]
   10.30                     is_the_recfun 1);
   10.31 -  by (rewrite_goals_tac [is_recfun_def]);
   10.32 +  by (rewtac is_recfun_def);
   10.33    by (rtac (cuts_eq RS ssubst) 1);
   10.34    by (rtac allI 1);
   10.35    by (rtac impI 1);
    11.1 --- a/src/HOL/subset.ML	Wed Mar 06 12:19:16 1996 +0100
    11.2 +++ b/src/HOL/subset.ML	Wed Mar 06 12:52:11 1996 +0100
    11.3 @@ -13,7 +13,7 @@
    11.4   (fn _=> [ (rtac subsetI 1), (etac insertI2 1) ]);
    11.5  
    11.6  goal Set.thy "!!x. x ~: A ==> (A <= insert x B) = (A <= B)";
    11.7 -by(fast_tac set_cs 1);
    11.8 +by (fast_tac set_cs 1);
    11.9  qed "subset_insert";
   11.10  
   11.11  (*** Big Union -- least upper bound of a set  ***)