# HG changeset patch
# User paulson
# Date 826113131 -3600
# Node ID 6f71b5d467008c1c37fbd8bfb8892c944c3121af
# Parent  4a617e14d12c0afea13cd61ddc302a6aa8502461
Ran expandshort

diff -r 4a617e14d12c -r 6f71b5d46700 src/HOL/Arith.ML
--- a/src/HOL/Arith.ML	Wed Mar 06 12:19:16 1996 +0100
+++ b/src/HOL/Arith.ML	Wed Mar 06 12:52:11 1996 +0100
@@ -19,9 +19,9 @@
 (** pred **)
 
 val prems = goal Arith.thy "n ~= 0 ==> Suc(pred n) = n";
-by(res_inst_tac [("n","n")] natE 1);
-by(cut_facts_tac prems 1);
-by(ALLGOALS Asm_full_simp_tac);
+by (res_inst_tac [("n","n")] natE 1);
+by (cut_facts_tac prems 1);
+by (ALLGOALS Asm_full_simp_tac);
 qed "Suc_pred";
 Addsimps [Suc_pred];
 
@@ -205,12 +205,12 @@
 
 goal Arith.thy "!!m. m<n ==> m mod n = m";
 by (rtac (mod_def1 RS wf_less_trans) 1);
-by(Asm_simp_tac 1);
+by (Asm_simp_tac 1);
 qed "mod_less";
 
 goal Arith.thy "!!m. [| 0<n;  ~m<n |] ==> m mod n = (m-n) mod n";
 by (rtac (mod_def1 RS wf_less_trans) 1);
-by(asm_simp_tac (!simpset addsimps [diff_less, cut_apply, less_eq]) 1);
+by (asm_simp_tac (!simpset addsimps [diff_less, cut_apply, less_eq]) 1);
 qed "mod_geq";
 
 
@@ -223,12 +223,12 @@
 
 goal Arith.thy "!!m. m<n ==> m div n = 0";
 by (rtac (div_def1 RS wf_less_trans) 1);
-by(Asm_simp_tac 1);
+by (Asm_simp_tac 1);
 qed "div_less";
 
 goal Arith.thy "!!M. [| 0<n;  ~m<n |] ==> m div n = Suc((m-n) div n)";
 by (rtac (div_def1 RS wf_less_trans) 1);
-by(asm_simp_tac (!simpset addsimps [diff_less, cut_apply, less_eq]) 1);
+by (asm_simp_tac (!simpset addsimps [diff_less, cut_apply, less_eq]) 1);
 qed "div_geq";
 
 (*Main Result about quotient and remainder.*)
@@ -268,7 +268,7 @@
 qed "Suc_diff_n";
 
 goal Arith.thy "Suc(m)-n = (if m<n then 0 else Suc(m-n))";
-by(simp_tac (!simpset addsimps [less_imp_diff_is_0, not_less_eq, Suc_diff_n]
+by (simp_tac (!simpset addsimps [less_imp_diff_is_0, not_less_eq, Suc_diff_n]
                     setloop (split_tac [expand_if])) 1);
 qed "if_Suc_diff_n";
 
@@ -326,20 +326,20 @@
 bind_thm ("trans_less_add2", le_add2 RSN (2,less_le_trans));
 
 goal Arith.thy "!!i. i+j < (k::nat) ==> i<k";
-be rev_mp 1;
-by(nat_ind_tac "j" 1);
+by (etac rev_mp 1);
+by (nat_ind_tac "j" 1);
 by (ALLGOALS Asm_simp_tac);
-by(fast_tac (HOL_cs addDs [Suc_lessD]) 1);
+by (fast_tac (HOL_cs addDs [Suc_lessD]) 1);
 qed "add_lessD1";
 
 goal Arith.thy "!!k::nat. m <= n ==> m <= n+k";
-by (eresolve_tac [le_trans] 1);
-by (resolve_tac [le_add1] 1);
+by (etac le_trans 1);
+by (rtac le_add1 1);
 qed "le_imp_add_le";
 
 goal Arith.thy "!!k::nat. m < n ==> m < n+k";
-by (eresolve_tac [less_le_trans] 1);
-by (resolve_tac [le_add1] 1);
+by (etac less_le_trans 1);
+by (rtac le_add1 1);
 qed "less_imp_add_less";
 
 goal Arith.thy "m+k<=n --> m<=(n::nat)";
@@ -353,7 +353,7 @@
 by (asm_full_simp_tac
     (!simpset delsimps [add_Suc_right]
                 addsimps ([add_Suc_right RS sym, add_left_cancel] @add_ac)) 1);
-by (eresolve_tac [subst] 1);
+by (etac subst 1);
 by (simp_tac (!simpset addsimps [less_add_Suc1]) 1);
 qed "less_add_eq_less";
 
@@ -389,7 +389,7 @@
 (*non-strict, in 1st argument*)
 goal Arith.thy "!!i j k::nat. i<=j ==> i + k <= j + k";
 by (res_inst_tac [("f", "%j.j+k")] less_mono_imp_le_mono 1);
-by (eresolve_tac [add_less_mono1] 1);
+by (etac add_less_mono1 1);
 by (assume_tac 1);
 qed "add_le_mono1";
 
@@ -398,5 +398,5 @@
 by (etac (add_le_mono1 RS le_trans) 1);
 by (simp_tac (!simpset addsimps [add_commute]) 1);
 (*j moves to the end because it is free while k, l are bound*)
-by (eresolve_tac [add_le_mono1] 1);
+by (etac add_le_mono1 1);
 qed "add_le_mono";
diff -r 4a617e14d12c -r 6f71b5d46700 src/HOL/Lfp.ML
--- a/src/HOL/Lfp.ML	Wed Mar 06 12:19:16 1996 +0100
+++ b/src/HOL/Lfp.ML	Wed Mar 06 12:52:11 1996 +0100
@@ -54,18 +54,18 @@
 val major::prems = goal Lfp.thy
   "[| (a,b) : lfp f; mono f; \
 \     !!a b. (a,b) : f(lfp f Int Collect(split P)) ==> P a b |] ==> P a b";
-by(res_inst_tac [("c1","P")] (split RS subst) 1);
+by (res_inst_tac [("c1","P")] (split RS subst) 1);
 by (rtac (major RS induct) 1);
 by (resolve_tac prems 1);
-by(res_inst_tac[("p","x")]PairE 1);
-by(hyp_subst_tac 1);
-by(asm_simp_tac (!simpset addsimps prems) 1);
+by (res_inst_tac[("p","x")]PairE 1);
+by (hyp_subst_tac 1);
+by (asm_simp_tac (!simpset addsimps prems) 1);
 qed"induct2";
 
 (*** Fixpoint induction a la David Park ***)
 goal Lfp.thy "!!f. [| mono f; f A <= A |] ==> lfp(f) <= A";
 by (rtac subsetI 1);
-by(EVERY[etac induct 1, atac 1, etac subsetD 1, rtac subsetD 1,
+by (EVERY[etac induct 1, atac 1, etac subsetD 1, rtac subsetD 1,
                 atac 2, fast_tac (set_cs addSEs [monoD]) 1]);
 qed "Park_induct";
 
diff -r 4a617e14d12c -r 6f71b5d46700 src/HOL/List.ML
--- a/src/HOL/List.ML	Wed Mar 06 12:19:16 1996 +0100
+++ b/src/HOL/List.ML	Wed Mar 06 12:52:11 1996 +0100
@@ -193,7 +193,7 @@
 qed "drop_0";
 
 goal thy "drop (Suc n) (x#xs) = drop n xs";
-by(Simp_tac 1);
+by (Simp_tac 1);
 qed "drop_Suc_Cons";
 
 Delsimps [drop_Cons];
@@ -207,7 +207,7 @@
 qed "take_0";
 
 goal thy "take (Suc n) (x#xs) = x # take n xs";
-by(Simp_tac 1);
+by (Simp_tac 1);
 qed "take_Suc_Cons";
 
 Delsimps [take_Cons];
diff -r 4a617e14d12c -r 6f71b5d46700 src/HOL/Nat.ML
--- a/src/HOL/Nat.ML	Wed Mar 06 12:19:16 1996 +0100
+++ b/src/HOL/Nat.ML	Wed Mar 06 12:52:11 1996 +0100
@@ -231,7 +231,7 @@
 (** Elimination properties **)
 
 val prems = goalw Nat.thy [less_def] "n<m ==> ~ m<(n::nat)";
-by(fast_tac (HOL_cs addIs ([wf_pred_nat, wf_trancl RS wf_asym]@prems))1);
+by (fast_tac (HOL_cs addIs ([wf_pred_nat, wf_trancl RS wf_asym]@prems))1);
 qed "less_not_sym";
 
 (* [| n(m; m(n |] ==> R *)
@@ -246,7 +246,7 @@
 bind_thm ("less_anti_refl", (less_not_refl RS notE));
 
 goal Nat.thy "!!m. n<m ==> m ~= (n::nat)";
-by(fast_tac (HOL_cs addEs [less_anti_refl]) 1);
+by (fast_tac (HOL_cs addEs [less_anti_refl]) 1);
 qed "less_not_refl2";
 
 
@@ -285,9 +285,9 @@
 qed "less_Suc_eq";
 
 val prems = goal Nat.thy "m<n ==> n ~= 0";
-by(res_inst_tac [("n","n")] natE 1);
-by(cut_facts_tac prems 1);
-by(ALLGOALS Asm_full_simp_tac);
+by (res_inst_tac [("n","n")] natE 1);
+by (cut_facts_tac prems 1);
+by (ALLGOALS Asm_full_simp_tac);
 qed "gr_implies_not0";
 Addsimps [gr_implies_not0];
 
@@ -335,14 +335,14 @@
 Addsimps [Suc_less_eq];
 
 goal Nat.thy "~(Suc(n) < n)";
-by(fast_tac (HOL_cs addEs [Suc_lessD RS less_anti_refl]) 1);
+by (fast_tac (HOL_cs addEs [Suc_lessD RS less_anti_refl]) 1);
 qed "not_Suc_n_less_n";
 Addsimps [not_Suc_n_less_n];
 
 goal Nat.thy "!!i. i<j ==> j<k --> Suc i < k";
-by(nat_ind_tac "k" 1);
-by(ALLGOALS (asm_simp_tac (!simpset addsimps [less_Suc_eq])));
-by(fast_tac (HOL_cs addDs [Suc_lessD]) 1);
+by (nat_ind_tac "k" 1);
+by (ALLGOALS (asm_simp_tac (!simpset addsimps [less_Suc_eq])));
+by (fast_tac (HOL_cs addDs [Suc_lessD]) 1);
 qed_spec_mp "less_trans_Suc";
 
 (*"Less than" is a linear ordering*)
@@ -357,7 +357,7 @@
 (*Can be used with less_Suc_eq to get n=m | n<m *)
 goal Nat.thy "(~ m < n) = (n < Suc(m))";
 by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
-by(ALLGOALS Asm_simp_tac);
+by (ALLGOALS Asm_simp_tac);
 qed "not_less_eq";
 
 (*Complete induction, aka course-of-values induction*)
@@ -375,12 +375,12 @@
 qed "le0";
 
 goalw Nat.thy [le_def] "~ Suc n <= n";
-by(Simp_tac 1);
+by (Simp_tac 1);
 qed "Suc_n_not_le_n";
 
 goalw Nat.thy [le_def] "(i <= 0) = (i = 0)";
-by(nat_ind_tac "i" 1);
-by(ALLGOALS Asm_simp_tac);
+by (nat_ind_tac "i" 1);
+by (ALLGOALS Asm_simp_tac);
 qed "le_0";
 
 Addsimps [less_not_refl,
@@ -413,13 +413,13 @@
 qed "not_leE";
 
 goalw Nat.thy [le_def] "!!m. m < n ==> Suc(m) <= n";
-by(Simp_tac 1);
+by (Simp_tac 1);
 by (fast_tac (HOL_cs addEs [less_anti_refl,less_asym]) 1);
 qed "lessD";
 
 goalw Nat.thy [le_def] "!!m. Suc(m) <= n ==> m <= n";
-by(Asm_full_simp_tac 1);
-by(fast_tac HOL_cs 1);
+by (Asm_full_simp_tac 1);
+by (fast_tac HOL_cs 1);
 qed "Suc_leD";
 
 goalw Nat.thy [le_def] "!!m. m <= n ==> m <= Suc n";
@@ -447,7 +447,7 @@
 qed "le_eq_less_or_eq";
 
 goal Nat.thy "n <= (n::nat)";
-by(simp_tac (!simpset addsimps [le_eq_less_or_eq]) 1);
+by (simp_tac (!simpset addsimps [le_eq_less_or_eq]) 1);
 qed "le_refl";
 
 val prems = goal Nat.thy "!!i. [| i <= j; j < k |] ==> i < (k::nat)";
diff -r 4a617e14d12c -r 6f71b5d46700 src/HOL/Prod.ML
--- a/src/HOL/Prod.ML	Wed Mar 06 12:19:16 1996 +0100
+++ b/src/HOL/Prod.ML	Wed Mar 06 12:52:11 1996 +0100
@@ -78,7 +78,7 @@
 end;
 
 goal Prod.thy "(!x. P x) = (!a b. P(a,b))";
-by(fast_tac (HOL_cs addbefore split_all_tac 1) 1);
+by (fast_tac (HOL_cs addbefore split_all_tac 1) 1);
 qed "split_paired_All";
 
 goalw Prod.thy [split_def] "split c (a,b) = c a b";
@@ -123,7 +123,7 @@
   Could instead call simp_tac/asm_full_simp_tac using split as rewrite.*)
 
 goal Prod.thy "!!p. [| !!a b. p=(a,b) ==> c a b |] ==> split c p";
-by(split_all_tac 1);
+by (split_all_tac 1);
 by (Asm_simp_tac 1);
 qed "splitI2";
 
@@ -145,7 +145,7 @@
 qed "mem_splitI";
 
 goal Prod.thy "!!p. [| !!a b. p=(a,b) ==> z: c a b |] ==> z: split c p";
-by(split_all_tac 1);
+by (split_all_tac 1);
 by (Asm_simp_tac 1);
 qed "mem_splitI2";
 
diff -r 4a617e14d12c -r 6f71b5d46700 src/HOL/RelPow.ML
--- a/src/HOL/RelPow.ML	Wed Mar 06 12:19:16 1996 +0100
+++ b/src/HOL/RelPow.ML	Wed Mar 06 12:52:11 1996 +0100
@@ -10,85 +10,85 @@
 Addsimps [rel_pow_0];
 
 goal RelPow.thy "(x,x) : R^0";
-by(Simp_tac 1);
+by (Simp_tac 1);
 qed "rel_pow_0_I";
 
 goal RelPow.thy "!!R. [| (x,y) : R^n; (y,z):R |] ==> (x,z):R^(Suc n)";
-by(simp_tac (!simpset addsimps [rel_pow_Suc]) 1);
-by(fast_tac comp_cs 1);
+by (simp_tac (!simpset addsimps [rel_pow_Suc]) 1);
+by (fast_tac comp_cs 1);
 qed "rel_pow_Suc_I";
 
 goal RelPow.thy "!z. (x,y) : R --> (y,z):R^n -->  (x,z):R^(Suc n)";
-by(nat_ind_tac "n" 1);
-by(simp_tac (!simpset addsimps [rel_pow_Suc]) 1);
-by(fast_tac comp_cs 1);
-by(asm_full_simp_tac (!simpset addsimps [rel_pow_Suc]) 1);
-by(fast_tac comp_cs 1);
+by (nat_ind_tac "n" 1);
+by (simp_tac (!simpset addsimps [rel_pow_Suc]) 1);
+by (fast_tac comp_cs 1);
+by (asm_full_simp_tac (!simpset addsimps [rel_pow_Suc]) 1);
+by (fast_tac comp_cs 1);
 qed_spec_mp "rel_pow_Suc_I2";
 
 goal RelPow.thy "!!R. [| (x,y) : R^0; x=y ==> P |] ==> P";
-by(Asm_full_simp_tac 1);
+by (Asm_full_simp_tac 1);
 qed "rel_pow_0_E";
 
 val [major,minor] = goal RelPow.thy
   "[| (x,z) : R^(Suc n);  !!y. [| (x,y) : R^n; (y,z) : R |] ==> P |] ==> P";
-by(cut_facts_tac [major] 1);
-by(asm_full_simp_tac (!simpset addsimps [rel_pow_Suc]) 1);
-by(fast_tac (comp_cs addIs [minor]) 1);
+by (cut_facts_tac [major] 1);
+by (asm_full_simp_tac (!simpset addsimps [rel_pow_Suc]) 1);
+by (fast_tac (comp_cs addIs [minor]) 1);
 qed "rel_pow_Suc_E";
 
 val [p1,p2,p3] = goal RelPow.thy
     "[| (x,z) : R^n;  [| n=0; x = z |] ==> P;        \
 \       !!y m. [| n = Suc m; (x,y) : R^m; (y,z) : R |] ==> P  \
 \    |] ==> P";
-by(res_inst_tac [("n","n")] natE 1);
-by(cut_facts_tac [p1] 1);
-by(asm_full_simp_tac (!simpset addsimps [p2]) 1);
-by(cut_facts_tac [p1] 1);
-by(Asm_full_simp_tac 1);
-be rel_pow_Suc_E 1;
-by(REPEAT(ares_tac [p3] 1));
+by (res_inst_tac [("n","n")] natE 1);
+by (cut_facts_tac [p1] 1);
+by (asm_full_simp_tac (!simpset addsimps [p2]) 1);
+by (cut_facts_tac [p1] 1);
+by (Asm_full_simp_tac 1);
+by (etac rel_pow_Suc_E 1);
+by (REPEAT(ares_tac [p3] 1));
 qed "rel_pow_E";
 
 goal RelPow.thy "!x z. (x,z):R^(Suc n) --> (? y. (x,y):R & (y,z):R^n)";
-by(nat_ind_tac "n" 1);
-by(fast_tac (HOL_cs addIs [rel_pow_0_I] addEs [rel_pow_0_E,rel_pow_Suc_E]) 1);
-by(fast_tac (HOL_cs addIs [rel_pow_Suc_I] addEs[rel_pow_0_E,rel_pow_Suc_E]) 1);
+by (nat_ind_tac "n" 1);
+by (fast_tac (HOL_cs addIs [rel_pow_0_I] addEs [rel_pow_0_E,rel_pow_Suc_E]) 1);
+by (fast_tac (HOL_cs addIs [rel_pow_Suc_I] addEs[rel_pow_0_E,rel_pow_Suc_E]) 1);
 qed_spec_mp "rel_pow_Suc_D2";
 
 val [p1,p2,p3] = goal RelPow.thy
     "[| (x,z) : R^n;  [| n=0; x = z |] ==> P;        \
 \       !!y m. [| n = Suc m; (x,y) : R; (y,z) : R^m |] ==> P  \
 \    |] ==> P";
-by(res_inst_tac [("n","n")] natE 1);
-by(cut_facts_tac [p1] 1);
-by(asm_full_simp_tac (!simpset addsimps [p2]) 1);
-by(cut_facts_tac [p1] 1);
-by(Asm_full_simp_tac 1);
-bd rel_pow_Suc_D2 1;
-be exE 1;
-be p3 1;
-be conjunct1 1;
-be conjunct2 1;
+by (res_inst_tac [("n","n")] natE 1);
+by (cut_facts_tac [p1] 1);
+by (asm_full_simp_tac (!simpset addsimps [p2]) 1);
+by (cut_facts_tac [p1] 1);
+by (Asm_full_simp_tac 1);
+by (dtac rel_pow_Suc_D2 1);
+by (etac exE 1);
+by (etac p3 1);
+by (etac conjunct1 1);
+by (etac conjunct2 1);
 qed "rel_pow_E2";
 
 goal RelPow.thy "!!p. p:R^* ==> p : (UN n. R^n)";
-by(split_all_tac 1);
-be rtrancl_induct 1;
-by(ALLGOALS (fast_tac (rel_cs addIs [rel_pow_0_I,rel_pow_Suc_I])));
+by (split_all_tac 1);
+by (etac rtrancl_induct 1);
+by (ALLGOALS (fast_tac (rel_cs addIs [rel_pow_0_I,rel_pow_Suc_I])));
 qed "rtrancl_imp_UN_rel_pow";
 
 goal RelPow.thy "!y. (x,y):R^n --> (x,y):R^*";
-by(nat_ind_tac "n" 1);
-by(fast_tac (HOL_cs addIs [rtrancl_refl] addEs [rel_pow_0_E]) 1);
-by(fast_tac (trancl_cs addEs [rel_pow_Suc_E,rtrancl_into_rtrancl]) 1);
+by (nat_ind_tac "n" 1);
+by (fast_tac (HOL_cs addIs [rtrancl_refl] addEs [rel_pow_0_E]) 1);
+by (fast_tac (trancl_cs addEs [rel_pow_Suc_E,rtrancl_into_rtrancl]) 1);
 val lemma = result() RS spec RS mp;
 
 goal RelPow.thy "!!p. p:R^n ==> p:R^*";
-by(split_all_tac 1);
-be lemma 1;
+by (split_all_tac 1);
+by (etac lemma 1);
 qed "rel_pow_imp_rtrancl";
 
 goal RelPow.thy "R^* = (UN n. R^n)";
-by(fast_tac (eq_cs addIs [rtrancl_imp_UN_rel_pow,rel_pow_imp_rtrancl]) 1);
+by (fast_tac (eq_cs addIs [rtrancl_imp_UN_rel_pow,rel_pow_imp_rtrancl]) 1);
 qed "rtrancl_is_UN_rel_pow";
diff -r 4a617e14d12c -r 6f71b5d46700 src/HOL/Relation.ML
--- a/src/HOL/Relation.ML	Wed Mar 06 12:19:16 1996 +0100
+++ b/src/HOL/Relation.ML	Wed Mar 06 12:52:11 1996 +0100
@@ -27,7 +27,7 @@
 qed "idE";
 
 goalw Relation.thy [id_def] "(a,b):id = (a=b)";
-by(fast_tac prod_cs 1);
+by (fast_tac prod_cs 1);
 qed "pair_in_id_conv";
 
 
diff -r 4a617e14d12c -r 6f71b5d46700 src/HOL/Set.ML
--- a/src/HOL/Set.ML	Wed Mar 06 12:19:16 1996 +0100
+++ b/src/HOL/Set.ML	Wed Mar 06 12:52:11 1996 +0100
@@ -311,7 +311,7 @@
     (REPEAT (eresolve_tac (prems @ [emptyE]) 1)) ]);
 
 goalw Set.thy [insert_def] "!!a. b : {a} ==> b=a";
-by(fast_tac (HOL_cs addSEs [emptyE,CollectE,UnE]) 1);
+by (fast_tac (HOL_cs addSEs [emptyE,CollectE,UnE]) 1);
 qed "singletonD";
 
 val singletonE = make_elim singletonD;
diff -r 4a617e14d12c -r 6f71b5d46700 src/HOL/Trancl.ML
--- a/src/HOL/Trancl.ML	Wed Mar 06 12:19:16 1996 +0100
+++ b/src/HOL/Trancl.ML	Wed Mar 06 12:52:11 1996 +0100
@@ -32,13 +32,13 @@
 
 (*rtrancl of r contains r*)
 goal Trancl.thy "!!p. p : r ==> p : r^*";
-by(split_all_tac 1);
+by (split_all_tac 1);
 by (etac (rtrancl_refl RS rtrancl_into_rtrancl) 1);
 qed "r_into_rtrancl";
 
 (*monotonicity of rtrancl*)
 goalw Trancl.thy [rtrancl_def] "!!r s. r <= s ==> r^* <= s^*";
-by(REPEAT(ares_tac [lfp_mono,Un_mono,comp_mono,subset_refl] 1));
+by (REPEAT(ares_tac [lfp_mono,Un_mono,comp_mono,subset_refl] 1));
 qed "rtrancl_mono";
 
 (** standard induction rule **)
@@ -71,7 +71,7 @@
 (*transitivity of transitive closure!! -- by induction.*)
 goal Trancl.thy "!!r. [| (a,b):r^*; (b,c):r^* |] ==> (a,c):r^*";
 by (eres_inst_tac [("b","c")] rtrancl_induct 1);
-by(ALLGOALS(fast_tac (HOL_cs addIs [rtrancl_into_rtrancl])));
+by (ALLGOALS(fast_tac (HOL_cs addIs [rtrancl_into_rtrancl])));
 qed "rtrancl_trans";
 
 (*elimination of rtrancl -- by induction on a special formula*)
@@ -87,13 +87,13 @@
 qed "rtranclE";
 
 goal Trancl.thy "!!R. (y,z):R^* ==> !x. (x,y):R --> (x,z):R^*";
-be rtrancl_induct 1;
-by(fast_tac (HOL_cs addIs [r_into_rtrancl]) 1);
-by(fast_tac (HOL_cs addEs [rtrancl_into_rtrancl]) 1);
+by (etac rtrancl_induct 1);
+by (fast_tac (HOL_cs addIs [r_into_rtrancl]) 1);
+by (fast_tac (HOL_cs addEs [rtrancl_into_rtrancl]) 1);
 val lemma = result();
 
 goal Trancl.thy  "!!R. [| (x,y) : R;  (y,z) : R^* |] ==> (x,z) : R^*";
-by(fast_tac (HOL_cs addDs [lemma]) 1);
+by (fast_tac (HOL_cs addDs [lemma]) 1);
 qed "rtrancl_into_rtrancl2";
 
 
@@ -163,12 +163,12 @@
 
 goal Trancl.thy "(r^*)^* = r^*";
 by (rtac set_ext 1);
-by(res_inst_tac [("p","x")] PairE 1);
-by(hyp_subst_tac 1);
+by (res_inst_tac [("p","x")] PairE 1);
+by (hyp_subst_tac 1);
 by (rtac iffI 1);
 by (etac rtrancl_induct 1);
 by (rtac rtrancl_refl 1);
-by(fast_tac (HOL_cs addEs [rtrancl_trans]) 1);
+by (fast_tac (HOL_cs addEs [rtrancl_trans]) 1);
 by (etac r_into_rtrancl 1);
 qed "rtrancl_idemp";
 Addsimps [rtrancl_idemp];
@@ -176,17 +176,17 @@
 goal Trancl.thy "!!R. [| R <= S; S <= R^* |] ==> S^* = R^*";
 by (dtac rtrancl_mono 1);
 by (dtac rtrancl_mono 1);
-by(Asm_full_simp_tac 1);
-by(fast_tac eq_cs 1);
+by (Asm_full_simp_tac 1);
+by (fast_tac eq_cs 1);
 qed "rtrancl_subset";
 
 goal Trancl.thy "!!R. (R^* Un S^*)^* = (R Un S)^*";
-by(best_tac (set_cs addIs [rtrancl_subset,r_into_rtrancl,
+by (best_tac (set_cs addIs [rtrancl_subset,r_into_rtrancl,
                            rtrancl_mono RS subsetD]) 1);
 qed "trancl_Un_trancl";
 
 goal Trancl.thy "(R^=)^* = R^*";
-by(fast_tac (rel_cs addIs [rtrancl_refl,rtrancl_subset,r_into_rtrancl]) 1);
+by (fast_tac (rel_cs addIs [rtrancl_refl,rtrancl_subset,r_into_rtrancl]) 1);
 qed "rtrancl_reflcl";
 Addsimps [rtrancl_reflcl];
 
@@ -194,20 +194,20 @@
 by (rtac converseI 1);
 by (etac rtrancl_induct 1);
 by (rtac rtrancl_refl 1);
-by(fast_tac (rel_cs addIs [r_into_rtrancl,rtrancl_trans]) 1);
+by (fast_tac (rel_cs addIs [r_into_rtrancl,rtrancl_trans]) 1);
 qed "rtrancl_converseD";
 
 goal Trancl.thy "!!r. (x,y) : converse(r^*) ==> (x,y) : (converse r)^*";
 by (dtac converseD 1);
 by (etac rtrancl_induct 1);
 by (rtac rtrancl_refl 1);
-by(fast_tac (rel_cs addIs [r_into_rtrancl,rtrancl_trans]) 1);
+by (fast_tac (rel_cs addIs [r_into_rtrancl,rtrancl_trans]) 1);
 qed "rtrancl_converseI";
 
 goal Trancl.thy "(converse r)^* = converse(r^*)";
-by(safe_tac (rel_eq_cs addSIs [rtrancl_converseI]));
-by(res_inst_tac [("p","x")] PairE 1);
-by(hyp_subst_tac 1);
+by (safe_tac (rel_eq_cs addSIs [rtrancl_converseI]));
+by (res_inst_tac [("p","x")] PairE 1);
+by (hyp_subst_tac 1);
 by (etac rtrancl_converseD 1);
 qed "rtrancl_converse";
 
diff -r 4a617e14d12c -r 6f71b5d46700 src/HOL/WF.ML
--- a/src/HOL/WF.ML	Wed Mar 06 12:19:16 1996 +0100
+++ b/src/HOL/WF.ML	Wed Mar 06 12:52:11 1996 +0100
@@ -69,12 +69,12 @@
   H_cong to expose the equality*)
 goalw WF.thy [cut_def]
     "(cut f r x = cut g r x) = (!y. (y,x):r --> f(y)=g(y))";
-by(simp_tac (HOL_ss addsimps [expand_fun_eq]
+by (simp_tac (HOL_ss addsimps [expand_fun_eq]
                     setloop (split_tac [expand_if])) 1);
 qed "cuts_eq";
 
 goalw WF.thy [cut_def] "!!x. (x,a):r ==> (cut f r a)(x) = f(x)";
-by(asm_simp_tac HOL_ss 1);
+by (asm_simp_tac HOL_ss 1);
 qed "cut_apply";
 
 (*** is_recfun ***)
@@ -82,7 +82,7 @@
 goalw WF.thy [is_recfun_def,cut_def]
     "!!f. [| is_recfun r H a f;  ~(b,a):r |] ==> f(b) = (@z.True)";
 by (etac ssubst 1);
-by(asm_simp_tac HOL_ss 1);
+by (asm_simp_tac HOL_ss 1);
 qed "is_recfun_undef";
 
 (*** NOTE! some simplifications need a different finish_tac!! ***)
@@ -129,7 +129,7 @@
   by (wf_ind_tac "a" prems 1);
   by (res_inst_tac [("f","cut (%y. H (the_recfun r H y) y) r a1")]
                    is_the_recfun 1);
-  by (rewrite_goals_tac [is_recfun_def]);
+  by (rewtac is_recfun_def);
   by (rtac (cuts_eq RS ssubst) 1);
   by (rtac allI 1);
   by (rtac impI 1);
diff -r 4a617e14d12c -r 6f71b5d46700 src/HOL/subset.ML
--- a/src/HOL/subset.ML	Wed Mar 06 12:19:16 1996 +0100
+++ b/src/HOL/subset.ML	Wed Mar 06 12:52:11 1996 +0100
@@ -13,7 +13,7 @@
  (fn _=> [ (rtac subsetI 1), (etac insertI2 1) ]);
 
 goal Set.thy "!!x. x ~: A ==> (A <= insert x B) = (A <= B)";
-by(fast_tac set_cs 1);
+by (fast_tac set_cs 1);
 qed "subset_insert";
 
 (*** Big Union -- least upper bound of a set  ***)