# HG changeset patch
# User paulson
# Date 917623572 -3600
# Node ID 484adda70b6524b967b2b48a93025cb4b5ad82db
# Parent  bc2a76ce1ea3454850820ccc5afdf1ce64a69968
expandshort

diff -r bc2a76ce1ea3 -r 484adda70b65 src/HOL/AxClasses/Lattice/Lattice.ML
--- a/src/HOL/AxClasses/Lattice/Lattice.ML	Fri Jan 29 16:23:56 1999 +0100
+++ b/src/HOL/AxClasses/Lattice/Lattice.ML	Fri Jan 29 16:26:12 1999 +0100
@@ -2,7 +2,7 @@
 context HOL.thy;
 
 Goalw [Ex_def] "EX x. P x ==> P (@x. P x)";
-  ba 1;
+  by (assume_tac 1);
 qed "selectI1";
 
 context thy;
diff -r bc2a76ce1ea3 -r 484adda70b65 src/HOL/AxClasses/Lattice/OrdDefs.ML
--- a/src/HOL/AxClasses/Lattice/OrdDefs.ML	Fri Jan 29 16:23:56 1999 +0100
+++ b/src/HOL/AxClasses/Lattice/OrdDefs.ML	Fri Jan 29 16:26:12 1999 +0100
@@ -66,8 +66,8 @@
 qed "le_dual_refl";
 
 Goalw [le_dual_def] "x [= y & y [= z --> x [= (z::'a::quasi_order dual)";
-  br impI 1;
-  br (le_trans RS mp) 1;
+  by (rtac impI 1);
+  by (rtac (le_trans RS mp) 1);
   by (Blast_tac 1);
 qed "le_dual_trans";
 
diff -r bc2a76ce1ea3 -r 484adda70b65 src/HOL/Finite.ML
--- a/src/HOL/Finite.ML	Fri Jan 29 16:23:56 1999 +0100
+++ b/src/HOL/Finite.ML	Fri Jan 29 16:26:12 1999 +0100
@@ -112,7 +112,7 @@
 Addsimps [finite_Diff];
 
 Goal "finite(A - insert a B) = finite(A-B)";
-by(stac Diff_insert 1);
+by (stac Diff_insert 1);
 by (case_tac "a : A-B" 1);
 by (rtac (finite_insert RS sym RS trans) 1);
 by (stac insert_Diff 1);
@@ -331,38 +331,38 @@
 AddSIs cardR.intrs;
 
 Goal "[| (A,n) : cardR |] ==> a : A --> (? m. n = Suc m)";
-be cardR.induct 1;
- by(Blast_tac 1);
-by(Blast_tac 1);
+by (etac cardR.induct 1);
+ by (Blast_tac 1);
+by (Blast_tac 1);
 qed "cardR_SucD";
 
 Goal "(A,m): cardR ==> (!n a. m = Suc n --> a:A --> (A-{a},n) : cardR)";
-be cardR.induct 1;
- by(Auto_tac);
-by(asm_simp_tac (simpset() addsimps [insert_Diff_if]) 1);
-by(Auto_tac);
-by(forward_tac [cardR_SucD] 1);
-by(Blast_tac 1);
+by (etac cardR.induct 1);
+ by (Auto_tac);
+by (asm_simp_tac (simpset() addsimps [insert_Diff_if]) 1);
+by (Auto_tac);
+by (forward_tac [cardR_SucD] 1);
+by (Blast_tac 1);
 val lemma = result();
 
 Goal "[| (insert a A, Suc m) : cardR; a ~: A |] ==> (A,m) : cardR";
-bd lemma 1;
-by(Asm_full_simp_tac 1);
+by (dtac lemma 1);
+by (Asm_full_simp_tac 1);
 val lemma = result();
 
 Goal "(A,m): cardR ==> (!n. (A,n) : cardR --> n=m)";
-be cardR.induct 1;
- by(safe_tac (claset() addSEs [cardR_insertE]));
-by(rename_tac "B b m" 1);
-by(case_tac "a = b" 1);
- by(subgoal_tac "A = B" 1);
-  by(blast_tac (claset() addEs [equalityE]) 2);
- by(Blast_tac 1);
-by(subgoal_tac "? C. A = insert b C & B = insert a C" 1);
- by(res_inst_tac [("x","A Int B")] exI 2);
- by(blast_tac (claset() addEs [equalityE]) 2);
-by(forw_inst_tac [("A","B")] cardR_SucD 1);
-by(blast_tac (claset() addDs [lemma]) 1);
+by (etac cardR.induct 1);
+ by (safe_tac (claset() addSEs [cardR_insertE]));
+by (rename_tac "B b m" 1);
+by (case_tac "a = b" 1);
+ by (subgoal_tac "A = B" 1);
+  by (blast_tac (claset() addEs [equalityE]) 2);
+ by (Blast_tac 1);
+by (subgoal_tac "? C. A = insert b C & B = insert a C" 1);
+ by (res_inst_tac [("x","A Int B")] exI 2);
+ by (blast_tac (claset() addEs [equalityE]) 2);
+by (forw_inst_tac [("A","B")] cardR_SucD 1);
+by (blast_tac (claset() addDs [lemma]) 1);
 qed_spec_mp "cardR_determ";
 
 Goal "(A,n) : cardR ==> finite(A)";
@@ -730,26 +730,26 @@
 (*** setsum ***)
 
 Goalw [setsum_def] "setsum f {} = 0";
-by(Simp_tac 1);
+by (Simp_tac 1);
 qed "setsum_empty";
 Addsimps [setsum_empty];
 
 Goalw [setsum_def]
  "[| finite F; a ~: F |] ==> setsum f (insert a F) = f(a) + setsum f F";
-by(asm_simp_tac (simpset() addsimps [export fold_insert]) 1);
+by (asm_simp_tac (simpset() addsimps [export fold_insert]) 1);
 qed "setsum_insert";
 Addsimps [setsum_insert];
 
 Goalw [setsum_def]
  "[| finite A; finite B; A Int B = {} |] ==> \
 \ setsum f (A Un B) = setsum f A + setsum f B";
-by(asm_simp_tac (simpset() addsimps [export fold_Un_disjoint2]) 1);
+by (asm_simp_tac (simpset() addsimps [export fold_Un_disjoint2]) 1);
 qed_spec_mp "setsum_disj_Un";
 
 Goal "[| finite F |] ==> \
 \     setsum f (F-{a}) = (if a:F then setsum f F - f a else setsum f F)";
-be finite_induct 1;
-by(auto_tac (claset(), simpset() addsimps [insert_Diff_if]));
-by(dres_inst_tac [("a","a")] mk_disjoint_insert 1);
-by(Auto_tac);
+by (etac finite_induct 1);
+by (auto_tac (claset(), simpset() addsimps [insert_Diff_if]));
+by (dres_inst_tac [("a","a")] mk_disjoint_insert 1);
+by (Auto_tac);
 qed_spec_mp "setsum_diff1";
diff -r bc2a76ce1ea3 -r 484adda70b65 src/HOL/Hoare/Examples.ML
--- a/src/HOL/Hoare/Examples.ML	Fri Jan 29 16:23:56 1999 +0100
+++ b/src/HOL/Hoare/Examples.ML	Fri Jan 29 16:26:12 1999 +0100
@@ -14,7 +14,7 @@
 \  INV {s=m*b} \  
 \  DO s := s+b; m := m+1 OD \
 \  {s = a*b}";
-by(hoare_tac (Asm_full_simp_tac) 1);
+by (hoare_tac (Asm_full_simp_tac) 1);
 qed "multiply_by_add";
 
 (*** Euclid's algorithm for GCD ***)
@@ -49,7 +49,7 @@
 \     c := c*a; b := b-1 \
 \ OD \
 \ {c = A^B}";
-by(hoare_tac (Asm_full_simp_tac) 1);
+by (hoare_tac (Asm_full_simp_tac) 1);
 by (exhaust_tac "b" 1);
 by (hyp_subst_tac 1);
 by (asm_full_simp_tac (simpset() addsimps [mod_less]) 1);
@@ -116,7 +116,7 @@
 \ {(i < length A --> A!i = 0) & \
 \  (i = length A --> (!j. j < length A --> A!j ~= 0))}";
 by (hoare_tac Asm_full_simp_tac 1);
-by(blast_tac (claset() addSEs [less_SucE]) 1);
+by (blast_tac (claset() addSEs [less_SucE]) 1);
 qed "zero_search";
 
 (* 
@@ -146,30 +146,30 @@
 \  OD \
 \ {leq A u & (!k. u<k & k<l --> A!k = pivot) & geq A l}";
 (* expand and delete abbreviations first *)
-by(asm_simp_tac HOL_basic_ss 1);
-by(REPEAT(etac thin_rl 1));
+by (asm_simp_tac HOL_basic_ss 1);
+by (REPEAT(etac thin_rl 1));
 by (hoare_tac Asm_full_simp_tac 1);
-    by(asm_full_simp_tac (simpset() addsimps [neq_Nil_conv]) 1);
-    by(Clarify_tac 1);
-    by(asm_full_simp_tac (simpset() addsimps [nth_list_update]) 1);
-   by(blast_tac (claset() addSEs [less_SucE] addIs [Suc_leI]) 1);
-  br conjI 1;
-   by(Clarify_tac 1);
-   bd (pred_less_imp_le RS le_imp_less_Suc) 1;
-   by(blast_tac (claset() addSEs [less_SucE]) 1);
-  br less_imp_diff_less 1;
-  by(Blast_tac 1);
- by(Clarify_tac 1);
- by(asm_simp_tac (simpset() addsimps [nth_list_update]) 1);
- by(Clarify_tac 1);
- by(Simp_tac 1);
-by(Clarify_tac 1);
-by(Asm_simp_tac 1);
-br conjI 1;
- by(Clarify_tac 1);
- br order_antisym 1;
-  by(Asm_simp_tac 1);
- by(Asm_simp_tac 1);
-by(Clarify_tac 1);
-by(Asm_simp_tac 1);
+    by (asm_full_simp_tac (simpset() addsimps [neq_Nil_conv]) 1);
+    by (Clarify_tac 1);
+    by (asm_full_simp_tac (simpset() addsimps [nth_list_update]) 1);
+   by (blast_tac (claset() addSEs [less_SucE] addIs [Suc_leI]) 1);
+  by (rtac conjI 1);
+   by (Clarify_tac 1);
+   by (dtac (pred_less_imp_le RS le_imp_less_Suc) 1);
+   by (blast_tac (claset() addSEs [less_SucE]) 1);
+  by (rtac less_imp_diff_less 1);
+  by (Blast_tac 1);
+ by (Clarify_tac 1);
+ by (asm_simp_tac (simpset() addsimps [nth_list_update]) 1);
+ by (Clarify_tac 1);
+ by (Simp_tac 1);
+by (Clarify_tac 1);
+by (Asm_simp_tac 1);
+by (rtac conjI 1);
+ by (Clarify_tac 1);
+ by (rtac order_antisym 1);
+  by (Asm_simp_tac 1);
+ by (Asm_simp_tac 1);
+by (Clarify_tac 1);
+by (Asm_simp_tac 1);
 qed "Partition";
diff -r bc2a76ce1ea3 -r 484adda70b65 src/HOL/Hoare/Hoare.ML
--- a/src/HOL/Hoare/Hoare.ML	Fri Jan 29 16:23:56 1999 +0100
+++ b/src/HOL/Hoare/Hoare.ML	Fri Jan 29 16:26:12 1999 +0100
@@ -9,43 +9,43 @@
 (*** The proof rules ***)
 
 Goalw [Valid_def] "p <= q ==> Valid p SKIP q";
-by(Auto_tac);
+by (Auto_tac);
 qed "SkipRule";
 
 Goalw [Valid_def] "p <= {s. (f s):q} ==> Valid p (Basic f) q";
-by(Auto_tac);
+by (Auto_tac);
 qed "BasicRule";
 
 Goalw [Valid_def] "[| Valid P c1 Q; Valid Q c2 R |] ==> Valid P (c1;c2) R";
-by(Asm_simp_tac 1);
-by(Blast_tac 1);
+by (Asm_simp_tac 1);
+by (Blast_tac 1);
 qed "SeqRule";
 
 Goalw [Valid_def]
  "[| p <= {s. (s:b --> s:w) & (s~:b --> s:w')}; \
 \    Valid w c1 q; Valid w' c2 q |] \
 \ ==> Valid p (IF b THEN c1 ELSE c2 FI) q";
-by(Asm_simp_tac 1);
-by(Blast_tac 1);
+by (Asm_simp_tac 1);
+by (Blast_tac 1);
 qed "CondRule";
 
 Goal "! s s'. Sem c s s' --> s : I Int b --> s' : I ==> \
 \     ! s s'. s : I --> iter n b (Sem c) s s' --> s' : I & s' ~: b";
-by(induct_tac "n" 1);
- by(Asm_simp_tac 1);
-by(Simp_tac 1);
-by(Blast_tac 1);
+by (induct_tac "n" 1);
+ by (Asm_simp_tac 1);
+by (Simp_tac 1);
+by (Blast_tac 1);
 val lemma = result() RS spec RS spec RS mp RS mp;
 
 Goalw [Valid_def]
  "[| p <= i; Valid (i Int b) c i; (i Int -b) <= q |] \
 \ ==> Valid p (WHILE b INV {i} DO c OD) q";
-by(Asm_simp_tac 1);
-by(Clarify_tac 1);
-bd lemma 1;
-ba 2;
-by(Blast_tac 1);
-by(Blast_tac 1);
+by (Asm_simp_tac 1);
+by (Clarify_tac 1);
+by (dtac lemma 1);
+by (assume_tac 2);
+by (Blast_tac 1);
+by (Blast_tac 1);
 qed "WhileRule";
 
 (*** The tactics ***)
diff -r bc2a76ce1ea3 -r 484adda70b65 src/HOL/IMP/Natural.ML
--- a/src/HOL/IMP/Natural.ML	Fri Jan 29 16:23:56 1999 +0100
+++ b/src/HOL/IMP/Natural.ML	Fri Jan 29 16:26:12 1999 +0100
@@ -31,20 +31,20 @@
 
 Goal "[| !x. P x --> Q x; <w,s> -c-> t |] ==> \
 \ !c. w = While P c --> <While Q c,t> -c-> u --> <While Q c,s> -c-> u";
-be evalc.induct 1;
-by(Auto_tac);
+by (etac evalc.induct 1);
+by (Auto_tac);
 val lemma1 = result() RS spec RS mp RS mp;
 
 Goal "[| !x. P x --> Q x; <w,s> -c-> u |] ==> \
 \ !c. w = While Q c --> <While P c; While Q c,s> -c-> u";
-be evalc.induct 1;
-by(ALLGOALS Asm_simp_tac);
-by(Blast_tac 1);
-by(case_tac "P s" 1);
-by(Auto_tac);
+by (etac evalc.induct 1);
+by (ALLGOALS Asm_simp_tac);
+by (Blast_tac 1);
+by (case_tac "P s" 1);
+by (Auto_tac);
 val lemma2 = result() RS spec RS mp;
 
 Goal "!x. P x --> Q x ==> \
 \ (<While P c; While Q c, s> -c-> t) = (<While Q c, s> -c-> t)";
-by(blast_tac (claset() addIs [lemma1,lemma2]) 1);
+by (blast_tac (claset() addIs [lemma1,lemma2]) 1);
 qed "Hoare_example";
diff -r bc2a76ce1ea3 -r 484adda70b65 src/HOL/Induct/Multiset.ML
--- a/src/HOL/Induct/Multiset.ML	Fri Jan 29 16:23:56 1999 +0100
+++ b/src/HOL/Induct/Multiset.ML	Fri Jan 29 16:26:12 1999 +0100
@@ -9,39 +9,39 @@
 (** Preservation of representing set `multiset' **)
 
 Goalw [multiset_def] "(%a. 0) : multiset";
-by(Simp_tac 1);
+by (Simp_tac 1);
 qed "const0_in_multiset";
 Addsimps [const0_in_multiset];
 
 Goalw [multiset_def] "(%b. if b=a then 1 else 0) : multiset";
-by(Simp_tac 1);
+by (Simp_tac 1);
 qed "only1_in_multiset";
 Addsimps [only1_in_multiset];
 
 Goalw [multiset_def]
  "[| M : multiset; N : multiset |] ==> (%a. M a + N a) : multiset";
-by(Asm_full_simp_tac 1);
-bd finite_UnI 1;
-ba 1;
-by(asm_full_simp_tac (simpset() delsimps [finite_Un]addsimps [Un_def]) 1);
+by (Asm_full_simp_tac 1);
+by (dtac finite_UnI 1);
+by (assume_tac 1);
+by (asm_full_simp_tac (simpset() delsimps [finite_Un]addsimps [Un_def]) 1);
 qed "union_preserves_multiset";
 Addsimps [union_preserves_multiset];
 
 Goalw [multiset_def]
  "[| M : multiset |] ==> (%a. M a - N a) : multiset";
-by(Asm_full_simp_tac 1);
-be (rotate_prems 1 finite_subset) 1;
-by(Auto_tac);
+by (Asm_full_simp_tac 1);
+by (etac (rotate_prems 1 finite_subset) 1);
+by (Auto_tac);
 qed "diff_preserves_multiset";
 Addsimps [diff_preserves_multiset];
 
 (** Injectivity of Rep_multiset **)
 
 Goal "(M = N) = (Rep_multiset M = Rep_multiset N)";
-br iffI 1;
- by(Asm_simp_tac 1);
-by(dres_inst_tac [("f","Abs_multiset")] arg_cong 1);
-by(Asm_full_simp_tac 1);
+by (rtac iffI 1);
+ by (Asm_simp_tac 1);
+by (dres_inst_tac [("f","Abs_multiset")] arg_cong 1);
+by (Asm_full_simp_tac 1);
 qed "multiset_eq_conv_Rep_eq";
 Addsimps [multiset_eq_conv_Rep_eq];
 Addsimps [expand_fun_eq];
@@ -49,13 +49,13 @@
 Goal
  "[| f : multiset; g : multiset |] ==> \
 \ (Abs_multiset f = Abs_multiset g) = (!x. f x = g x)";
-br iffI 1;
- by(dres_inst_tac [("f","Rep_multiset")] arg_cong 1);
- by(Asm_full_simp_tac 1);
-by(subgoal_tac "f = g" 1);
- by(Asm_simp_tac 1);
-br ext 1;
-by(Blast_tac 1);
+by (rtac iffI 1);
+ by (dres_inst_tac [("f","Rep_multiset")] arg_cong 1);
+ by (Asm_full_simp_tac 1);
+by (subgoal_tac "f = g" 1);
+ by (Asm_simp_tac 1);
+by (rtac ext 1);
+by (Blast_tac 1);
 qed "Abs_multiset_eq";
 Addsimps [Abs_multiset_eq];
 *)
@@ -66,18 +66,18 @@
 
 Goalw [union_def,empty_def]
  "M + {#} = M & {#} + M = M";
-by(Simp_tac 1);
+by (Simp_tac 1);
 qed "union_empty";
 Addsimps [union_empty];
 
 Goalw [union_def]
  "(M::'a multiset) + N = N + M";
-by(simp_tac (simpset() addsimps add_ac) 1);
+by (simp_tac (simpset() addsimps add_ac) 1);
 qed "union_comm";
 
 Goalw [union_def]
  "((M::'a multiset)+N)+K = M+(N+K)";
-by(simp_tac (simpset() addsimps add_ac) 1);
+by (simp_tac (simpset() addsimps add_ac) 1);
 qed "union_assoc";
 
 qed_goal "union_lcomm" thy "M+(N+K) = N+((M+K)::'a multiset)"
@@ -90,13 +90,13 @@
 
 Goalw [empty_def,diff_def]
  "M-{#} = M & {#}-M = {#}";
-by(Simp_tac 1);
+by (Simp_tac 1);
 qed "diff_empty";
 Addsimps [diff_empty];
 
 Goalw [union_def,diff_def]
  "M+{#a#}-{#a#} = M";
-by(Simp_tac 1);
+by (Simp_tac 1);
 qed "diff_union_inverse2";
 Addsimps [diff_union_inverse2];
 
@@ -104,57 +104,57 @@
 
 Goalw [count_def,empty_def]
  "count {#} a = 0";
-by(Simp_tac 1);
+by (Simp_tac 1);
 qed "count_empty";
 Addsimps [count_empty];
 
 Goalw [count_def,single_def]
  "count {#b#} a = (if b=a then 1 else 0)";
-by(Simp_tac 1);
+by (Simp_tac 1);
 qed "count_single";
 Addsimps [count_single];
 
 Goalw [count_def,union_def]
  "count (M+N) a = count M a + count N a";
-by(Simp_tac 1);
+by (Simp_tac 1);
 qed "count_union";
 Addsimps [count_union];
 
 Goalw [count_def,diff_def]
  "count (M-N) a = count M a - count N a";
-by(Simp_tac 1);
+by (Simp_tac 1);
 qed "count_diff";
 Addsimps [count_diff];
 
 (* set_of *)
 
 Goalw [set_of_def] "set_of {#} = {}";
-by(Simp_tac 1);
+by (Simp_tac 1);
 qed "set_of_empty";
 Addsimps [set_of_empty];
 
 Goalw [set_of_def]
  "set_of {#b#} = {b}";
-by(Simp_tac 1);
+by (Simp_tac 1);
 qed "set_of_single";
 Addsimps [set_of_single];
 
 Goalw [set_of_def]
  "set_of(M+N) = set_of M Un set_of N";
-by(Auto_tac);
+by (Auto_tac);
 qed "set_of_union";
 Addsimps [set_of_union];
 
 (* size *)
 
 Goalw [size_def] "size {#} = 0";
-by(Simp_tac 1);
+by (Simp_tac 1);
 qed "size_empty";
 Addsimps [size_empty];
 
 Goalw [size_def]
  "size {#b#} = 1";
-by(Simp_tac 1);
+by (Simp_tac 1);
 qed "size_single";
 Addsimps [size_single];
 
@@ -166,99 +166,99 @@
 (* equalities *)
 
 Goalw [count_def] "(M = N) = (!a. count M a = count N a)";
-by(Simp_tac 1);
+by (Simp_tac 1);
 qed "multiset_eq_conv_count_eq";
 
 Goalw [single_def,empty_def] "{#a#} ~= {#}  &  {#} ~= {#a#}";
-by(Simp_tac 1);
+by (Simp_tac 1);
 qed "single_not_empty";
 Addsimps [single_not_empty];
 
 Goalw [single_def] "({#a#}={#b#}) = (a=b)";
-by(Auto_tac);
+by (Auto_tac);
 qed "single_eq_single";
 Addsimps [single_eq_single];
 
 Goalw [union_def,empty_def]
  "(M+N = {#}) = (M = {#} & N = {#})";
-by(Simp_tac 1);
-by(Blast_tac 1);
+by (Simp_tac 1);
+by (Blast_tac 1);
 qed "union_eq_empty";
 AddIffs [union_eq_empty];
 
 Goalw [union_def,empty_def]
  "({#} = M+N) = (M = {#} & N = {#})";
-by(Simp_tac 1);
-by(Blast_tac 1);
+by (Simp_tac 1);
+by (Blast_tac 1);
 qed "empty_eq_union";
 AddIffs [empty_eq_union];
 
 Goalw [union_def]
  "(M+K = N+K) = (M=(N::'a multiset))";
-by(Simp_tac 1);
+by (Simp_tac 1);
 qed "union_right_cancel";
 Addsimps [union_right_cancel];
 
 Goalw [union_def]
  "(K+M = K+N) = (M=(N::'a multiset))";
-by(Simp_tac 1);
+by (Simp_tac 1);
 qed "union_left_cancel";
 Addsimps [union_left_cancel];
 
 Goalw [empty_def,single_def,union_def]
  "(M+N = {#a#}) = (M={#a#} & N={#} | M={#} & N={#a#})";
-by(simp_tac (simpset() addsimps [add_is_1]) 1);
-by(Blast_tac 1);
+by (simp_tac (simpset() addsimps [add_is_1]) 1);
+by (Blast_tac 1);
 qed "union_is_single";
 
 Goalw [empty_def,single_def,union_def]
  "({#a#} = M+N) = ({#a#}=M & N={#} | M={#} & {#a#}=N)";
-by(simp_tac (simpset() addsimps [one_is_add]) 1);
-by(blast_tac (claset() addDs [sym]) 1);
+by (simp_tac (simpset() addsimps [one_is_add]) 1);
+by (blast_tac (claset() addDs [sym]) 1);
 qed "single_is_union";
 
 Goalw [single_def,union_def,diff_def]
  "(M+{#a#} = N+{#b#}) = (M=N & a=b | M = N-{#a#}+{#b#} & N = M-{#b#}+{#a#})";
-by(Simp_tac 1);
-br conjI 1;
- by(Force_tac 1);
-by(Clarify_tac 1);
-br conjI 1;
- by(Blast_tac 1);
-by(Clarify_tac 1);
-br iffI 1;
- br conjI 1;
- by(Clarify_tac 1);
-  br conjI 1;
-   by(asm_full_simp_tac (simpset() addsimps [eq_sym_conv]) 1);
+by (Simp_tac 1);
+by (rtac conjI 1);
+ by (Force_tac 1);
+by (Clarify_tac 1);
+by (rtac conjI 1);
+ by (Blast_tac 1);
+by (Clarify_tac 1);
+by (rtac iffI 1);
+ by (rtac conjI 1);
+ by (Clarify_tac 1);
+  by (rtac conjI 1);
+   by (asm_full_simp_tac (simpset() addsimps [eq_sym_conv]) 1);
 (* PROOF FAILED:
-by(Blast_tac 1);
+by (Blast_tac 1);
 *)
-  by(Fast_tac 1);
- by(Asm_simp_tac 1);
-by(Force_tac 1);
+  by (Fast_tac 1);
+ by (Asm_simp_tac 1);
+by (Force_tac 1);
 qed "add_eq_conv_diff";
 
 (* FIXME
 val prems = Goal
  "[| !!F. [| finite F; !G. G < F --> P G |] ==> P F |] ==> finite F --> P F";
-by(res_inst_tac [("a","F"),("f","%A. if finite A then card A else 0")]
+by (res_inst_tac [("a","F"),("f","%A. if finite A then card A else 0")]
      measure_induct 1);
-by(Clarify_tac 1);
-brs prems 1;
- ba 1;
-by(Clarify_tac 1);
-by(subgoal_tac "finite G" 1);
- by(fast_tac (claset() addDs [finite_subset,order_less_le RS iffD1]) 2);
-be allE 1;
-be impE 1;
- by(Blast_tac 2);
-by(asm_simp_tac (simpset() addsimps [psubset_card]) 1);
+by (Clarify_tac 1);
+by (resolve_tac prems 1);
+ by (assume_tac 1);
+by (Clarify_tac 1);
+by (subgoal_tac "finite G" 1);
+ by (fast_tac (claset() addDs [finite_subset,order_less_le RS iffD1]) 2);
+by (etac allE 1);
+by (etac impE 1);
+ by (Blast_tac 2);
+by (asm_simp_tac (simpset() addsimps [psubset_card]) 1);
 val lemma = result();
 
 val prems = Goal
  "[| finite F; !!F. [| finite F; !G. G < F --> P G |] ==> P F |] ==> P F";
-br (lemma RS mp) 1;
+by (rtac (lemma RS mp) 1);
 by (REPEAT(ares_tac prems 1));
 qed "finite_psubset_induct";
 
@@ -268,65 +268,65 @@
 (** Towards the induction rule **)
 
 Goal "finite F ==> (setsum f F = 0) = (!a:F. f a = 0)";
-be finite_induct 1;
-by(Auto_tac);
+by (etac finite_induct 1);
+by (Auto_tac);
 qed "setsum_0";
 Addsimps [setsum_0];
 
 Goal "finite F ==> setsum f F = Suc n --> (? a:F. 0 < f a)";
-be finite_induct 1;
-by(Auto_tac);
+by (etac finite_induct 1);
+by (Auto_tac);
 val lemma = result();
 
 Goal "[| setsum f F = Suc n; finite F |] ==> ? a:F. 0 < f a";
-bd lemma 1;
-by(Fast_tac 1);
+by (dtac lemma 1);
+by (Fast_tac 1);
 qed "setsum_SucD";
 
 Goal "[| finite F; 0 < f a |] ==> \
 \     setsum (f(a:=f(a)-1)) F = (if a:F then setsum f F - 1 else setsum f F)";
-be finite_induct 1;
-by(Auto_tac);
- by(asm_simp_tac (simpset() addsimps add_ac) 1);
-by(dres_inst_tac [("a","a")] mk_disjoint_insert 1);
-by(Auto_tac);
+by (etac finite_induct 1);
+by (Auto_tac);
+ by (asm_simp_tac (simpset() addsimps add_ac) 1);
+by (dres_inst_tac [("a","a")] mk_disjoint_insert 1);
+by (Auto_tac);
 qed "setsum_decr";
 
 val prems = Goalw [multiset_def]
  "[| P(%a.0); \
 \    !!f b. [| f : multiset; P(f) |] ==> P(f(b:=f(b)+1)) |] \
 \  ==> !f. f : multiset --> setsum f {x. 0 < f x} = n --> P(f)";
-by(induct_tac "n" 1);
- by(Asm_simp_tac 1);
- by(Clarify_tac 1);
- by(subgoal_tac "f = (%a.0)" 1);
-  by(Asm_simp_tac 1);
-  brs prems 1;
- br ext 1;
- by(Force_tac 1);
-by(Clarify_tac 1);
-by(forward_tac [setsum_SucD] 1);
- ba 1;
-by(Clarify_tac 1);
-by(rename_tac "a" 1);
-by(subgoal_tac "finite{x. 0 < (f(a:=f(a)-1)) x}" 1);
- be (rotate_prems 1 finite_subset) 2;
- by(Simp_tac 2);
- by(Blast_tac 2);
-by(subgoal_tac
+by (induct_tac "n" 1);
+ by (Asm_simp_tac 1);
+ by (Clarify_tac 1);
+ by (subgoal_tac "f = (%a.0)" 1);
+  by (Asm_simp_tac 1);
+  by (resolve_tac prems 1);
+ by (rtac ext 1);
+ by (Force_tac 1);
+by (Clarify_tac 1);
+by (forward_tac [setsum_SucD] 1);
+ by (assume_tac 1);
+by (Clarify_tac 1);
+by (rename_tac "a" 1);
+by (subgoal_tac "finite{x. 0 < (f(a:=f(a)-1)) x}" 1);
+ by (etac (rotate_prems 1 finite_subset) 2);
+ by (Simp_tac 2);
+ by (Blast_tac 2);
+by (subgoal_tac
    "f = (f(a:=f(a)-1))(a:=(f(a:=f(a)-1))a+1)" 1);
- br ext 2;
- by(Asm_simp_tac 2);
-by(EVERY1[etac ssubst, resolve_tac prems]);
- by(Blast_tac 1);
-by(EVERY[etac allE 1, etac impE 1, etac mp 2]);
- by(Blast_tac 1);
-by(asm_simp_tac (simpset() addsimps [setsum_decr] delsimps [fun_upd_apply]) 1);
-by(subgoal_tac "{x. x ~= a --> 0 < f x} = {x. 0 < f x}" 1);
- by(Blast_tac 2);
-by(subgoal_tac "{x. x ~= a & 0 < f x} = {x. 0 < f x} - {a}" 1);
- by(Blast_tac 2);
-by(asm_simp_tac (simpset() addsimps [le_imp_diff_is_add,setsum_diff1]
+ by (rtac ext 2);
+ by (Asm_simp_tac 2);
+by (EVERY1[etac ssubst, resolve_tac prems]);
+ by (Blast_tac 1);
+by (EVERY[etac allE 1, etac impE 1, etac mp 2]);
+ by (Blast_tac 1);
+by (asm_simp_tac (simpset() addsimps [setsum_decr] delsimps [fun_upd_apply]) 1);
+by (subgoal_tac "{x. x ~= a --> 0 < f x} = {x. 0 < f x}" 1);
+ by (Blast_tac 2);
+by (subgoal_tac "{x. x ~= a & 0 < f x} = {x. 0 < f x} - {a}" 1);
+ by (Blast_tac 2);
+by (asm_simp_tac (simpset() addsimps [le_imp_diff_is_add,setsum_diff1]
                            addcongs [conj_cong]) 1);
 val lemma = result();
 
@@ -334,22 +334,22 @@
  "[| f : multiset; \
 \    P(%a.0); \
 \    !!f b. [| f : multiset; P(f) |] ==> P(f(b:=f(b)+1)) |] ==> P(f)";
-by(rtac (major RSN (3, lemma RS spec RS mp RS mp)) 1);
-by(REPEAT(ares_tac (refl::prems) 1));
+by (rtac (major RSN (3, lemma RS spec RS mp RS mp)) 1);
+by (REPEAT(ares_tac (refl::prems) 1));
 qed "Rep_multiset_induct";
 
 val [prem1,prem2] = Goalw [union_def,single_def,empty_def]
  "[| P({#}); !!M x. P(M) ==> P(M + {#x#}) |] ==> P(M)";
 by (rtac (Rep_multiset_inverse RS subst) 1);
 by (rtac (Rep_multiset RS Rep_multiset_induct) 1);
- by(rtac prem1 1);
-by(Clarify_tac 1);
-by(subgoal_tac
+ by (rtac prem1 1);
+by (Clarify_tac 1);
+by (subgoal_tac
     "f(b := f b + 1) = (%a. f a + (if a = b then 1 else 0))" 1);
- by(Simp_tac 2);
-be ssubst 1;
-by(etac (Abs_multiset_inverse RS subst) 1);
-by(etac(simplify (simpset()) prem2)1);
+ by (Simp_tac 2);
+by (etac ssubst 1);
+by (etac (Abs_multiset_inverse RS subst) 1);
+by (etac(simplify (simpset()) prem2)1);
 qed "multiset_induct";
 
 Delsimps [multiset_eq_conv_Rep_eq, expand_fun_eq];
@@ -357,14 +357,14 @@
 
 Goal
  "(M+{#a#} = N+{#b#}) = (M = N & a = b | (? K. M = K+{#b#} & N = K+{#a#}))";
-by(simp_tac (simpset() addsimps [add_eq_conv_diff]) 1);
-by(Auto_tac);
+by (simp_tac (simpset() addsimps [add_eq_conv_diff]) 1);
+by (Auto_tac);
 qed "add_eq_conv_ex";
 
 (** order **)
 
 Goalw [mult1_def] "(M, {#}) ~: mult1(r)";
-by(Simp_tac 1);
+by (Simp_tac 1);
 qed "not_less_empty";
 AddIffs [not_less_empty];
 
@@ -372,22 +372,22 @@
  "(N,M0 + {#a#}) : mult1(r) = \
 \ ((? M. (M,M0) : mult1(r) & N = M + {#a#}) | \
 \  (? K. (!b. elem K b --> (b,a) : r) & N = M0 + K))";
-br iffI 1;
- by(asm_full_simp_tac (simpset() addsimps [add_eq_conv_ex]) 1);
- by(Clarify_tac 1);
- be disjE 1;
-  by(Blast_tac 1);
- by(Clarify_tac 1);
- by(res_inst_tac [("x","Ka+K")] exI 1);
- by(simp_tac (simpset() addsimps union_ac) 1);
- by(Blast_tac 1);
-be disjE 1;
- by(Clarify_tac 1);
- by(res_inst_tac [("x","aa")] exI 1);
- by(res_inst_tac [("x","M0+{#a#}")] exI 1);
- by(res_inst_tac [("x","K")] exI 1);
- by(simp_tac (simpset() addsimps union_ac) 1);
-by(Blast_tac 1);
+by (rtac iffI 1);
+ by (asm_full_simp_tac (simpset() addsimps [add_eq_conv_ex]) 1);
+ by (Clarify_tac 1);
+ by (etac disjE 1);
+  by (Blast_tac 1);
+ by (Clarify_tac 1);
+ by (res_inst_tac [("x","Ka+K")] exI 1);
+ by (simp_tac (simpset() addsimps union_ac) 1);
+ by (Blast_tac 1);
+by (etac disjE 1);
+ by (Clarify_tac 1);
+ by (res_inst_tac [("x","aa")] exI 1);
+ by (res_inst_tac [("x","M0+{#a#}")] exI 1);
+ by (res_inst_tac [("x","K")] exI 1);
+ by (simp_tac (simpset() addsimps union_ac) 1);
+by (Blast_tac 1);
 qed "less_add_conv";
 
 Open_locale "MSOrd";
@@ -398,47 +398,47 @@
  "[| !b. (b,a) : r --> (!M : W. M+{#b#} : W); M0 : W; \
 \    !M. (M,M0) : mult1(r) --> M+{#a#} : W |] \
 \ ==> M0+{#a#} : W";
-br accI 1;
-by(rename_tac "N" 1);
-by(full_simp_tac (simpset() addsimps [less_add_conv]) 1);
-be disjE 1;
- by(Blast_tac 1);
-by(Clarify_tac 1);
-by(rotate_tac ~1 1);
-be rev_mp 1;
-by(res_inst_tac [("M","K")] multiset_induct 1);
- by(Asm_simp_tac 1);
-by(simp_tac (simpset() addsimps [union_assoc RS sym]) 1);
-by(Blast_tac 1);
+by (rtac accI 1);
+by (rename_tac "N" 1);
+by (full_simp_tac (simpset() addsimps [less_add_conv]) 1);
+by (etac disjE 1);
+ by (Blast_tac 1);
+by (Clarify_tac 1);
+by (rotate_tac ~1 1);
+by (etac rev_mp 1);
+by (res_inst_tac [("M","K")] multiset_induct 1);
+ by (Asm_simp_tac 1);
+by (simp_tac (simpset() addsimps [union_assoc RS sym]) 1);
+by (Blast_tac 1);
 qed "lemma1";
 
 Goalw [W_def]
  "[| !b. (b,a) : r --> (!M : W. M+{#b#} : W); M : W |] ==> M+{#a#} : W";
-be acc_induct 1;
-by(blast_tac (claset() addIs [export lemma1]) 1);
+by (etac acc_induct 1);
+by (blast_tac (claset() addIs [export lemma1]) 1);
 qed "lemma2";
 
 Goalw [W_def]
  "wf(r) ==> !M:W. M+{#a#} : W";
-by(eres_inst_tac [("a","a")] wf_induct 1);
-by(blast_tac (claset() addIs [export lemma2]) 1);
+by (eres_inst_tac [("a","a")] wf_induct 1);
+by (blast_tac (claset() addIs [export lemma2]) 1);
 qed "lemma3";
 
 Goalw [W_def] "wf(r) ==> M : W";
-by(res_inst_tac [("M","M")] multiset_induct 1);
- br accI 1;
- by(Asm_full_simp_tac 1);
-by(blast_tac (claset() addDs [export lemma3]) 1);
+by (res_inst_tac [("M","M")] multiset_induct 1);
+ by (rtac accI 1);
+ by (Asm_full_simp_tac 1);
+by (blast_tac (claset() addDs [export lemma3]) 1);
 qed "all_accessible";
 
 Close_locale "MSOrd";
 
 Goal "wf(r) ==> wf(mult1 r)";
-by(blast_tac (claset() addIs [acc_wfI, export all_accessible]) 1);
+by (blast_tac (claset() addIs [acc_wfI, export all_accessible]) 1);
 qed "wf_mult1";
 
 Goalw [mult_def] "wf(r) ==> wf(mult r)";
-by(blast_tac (claset() addIs [wf_trancl,wf_mult1]) 1);
+by (blast_tac (claset() addIs [wf_trancl,wf_mult1]) 1);
 qed "wf_mult";
 
 (** Equivalence of mult with the usual (closure-free) def **)
@@ -446,7 +446,7 @@
 (* Badly needed: a linear arithmetic tactic for multisets *)
 
 Goal "elem J a ==> I+J - {#a#} = I + (J-{#a#})";
-by(asm_simp_tac (simpset() addsimps [multiset_eq_conv_count_eq]) 1);
+by (asm_simp_tac (simpset() addsimps [multiset_eq_conv_count_eq]) 1);
 qed "diff_union_single_conv";
 
 (* One direction *)
@@ -454,35 +454,35 @@
  "trans r ==> \
 \ (M,N) : mult r ==> (? I J K. N = I+J & M = I+K & J ~= {#} & \
 \                            (!k : set_of K. ? j : set_of J. (k,j) : r))";
-be converse_trancl_induct 1;
- by(Clarify_tac 1);
- by(res_inst_tac [("x","M0")] exI 1);
- by(Simp_tac 1);
-by(Clarify_tac 1);
-by(case_tac "elem K a" 1);
- by(res_inst_tac [("x","I")] exI 1);
- by(Simp_tac 1);
- by(res_inst_tac [("x","(K - {#a#}) + Ka")] exI 1);
- by(asm_simp_tac (simpset() addsimps [union_assoc RS sym]) 1);
- by(dres_inst_tac[("f","%M. M-{#a#}")] arg_cong 1);
- by(asm_full_simp_tac (simpset() addsimps [diff_union_single_conv]) 1);
- by(full_simp_tac (simpset() addsimps [trans_def]) 1);
- by(Blast_tac 1);
-by(subgoal_tac "elem I a" 1);
- by(res_inst_tac [("x","I-{#a#}")] exI 1);
- by(res_inst_tac [("x","J+{#a#}")] exI 1);
- by(res_inst_tac [("x","K + Ka")] exI 1);
- br conjI 1;
-  by(asm_simp_tac (simpset() addsimps [multiset_eq_conv_count_eq]
+by (etac converse_trancl_induct 1);
+ by (Clarify_tac 1);
+ by (res_inst_tac [("x","M0")] exI 1);
+ by (Simp_tac 1);
+by (Clarify_tac 1);
+by (case_tac "elem K a" 1);
+ by (res_inst_tac [("x","I")] exI 1);
+ by (Simp_tac 1);
+ by (res_inst_tac [("x","(K - {#a#}) + Ka")] exI 1);
+ by (asm_simp_tac (simpset() addsimps [union_assoc RS sym]) 1);
+ by (dres_inst_tac[("f","%M. M-{#a#}")] arg_cong 1);
+ by (asm_full_simp_tac (simpset() addsimps [diff_union_single_conv]) 1);
+ by (full_simp_tac (simpset() addsimps [trans_def]) 1);
+ by (Blast_tac 1);
+by (subgoal_tac "elem I a" 1);
+ by (res_inst_tac [("x","I-{#a#}")] exI 1);
+ by (res_inst_tac [("x","J+{#a#}")] exI 1);
+ by (res_inst_tac [("x","K + Ka")] exI 1);
+ by (rtac conjI 1);
+  by (asm_simp_tac (simpset() addsimps [multiset_eq_conv_count_eq]
                              addsplits [nat_diff_split]) 1);
- br conjI 1;
-  by(dres_inst_tac[("f","%M. M-{#a#}")] arg_cong 1);
-  by(Asm_full_simp_tac 1);
-  by(asm_simp_tac (simpset() addsimps [multiset_eq_conv_count_eq]
+ by (rtac conjI 1);
+  by (dres_inst_tac[("f","%M. M-{#a#}")] arg_cong 1);
+  by (Asm_full_simp_tac 1);
+  by (asm_simp_tac (simpset() addsimps [multiset_eq_conv_count_eq]
                              addsplits [nat_diff_split]) 1);
- by(full_simp_tac (simpset() addsimps [trans_def]) 1);
- by(Blast_tac 1);
-by(subgoal_tac "elem (M0 +{#a#}) a" 1);
- by(Asm_full_simp_tac 1);
-by(Simp_tac 1);
+ by (full_simp_tac (simpset() addsimps [trans_def]) 1);
+ by (Blast_tac 1);
+by (subgoal_tac "elem (M0 +{#a#}) a" 1);
+ by (Asm_full_simp_tac 1);
+by (Simp_tac 1);
 qed "mult_implies_one_step";
diff -r bc2a76ce1ea3 -r 484adda70b65 src/HOL/Lex/RegExp2NA.ML
--- a/src/HOL/Lex/RegExp2NA.ML	Fri Jan 29 16:23:56 1999 +0100
+++ b/src/HOL/Lex/RegExp2NA.ML	Fri Jan 29 16:26:12 1999 +0100
@@ -9,37 +9,37 @@
 (******************************************************)
 
 Goalw [atom_def] "(fin (atom a) q) = (q = [False])";
-by(Simp_tac 1);
+by (Simp_tac 1);
 qed "fin_atom";
 
 Goalw [atom_def] "start (atom a) = [True]";
-by(Simp_tac 1);
+by (Simp_tac 1);
 qed "start_atom";
 
 Goalw [atom_def,step_def]
  "(p,q) : step (atom a) b = (p=[True] & q=[False] & b=a)";
-by(Simp_tac 1);
+by (Simp_tac 1);
 qed "in_step_atom_Some";
 Addsimps [in_step_atom_Some];
 
 Goal
  "([False],[False]) : steps (atom a) w = (w = [])";
 by (induct_tac "w" 1);
- by(Simp_tac 1);
-by(asm_simp_tac (simpset() addsimps [comp_def]) 1);
+ by (Simp_tac 1);
+by (asm_simp_tac (simpset() addsimps [comp_def]) 1);
 qed "False_False_in_steps_atom";
 
 Goal
  "(start (atom a), [False]) : steps (atom a) w = (w = [a])";
 by (induct_tac "w" 1);
- by(asm_simp_tac (simpset() addsimps [start_atom]) 1);
-by(asm_full_simp_tac (simpset()
+ by (asm_simp_tac (simpset() addsimps [start_atom]) 1);
+by (asm_full_simp_tac (simpset()
      addsimps [False_False_in_steps_atom,comp_def,start_atom]) 1);
 qed "start_fin_in_steps_atom";
 
 Goal
  "accepts (atom a) w = (w = [a])";
-by(simp_tac(simpset() addsimps
+by (simp_tac(simpset() addsimps
        [accepts_conv_steps,start_fin_in_steps_atom,fin_atom]) 1);
 qed "accepts_atom";
 
@@ -67,13 +67,13 @@
 Goalw [union_def,step_def]
 "!L R. (True#p,q) : step (union L R) a = (? r. q = True#r & (p,r) : step L a)";
 by (Simp_tac 1);
-by(Blast_tac 1);
+by (Blast_tac 1);
 qed_spec_mp "True_in_step_union";
 
 Goalw [union_def,step_def]
 "!L R. (False#p,q) : step (union L R) a = (? r. q = False#r & (p,r) : step R a)";
 by (Simp_tac 1);
-by(Blast_tac 1);
+by (Blast_tac 1);
 qed_spec_mp "False_in_step_union";
 
 AddIffs [True_in_step_union,False_in_step_union];
@@ -102,8 +102,8 @@
  "!L R. (start(union L R),q) : step(union L R) a = \
 \       (? p. (q = True#p & (start L,p) : step L a) | \
 \             (q = False#p & (start R,p) : step R a))";
-by(Simp_tac 1);
-by(Blast_tac 1);
+by (Simp_tac 1);
+by (Blast_tac 1);
 qed_spec_mp "start_step_union";
 AddIffs [start_step_union];
 
@@ -112,17 +112,17 @@
 \ ( (w = [] & q = start(union L R)) | \
 \   (w ~= [] & (? p.  q = True  # p & (start L,p) : steps L w | \
 \                     q = False # p & (start R,p) : steps R w)))";
-by(exhaust_tac "w" 1);
+by (exhaust_tac "w" 1);
  by (Asm_simp_tac 1);
- by(Blast_tac 1);
+ by (Blast_tac 1);
 by (Asm_simp_tac 1);
-by(Blast_tac 1);
+by (Blast_tac 1);
 qed "steps_union";
 
 Goalw [union_def]
  "!L R. fin (union L R) (start(union L R)) = \
 \       (fin L (start L) | fin R (start R))";
-by(Simp_tac 1);
+by (Simp_tac 1);
 qed_spec_mp "fin_start_union";
 AddIffs [fin_start_union];
 
@@ -130,8 +130,8 @@
  "accepts (union L R) w = (accepts L w | accepts R w)";
 by (simp_tac (simpset() addsimps [accepts_conv_steps,steps_union]) 1);
 (* get rid of case_tac: *)
-by(case_tac "w = []" 1);
-by(Auto_tac);
+by (case_tac "w = []" 1);
+by (Auto_tac);
 qed "accepts_union";
 AddIffs [accepts_union];
 
@@ -160,14 +160,14 @@
 \       ((? r. q=True#r & (p,r): step L a) | \
 \        (fin L p & (? r. q=False#r & (start R,r) : step R a)))";
 by (Simp_tac 1);
-by(Blast_tac 1);
+by (Blast_tac 1);
 qed_spec_mp "True_step_conc";
 
 Goalw [conc_def,step_def]
  "!L R. (False#p,q) : step (conc L R) a = \
 \       (? r. q = False#r & (p,r) : step R a)";
 by (Simp_tac 1);
-by(Blast_tac 1);
+by (Blast_tac 1);
 qed_spec_mp "False_step_conc";
 
 AddIffs [True_step_conc, False_step_conc];
@@ -185,16 +185,16 @@
 
 Goal
  "!!L R. !p. (p,q) : steps L w --> (True#p,True#q) : steps (conc L R) w";
-by(induct_tac "w" 1);
+by (induct_tac "w" 1);
  by (Simp_tac 1);
 by (Simp_tac 1);
-by(Blast_tac 1);
+by (Blast_tac 1);
 qed_spec_mp "True_True_steps_concI";
 
 Goal
  "!L R. (True#p,False#q) : step (conc L R) a = \
 \       (fin L p & (start R,q) : step R a)";
-by(Simp_tac 1);
+by (Simp_tac 1);
 qed "True_False_step_conc";
 AddIffs [True_False_step_conc];
 
@@ -205,26 +205,26 @@
 \            (? r. (p,r) : steps L u & fin L r & \
 \            (? s. (start R,s) : step R a & \
 \            (? t. (s,t) : steps R v & q = False#t)))))";
-by(induct_tac "w" 1);
- by(Simp_tac 1);
-by(Simp_tac 1);
-by(clarify_tac (claset() delrules [disjCI]) 1);
-be disjE 1;
- by(clarify_tac (claset() delrules [disjCI]) 1);
- by(etac allE 1 THEN mp_tac 1);
- be disjE 1;
+by (induct_tac "w" 1);
+ by (Simp_tac 1);
+by (Simp_tac 1);
+by (clarify_tac (claset() delrules [disjCI]) 1);
+by (etac disjE 1);
+ by (clarify_tac (claset() delrules [disjCI]) 1);
+ by (etac allE 1 THEN mp_tac 1);
+ by (etac disjE 1);
   by (Blast_tac 1);
- br disjI2 1;
+ by (rtac disjI2 1);
  by (Clarify_tac 1);
- by(Simp_tac 1);
- by(res_inst_tac[("x","a#u")] exI 1);
- by(Simp_tac 1);
+ by (Simp_tac 1);
+ by (res_inst_tac[("x","a#u")] exI 1);
+ by (Simp_tac 1);
  by (Blast_tac 1);
-br disjI2 1;
+by (rtac disjI2 1);
 by (Clarify_tac 1);
-by(Simp_tac 1);
-by(res_inst_tac[("x","[]")] exI 1);
-by(Simp_tac 1);
+by (Simp_tac 1);
+by (res_inst_tac[("x","[]")] exI 1);
+by (Simp_tac 1);
 by (Blast_tac 1);
 qed_spec_mp "True_steps_concD";
 
@@ -235,7 +235,7 @@
 \            (? r. (p,r) : steps L u & fin L r & \
 \            (? s. (start R,s) : step R a & \
 \            (? t. (s,t) : steps R v & q = False#t)))))";
-by(force_tac (claset() addDs [True_steps_concD]
+by (force_tac (claset() addDs [True_steps_concD]
      addIs [True_True_steps_concI],simpset()) 1);
 qed "True_steps_conc";
 
@@ -243,7 +243,7 @@
 
 Goalw [conc_def]
   "!L R. start(conc L R) = True#start L";
-by(Simp_tac 1);
+by (Simp_tac 1);
 qed_spec_mp "start_conc";
 
 Goalw [conc_def]
@@ -257,27 +257,27 @@
  "accepts (conc L R) w = (? u v. w = u@v & accepts L u & accepts R v)";
 by (simp_tac (simpset() addsimps
      [accepts_conv_steps,True_steps_conc,final_conc,start_conc]) 1);
-br iffI 1;
+by (rtac iffI 1);
  by (Clarify_tac 1);
- be disjE 1;
+ by (etac disjE 1);
   by (Clarify_tac 1);
-  be disjE 1;
-   by(res_inst_tac [("x","w")] exI 1);
-   by(Simp_tac 1);
-   by(Blast_tac 1);
-  by(Blast_tac 1);
- be disjE 1;
-  by(Blast_tac 1);
+  by (etac disjE 1);
+   by (res_inst_tac [("x","w")] exI 1);
+   by (Simp_tac 1);
+   by (Blast_tac 1);
+  by (Blast_tac 1);
+ by (etac disjE 1);
+  by (Blast_tac 1);
  by (Clarify_tac 1);
- by(res_inst_tac [("x","u")] exI 1);
- by(Simp_tac 1);
- by(Blast_tac 1);
+ by (res_inst_tac [("x","u")] exI 1);
+ by (Simp_tac 1);
+ by (Blast_tac 1);
 by (Clarify_tac 1);
-by(exhaust_tac "v" 1);
- by(Asm_full_simp_tac 1);
- by(Blast_tac 1);
-by(Asm_full_simp_tac 1);
-by(Blast_tac 1);
+by (exhaust_tac "v" 1);
+ by (Asm_full_simp_tac 1);
+ by (Blast_tac 1);
+by (Asm_full_simp_tac 1);
+by (Blast_tac 1);
 qed "accepts_conc";
 
 (******************************************************)
@@ -285,19 +285,19 @@
 (******************************************************)
 
 Goalw [epsilon_def,step_def] "step epsilon a = {}";
-by(Simp_tac 1);
-by(Blast_tac 1);
+by (Simp_tac 1);
+by (Blast_tac 1);
 qed "step_epsilon";
 Addsimps [step_epsilon];
 
 Goal "((p,q) : steps epsilon w) = (w=[] & p=q)";
-by(induct_tac "w" 1);
-by(Auto_tac);
+by (induct_tac "w" 1);
+by (Auto_tac);
 qed "steps_epsilon";
 
 Goal "accepts epsilon w = (w = [])";
-by(simp_tac (simpset() addsimps [steps_epsilon,accepts_conv_steps]) 1);
-by(simp_tac (simpset() addsimps [epsilon_def]) 1);
+by (simp_tac (simpset() addsimps [steps_epsilon,accepts_conv_steps]) 1);
+by (simp_tac (simpset() addsimps [epsilon_def]) 1);
 qed "accepts_epsilon";
 AddIffs [accepts_epsilon];
 
@@ -306,41 +306,41 @@
 (******************************************************)
 
 Goalw [plus_def] "!A. start (plus A) = start A";
-by(Simp_tac 1);
+by (Simp_tac 1);
 qed_spec_mp "start_plus";
 Addsimps [start_plus];
 
 Goalw [plus_def] "!A. fin (plus A) = fin A";
-by(Simp_tac 1);
+by (Simp_tac 1);
 qed_spec_mp "fin_plus";
 AddIffs [fin_plus];
 
 Goalw [plus_def,step_def]
   "!A. (p,q) : step A a --> (p,q) : step (plus A) a";
-by(Simp_tac 1);
+by (Simp_tac 1);
 qed_spec_mp "step_plusI";
 
 Goal "!p. (p,q) : steps A w --> (p,q) : steps (plus A) w";
-by(induct_tac "w" 1);
- by(Simp_tac 1);
-by(Simp_tac 1);
-by(blast_tac (claset() addIs [step_plusI]) 1);
+by (induct_tac "w" 1);
+ by (Simp_tac 1);
+by (Simp_tac 1);
+by (blast_tac (claset() addIs [step_plusI]) 1);
 qed_spec_mp "steps_plusI";
 
 Goalw [plus_def,step_def]
  "!A. (p,r): step (plus A) a = \
 \     ( (p,r): step A a | fin A p & (start A,r) : step A a )";
-by(Simp_tac 1);
+by (Simp_tac 1);
 qed_spec_mp "step_plus_conv";
 AddIffs [step_plus_conv];
 
 Goal
  "[| (start A,q) : steps A u; u ~= []; fin A p |] \
 \ ==> (p,q) : steps (plus A) u";
-by(exhaust_tac "u" 1);
- by(Blast_tac 1);
-by(Asm_full_simp_tac 1);
-by(blast_tac (claset() addIs [steps_plusI]) 1);
+by (exhaust_tac "u" 1);
+ by (Blast_tac 1);
+by (Asm_full_simp_tac 1);
+by (blast_tac (claset() addIs [steps_plusI]) 1);
 qed "fin_steps_plusI";
 
 (* reverse list induction! Complicates matters for conc? *)
@@ -349,24 +349,24 @@
 \     (? us v. w = concat us @ v & \
 \              (!u:set us. u ~= [] & accepts A u) & \
 \              (start A,r) : steps A v)";
-by(rev_induct_tac "w" 1);
+by (rev_induct_tac "w" 1);
  by (Simp_tac 1);
- by(res_inst_tac [("x","[]")] exI 1);
+ by (res_inst_tac [("x","[]")] exI 1);
  by (Simp_tac 1);
 by (Simp_tac 1);
 by (Clarify_tac 1);
-by(etac allE 1 THEN mp_tac 1);
+by (etac allE 1 THEN mp_tac 1);
 by (Clarify_tac 1);
-be disjE 1;
- by(res_inst_tac [("x","us")] exI 1);
- by(Asm_simp_tac 1);
- by(Blast_tac 1);
-by(exhaust_tac "v" 1);
- by(res_inst_tac [("x","us")] exI 1);
- by(Asm_full_simp_tac 1);
-by(res_inst_tac [("x","us@[v]")] exI 1);
-by(asm_full_simp_tac (simpset() addsimps [accepts_conv_steps]) 1);
-by(Blast_tac 1);
+by (etac disjE 1);
+ by (res_inst_tac [("x","us")] exI 1);
+ by (Asm_simp_tac 1);
+ by (Blast_tac 1);
+by (exhaust_tac "v" 1);
+ by (res_inst_tac [("x","us")] exI 1);
+ by (Asm_full_simp_tac 1);
+by (res_inst_tac [("x","us@[v]")] exI 1);
+by (asm_full_simp_tac (simpset() addsimps [accepts_conv_steps]) 1);
+by (Blast_tac 1);
 qed_spec_mp "start_steps_plusD";
 
 Goal
@@ -374,54 +374,54 @@
 \     (? us v. w = concat us @ v & \
 \              (!u:set us. accepts A u) & \
 \              (start A,r) : steps A v)";
-by(rev_induct_tac "w" 1);
+by (rev_induct_tac "w" 1);
  by (Simp_tac 1);
- by(res_inst_tac [("x","[]")] exI 1);
+ by (res_inst_tac [("x","[]")] exI 1);
  by (Simp_tac 1);
 by (Simp_tac 1);
 by (Clarify_tac 1);
-by(etac allE 1 THEN mp_tac 1);
+by (etac allE 1 THEN mp_tac 1);
 by (Clarify_tac 1);
-be disjE 1;
- by(res_inst_tac [("x","us")] exI 1);
- by(Asm_simp_tac 1);
- by(Blast_tac 1);
-by(res_inst_tac [("x","us@[v]")] exI 1);
-by(asm_full_simp_tac (simpset() addsimps [accepts_conv_steps]) 1);
-by(Blast_tac 1);
+by (etac disjE 1);
+ by (res_inst_tac [("x","us")] exI 1);
+ by (Asm_simp_tac 1);
+ by (Blast_tac 1);
+by (res_inst_tac [("x","us@[v]")] exI 1);
+by (asm_full_simp_tac (simpset() addsimps [accepts_conv_steps]) 1);
+by (Blast_tac 1);
 qed_spec_mp "start_steps_plusD";
 
 Goal
  "us ~= [] --> (!u : set us. accepts A u) --> accepts (plus A) (concat us)";
-by(simp_tac (simpset() addsimps [accepts_conv_steps]) 1);
-by(rev_induct_tac "us" 1);
- by(Simp_tac 1);
-by(rename_tac "u us" 1);
-by(Simp_tac 1);
+by (simp_tac (simpset() addsimps [accepts_conv_steps]) 1);
+by (rev_induct_tac "us" 1);
+ by (Simp_tac 1);
+by (rename_tac "u us" 1);
+by (Simp_tac 1);
 by (Clarify_tac 1);
-by(case_tac "us = []" 1);
- by(Asm_full_simp_tac 1);
- by(blast_tac (claset() addIs [steps_plusI,fin_steps_plusI]) 1);
+by (case_tac "us = []" 1);
+ by (Asm_full_simp_tac 1);
+ by (blast_tac (claset() addIs [steps_plusI,fin_steps_plusI]) 1);
 by (Clarify_tac 1);
-by(case_tac "u = []" 1);
- by(Asm_full_simp_tac 1);
- by(blast_tac (claset() addIs [steps_plusI,fin_steps_plusI]) 1);
-by(Asm_full_simp_tac 1);
-by(blast_tac (claset() addIs [steps_plusI,fin_steps_plusI]) 1);
+by (case_tac "u = []" 1);
+ by (Asm_full_simp_tac 1);
+ by (blast_tac (claset() addIs [steps_plusI,fin_steps_plusI]) 1);
+by (Asm_full_simp_tac 1);
+by (blast_tac (claset() addIs [steps_plusI,fin_steps_plusI]) 1);
 qed_spec_mp "steps_star_cycle";
 
 Goal
  "accepts (plus A) w = \
 \ (? us. us ~= [] & w = concat us & (!u : set us. accepts A u))";
-br iffI 1;
- by(asm_full_simp_tac (simpset() addsimps [accepts_conv_steps]) 1);
+by (rtac iffI 1);
+ by (asm_full_simp_tac (simpset() addsimps [accepts_conv_steps]) 1);
  by (Clarify_tac 1);
- bd start_steps_plusD 1;
+ by (dtac start_steps_plusD 1);
  by (Clarify_tac 1);
- by(res_inst_tac [("x","us@[v]")] exI 1);
- by(asm_full_simp_tac (simpset() addsimps [accepts_conv_steps]) 1);
- by(Blast_tac 1);
-by(blast_tac (claset() addIs [steps_star_cycle]) 1);
+ by (res_inst_tac [("x","us@[v]")] exI 1);
+ by (asm_full_simp_tac (simpset() addsimps [accepts_conv_steps]) 1);
+ by (Blast_tac 1);
+by (blast_tac (claset() addIs [steps_star_cycle]) 1);
 qed "accepts_plus";
 AddIffs [accepts_plus];
 
@@ -432,24 +432,24 @@
 Goalw [star_def]
 "accepts (star A) w = \
 \ (? us. (!u : set us. accepts A u) & w = concat us)";
-br iffI 1;
+by (rtac iffI 1);
  by (Clarify_tac 1);
- be disjE 1;
-  by(res_inst_tac [("x","[]")] exI 1);
-  by(Simp_tac 1);
-  by(Blast_tac 1);
- by(Blast_tac 1);
-by(Force_tac 1);
+ by (etac disjE 1);
+  by (res_inst_tac [("x","[]")] exI 1);
+  by (Simp_tac 1);
+  by (Blast_tac 1);
+ by (Blast_tac 1);
+by (Force_tac 1);
 qed "accepts_star";
 
 (***** Correctness of r2n *****)
 
 Goal
  "!w. accepts (rexp2na r) w = (w : lang r)";
-by(induct_tac "r" 1);
-    by(simp_tac (simpset() addsimps [accepts_conv_steps]) 1);
-   by(simp_tac(simpset() addsimps [accepts_atom]) 1);
-  by(Asm_simp_tac 1);
- by(asm_simp_tac (simpset() addsimps [accepts_conc,RegSet.conc_def]) 1);
-by(asm_simp_tac (simpset() addsimps [accepts_star,in_star]) 1);
+by (induct_tac "r" 1);
+    by (simp_tac (simpset() addsimps [accepts_conv_steps]) 1);
+   by (simp_tac(simpset() addsimps [accepts_atom]) 1);
+  by (Asm_simp_tac 1);
+ by (asm_simp_tac (simpset() addsimps [accepts_conc,RegSet.conc_def]) 1);
+by (asm_simp_tac (simpset() addsimps [accepts_star,in_star]) 1);
 qed_spec_mp "accepts_rexp2na";
diff -r bc2a76ce1ea3 -r 484adda70b65 src/HOL/Lex/RegSet.ML
--- a/src/HOL/Lex/RegSet.ML	Fri Jan 29 16:23:56 1999 +0100
+++ b/src/HOL/Lex/RegSet.ML	Fri Jan 29 16:26:12 1999 +0100
@@ -16,7 +16,7 @@
 Goal
  "w : star U = (? us. (!u : set(us). u : U) & (w = concat us))";
 by (rtac iffI 1);
- be star.induct 1;
+ by (etac star.induct 1);
   by (res_inst_tac [("x","[]")] exI 1);
   by (Simp_tac 1);
  by (Clarify_tac 1);
diff -r bc2a76ce1ea3 -r 484adda70b65 src/HOL/List.ML
--- a/src/HOL/List.ML	Fri Jan 29 16:23:56 1999 +0100
+++ b/src/HOL/List.ML	Fri Jan 29 16:26:12 1999 +0100
@@ -384,7 +384,7 @@
 
 val prems = Goal "[| P []; !!x xs. P xs ==> P(xs@[x]) |] ==> P xs";
 by (stac (rev_rev_ident RS sym) 1);
-br(read_instantiate [("P","%xs. ?P(rev xs)")]list.induct)1;
+by (res_inst_tac [("list", "rev xs")] list.induct 1);
 by (ALLGOALS Simp_tac);
 by (resolve_tac prems 1);
 by (eresolve_tac prems 1);
@@ -571,7 +571,7 @@
 section "nth";
 
 Goal "(x#xs)!n = (case n of 0 => x | Suc m => xs!m)";
-by(simp_tac (simpset() addsplits [nat.split]) 1);
+by (simp_tac (simpset() addsplits [nat.split]) 1);
 qed "nth_Cons";
 
 Goal "!xs. (xs@ys)!n = (if n < length xs then xs!n else ys!(n - length xs))";
@@ -630,9 +630,9 @@
 Addsimps [length_list_update];
 
 Goal "!i j. i < length xs  --> (xs[i:=x])!j = (if i=j then x else xs!j)";
-by(induct_tac "xs" 1);
- by(Simp_tac 1);
-by(auto_tac (claset(), simpset() addsimps [nth_Cons] addsplits [nat.split]));
+by (induct_tac "xs" 1);
+ by (Simp_tac 1);
+by (auto_tac (claset(), simpset() addsimps [nth_Cons] addsplits [nat.split]));
 qed_spec_mp "nth_list_update";
 
 
@@ -874,13 +874,13 @@
 
 (* Does not terminate! *)
 Goal "[i..j(] = (if i<j then i#[Suc i..j(] else [])";
-by(induct_tac "j" 1);
+by (induct_tac "j" 1);
 by Auto_tac;
 qed "upt_rec";
 
 Goal "j<=i ==> [i..j(] = []";
-by(stac upt_rec 1);
-by(Asm_simp_tac 1);
+by (stac upt_rec 1);
+by (Asm_simp_tac 1);
 qed "upt_conv_Nil";
 Addsimps [upt_conv_Nil];
 
@@ -889,27 +889,27 @@
 qed "upt_Suc";
 
 Goal "i<j ==> [i..j(] = i#[Suc i..j(]";
-br trans 1;
-by(stac upt_rec 1);
-br refl 2;
+by (rtac trans 1);
+by (stac upt_rec 1);
+by (rtac refl 2);
 by (Asm_simp_tac 1);
 qed "upt_conv_Cons";
 
 Goal "length [i..j(] = j-i";
-by(induct_tac "j" 1);
+by (induct_tac "j" 1);
  by (Simp_tac 1);
-by(asm_simp_tac (simpset() addsimps [Suc_diff_le]) 1);
+by (asm_simp_tac (simpset() addsimps [Suc_diff_le]) 1);
 qed "length_upt";
 Addsimps [length_upt];
 
 Goal "i+k < j --> [i..j(] ! k = i+k";
-by(induct_tac "j" 1);
- by(Simp_tac 1);
-by(asm_simp_tac (simpset() addsimps [nth_append,less_diff_conv]@add_ac) 1);
-by(Clarify_tac 1);
-by(subgoal_tac "n=i+k" 1);
- by(Asm_simp_tac 2);
-by(Asm_simp_tac 1);
+by (induct_tac "j" 1);
+ by (Simp_tac 1);
+by (asm_simp_tac (simpset() addsimps [nth_append,less_diff_conv]@add_ac) 1);
+by (Clarify_tac 1);
+by (subgoal_tac "n=i+k" 1);
+ by (Asm_simp_tac 2);
+by (Asm_simp_tac 1);
 qed_spec_mp "nth_upt";
 Addsimps [nth_upt];
 
diff -r bc2a76ce1ea3 -r 484adda70b65 src/HOL/Quot/FRACT.ML
--- a/src/HOL/Quot/FRACT.ML	Fri Jan 29 16:23:56 1999 +0100
+++ b/src/HOL/Quot/FRACT.ML	Fri Jan 29 16:26:12 1999 +0100
@@ -7,11 +7,11 @@
 
 Goalw [per_def,per_NP_def]
 "(op ===)=(%x y. fst(rep_NP x)*snd(rep_NP y)=fst(rep_NP y)*snd(rep_NP x))";
-br refl 1;
+by (rtac refl 1);
 qed "inst_NP_per";
 
 
 Goalw [half_def] "half = <[abs_NP(n,2*n)]>";
-br per_class_eqI 1;
+by (rtac per_class_eqI 1);
 by (simp_tac (simpset() addsimps [inst_NP_per]) 1);
 qed "test";
diff -r bc2a76ce1ea3 -r 484adda70b65 src/HOL/Quot/HQUOT.ML
--- a/src/HOL/Quot/HQUOT.ML	Fri Jan 29 16:23:56 1999 +0100
+++ b/src/HOL/Quot/HQUOT.ML	Fri Jan 29 16:26:12 1999 +0100
@@ -124,33 +124,33 @@
 
 (* theorems for any_in *)
 Goalw [any_in_def,peclass_def] "any_in<[(s::'a::er)]>===s";
-br selectI2 1;
-br refl 1;
+by (rtac selectI2 1);
+by (rtac refl 1);
 by (fold_goals_tac [peclass_def]);
-be er_class_eqE 1;
+by (etac er_class_eqE 1);
 qed "er_any_in_class";
 
 Goalw [any_in_def,peclass_def] "s:D==>any_in<[s]>===s";
-br selectI2 1;
-br refl 1;
+by (rtac selectI2 1);
+by (rtac refl 1);
 by (fold_goals_tac [peclass_def]);
-br per_sym 1;
-be per_class_eqE 1;
-be sym 1;
+by (rtac per_sym 1);
+by (etac per_class_eqE 1);
+by (etac sym 1);
 qed "per_any_in_class";
 
 Goal "<[any_in (s::'a::er quot)]> = s";
-br per_class_all 1;
-br allI 1;
-br (er_any_in_class RS per_class_eqI) 1;
+by (rtac per_class_all 1);
+by (rtac allI 1);
+by (rtac (er_any_in_class RS per_class_eqI) 1);
 qed "er_class_any_in";
 
 (* equivalent theorem for per would need !x.x:D *)
 Goal "!x::'a::per. x:D==><[any_in (q::'a::per quot)]> = q";
-br per_class_all 1;
-br allI 1;
-br (per_any_in_class RS per_class_eqI) 1;
-be spec 1;
+by (rtac per_class_all 1);
+by (rtac allI 1);
+by (rtac (per_any_in_class RS per_class_eqI) 1);
+by (etac spec 1);
 qed "per_class_any_in";
 
 (* is like theorem for class er *)
diff -r bc2a76ce1ea3 -r 484adda70b65 src/HOL/Quot/PER.ML
--- a/src/HOL/Quot/PER.ML	Fri Jan 29 16:23:56 1999 +0100
+++ b/src/HOL/Quot/PER.ML	Fri Jan 29 16:26:12 1999 +0100
@@ -12,7 +12,7 @@
 
 (* Witness that quot is not empty *)
 Goal "?z:{s.? r.!y. y:s=y===r}";
-br CollectI 1;
+by (rtac CollectI 1);
 by (res_inst_tac [("x","x")] exI 1);
 by (rtac allI 1);
 by (rtac mem_Collect_eq 1);
diff -r bc2a76ce1ea3 -r 484adda70b65 src/HOL/Real/Real.ML
--- a/src/HOL/Real/Real.ML	Fri Jan 29 16:23:56 1999 +0100
+++ b/src/HOL/Real/Real.ML	Fri Jan 29 16:26:12 1999 +0100
@@ -243,8 +243,8 @@
 qed "real_less_add_left_cancel";
 
 Goal "[| 0r < x; 0r < y |] ==> 0r < x + y";
-be real_less_trans 1;
-bd real_add_less_mono2 1;
+by (etac real_less_trans 1);
+by (dtac real_add_less_mono2 1);
 by (Full_simp_tac 1);
 qed "real_add_order";
 
@@ -255,9 +255,9 @@
 qed "real_le_add_order";
 
 Goal "[| R1 < S1; R2 < S2 |] ==> R1 + R2 < S1 + (S2::real)";
-bd real_add_less_mono1 1;
-be real_less_trans 1;
-be real_add_less_mono2 1;
+by (dtac real_add_less_mono1 1);
+by (etac real_less_trans 1);
+by (etac real_add_less_mono2 1);
 qed "real_add_less_mono";
 
 Goal "!!(q1::real). q1 <= q2  ==> x + q1 <= x + q2";
@@ -265,8 +265,8 @@
 qed "real_add_left_le_mono1";
 
 Goal "[|i<=j;  k<=l |] ==> i + k <= j + (l::real)";
-bd real_add_le_mono1 1;
-be real_le_trans 1;
+by (dtac real_add_le_mono1 1);
+by (etac real_le_trans 1);
 by (Simp_tac 1);
 qed "real_add_le_mono";
 
diff -r bc2a76ce1ea3 -r 484adda70b65 src/HOL/Trancl.ML
--- a/src/HOL/Trancl.ML	Fri Jan 29 16:23:56 1999 +0100
+++ b/src/HOL/Trancl.ML	Fri Jan 29 16:26:12 1999 +0100
@@ -312,7 +312,7 @@
 \     ==> P(a)";
 by (rtac ((major RS converseI RS trancl_converseI) RS trancl_induct) 1);
  by (resolve_tac prems 1);
- be converseD 1;
+ by (etac converseD 1);
 by (blast_tac (claset() addIs prems addSDs [trancl_converseD])1);
 qed "converse_trancl_induct";