expandshort
authorpaulson
Fri Jan 29 16:26:12 1999 +0100 (1999-01-29)
changeset 6162484adda70b65
parent 6161 bc2a76ce1ea3
child 6163 be8234f37e48
expandshort
src/HOL/AxClasses/Lattice/Lattice.ML
src/HOL/AxClasses/Lattice/OrdDefs.ML
src/HOL/Finite.ML
src/HOL/Hoare/Examples.ML
src/HOL/Hoare/Hoare.ML
src/HOL/IMP/Natural.ML
src/HOL/Induct/Multiset.ML
src/HOL/Lex/RegExp2NA.ML
src/HOL/Lex/RegSet.ML
src/HOL/List.ML
src/HOL/Quot/FRACT.ML
src/HOL/Quot/HQUOT.ML
src/HOL/Quot/PER.ML
src/HOL/Real/Real.ML
src/HOL/Trancl.ML
     1.1 --- a/src/HOL/AxClasses/Lattice/Lattice.ML	Fri Jan 29 16:23:56 1999 +0100
     1.2 +++ b/src/HOL/AxClasses/Lattice/Lattice.ML	Fri Jan 29 16:26:12 1999 +0100
     1.3 @@ -2,7 +2,7 @@
     1.4  context HOL.thy;
     1.5  
     1.6  Goalw [Ex_def] "EX x. P x ==> P (@x. P x)";
     1.7 -  ba 1;
     1.8 +  by (assume_tac 1);
     1.9  qed "selectI1";
    1.10  
    1.11  context thy;
     2.1 --- a/src/HOL/AxClasses/Lattice/OrdDefs.ML	Fri Jan 29 16:23:56 1999 +0100
     2.2 +++ b/src/HOL/AxClasses/Lattice/OrdDefs.ML	Fri Jan 29 16:26:12 1999 +0100
     2.3 @@ -66,8 +66,8 @@
     2.4  qed "le_dual_refl";
     2.5  
     2.6  Goalw [le_dual_def] "x [= y & y [= z --> x [= (z::'a::quasi_order dual)";
     2.7 -  br impI 1;
     2.8 -  br (le_trans RS mp) 1;
     2.9 +  by (rtac impI 1);
    2.10 +  by (rtac (le_trans RS mp) 1);
    2.11    by (Blast_tac 1);
    2.12  qed "le_dual_trans";
    2.13  
     3.1 --- a/src/HOL/Finite.ML	Fri Jan 29 16:23:56 1999 +0100
     3.2 +++ b/src/HOL/Finite.ML	Fri Jan 29 16:26:12 1999 +0100
     3.3 @@ -112,7 +112,7 @@
     3.4  Addsimps [finite_Diff];
     3.5  
     3.6  Goal "finite(A - insert a B) = finite(A-B)";
     3.7 -by(stac Diff_insert 1);
     3.8 +by (stac Diff_insert 1);
     3.9  by (case_tac "a : A-B" 1);
    3.10  by (rtac (finite_insert RS sym RS trans) 1);
    3.11  by (stac insert_Diff 1);
    3.12 @@ -331,38 +331,38 @@
    3.13  AddSIs cardR.intrs;
    3.14  
    3.15  Goal "[| (A,n) : cardR |] ==> a : A --> (? m. n = Suc m)";
    3.16 -be cardR.induct 1;
    3.17 - by(Blast_tac 1);
    3.18 -by(Blast_tac 1);
    3.19 +by (etac cardR.induct 1);
    3.20 + by (Blast_tac 1);
    3.21 +by (Blast_tac 1);
    3.22  qed "cardR_SucD";
    3.23  
    3.24  Goal "(A,m): cardR ==> (!n a. m = Suc n --> a:A --> (A-{a},n) : cardR)";
    3.25 -be cardR.induct 1;
    3.26 - by(Auto_tac);
    3.27 -by(asm_simp_tac (simpset() addsimps [insert_Diff_if]) 1);
    3.28 -by(Auto_tac);
    3.29 -by(forward_tac [cardR_SucD] 1);
    3.30 -by(Blast_tac 1);
    3.31 +by (etac cardR.induct 1);
    3.32 + by (Auto_tac);
    3.33 +by (asm_simp_tac (simpset() addsimps [insert_Diff_if]) 1);
    3.34 +by (Auto_tac);
    3.35 +by (forward_tac [cardR_SucD] 1);
    3.36 +by (Blast_tac 1);
    3.37  val lemma = result();
    3.38  
    3.39  Goal "[| (insert a A, Suc m) : cardR; a ~: A |] ==> (A,m) : cardR";
    3.40 -bd lemma 1;
    3.41 -by(Asm_full_simp_tac 1);
    3.42 +by (dtac lemma 1);
    3.43 +by (Asm_full_simp_tac 1);
    3.44  val lemma = result();
    3.45  
    3.46  Goal "(A,m): cardR ==> (!n. (A,n) : cardR --> n=m)";
    3.47 -be cardR.induct 1;
    3.48 - by(safe_tac (claset() addSEs [cardR_insertE]));
    3.49 -by(rename_tac "B b m" 1);
    3.50 -by(case_tac "a = b" 1);
    3.51 - by(subgoal_tac "A = B" 1);
    3.52 -  by(blast_tac (claset() addEs [equalityE]) 2);
    3.53 - by(Blast_tac 1);
    3.54 -by(subgoal_tac "? C. A = insert b C & B = insert a C" 1);
    3.55 - by(res_inst_tac [("x","A Int B")] exI 2);
    3.56 - by(blast_tac (claset() addEs [equalityE]) 2);
    3.57 -by(forw_inst_tac [("A","B")] cardR_SucD 1);
    3.58 -by(blast_tac (claset() addDs [lemma]) 1);
    3.59 +by (etac cardR.induct 1);
    3.60 + by (safe_tac (claset() addSEs [cardR_insertE]));
    3.61 +by (rename_tac "B b m" 1);
    3.62 +by (case_tac "a = b" 1);
    3.63 + by (subgoal_tac "A = B" 1);
    3.64 +  by (blast_tac (claset() addEs [equalityE]) 2);
    3.65 + by (Blast_tac 1);
    3.66 +by (subgoal_tac "? C. A = insert b C & B = insert a C" 1);
    3.67 + by (res_inst_tac [("x","A Int B")] exI 2);
    3.68 + by (blast_tac (claset() addEs [equalityE]) 2);
    3.69 +by (forw_inst_tac [("A","B")] cardR_SucD 1);
    3.70 +by (blast_tac (claset() addDs [lemma]) 1);
    3.71  qed_spec_mp "cardR_determ";
    3.72  
    3.73  Goal "(A,n) : cardR ==> finite(A)";
    3.74 @@ -730,26 +730,26 @@
    3.75  (*** setsum ***)
    3.76  
    3.77  Goalw [setsum_def] "setsum f {} = 0";
    3.78 -by(Simp_tac 1);
    3.79 +by (Simp_tac 1);
    3.80  qed "setsum_empty";
    3.81  Addsimps [setsum_empty];
    3.82  
    3.83  Goalw [setsum_def]
    3.84   "[| finite F; a ~: F |] ==> setsum f (insert a F) = f(a) + setsum f F";
    3.85 -by(asm_simp_tac (simpset() addsimps [export fold_insert]) 1);
    3.86 +by (asm_simp_tac (simpset() addsimps [export fold_insert]) 1);
    3.87  qed "setsum_insert";
    3.88  Addsimps [setsum_insert];
    3.89  
    3.90  Goalw [setsum_def]
    3.91   "[| finite A; finite B; A Int B = {} |] ==> \
    3.92  \ setsum f (A Un B) = setsum f A + setsum f B";
    3.93 -by(asm_simp_tac (simpset() addsimps [export fold_Un_disjoint2]) 1);
    3.94 +by (asm_simp_tac (simpset() addsimps [export fold_Un_disjoint2]) 1);
    3.95  qed_spec_mp "setsum_disj_Un";
    3.96  
    3.97  Goal "[| finite F |] ==> \
    3.98  \     setsum f (F-{a}) = (if a:F then setsum f F - f a else setsum f F)";
    3.99 -be finite_induct 1;
   3.100 -by(auto_tac (claset(), simpset() addsimps [insert_Diff_if]));
   3.101 -by(dres_inst_tac [("a","a")] mk_disjoint_insert 1);
   3.102 -by(Auto_tac);
   3.103 +by (etac finite_induct 1);
   3.104 +by (auto_tac (claset(), simpset() addsimps [insert_Diff_if]));
   3.105 +by (dres_inst_tac [("a","a")] mk_disjoint_insert 1);
   3.106 +by (Auto_tac);
   3.107  qed_spec_mp "setsum_diff1";
     4.1 --- a/src/HOL/Hoare/Examples.ML	Fri Jan 29 16:23:56 1999 +0100
     4.2 +++ b/src/HOL/Hoare/Examples.ML	Fri Jan 29 16:26:12 1999 +0100
     4.3 @@ -14,7 +14,7 @@
     4.4  \  INV {s=m*b} \  
     4.5  \  DO s := s+b; m := m+1 OD \
     4.6  \  {s = a*b}";
     4.7 -by(hoare_tac (Asm_full_simp_tac) 1);
     4.8 +by (hoare_tac (Asm_full_simp_tac) 1);
     4.9  qed "multiply_by_add";
    4.10  
    4.11  (*** Euclid's algorithm for GCD ***)
    4.12 @@ -49,7 +49,7 @@
    4.13  \     c := c*a; b := b-1 \
    4.14  \ OD \
    4.15  \ {c = A^B}";
    4.16 -by(hoare_tac (Asm_full_simp_tac) 1);
    4.17 +by (hoare_tac (Asm_full_simp_tac) 1);
    4.18  by (exhaust_tac "b" 1);
    4.19  by (hyp_subst_tac 1);
    4.20  by (asm_full_simp_tac (simpset() addsimps [mod_less]) 1);
    4.21 @@ -116,7 +116,7 @@
    4.22  \ {(i < length A --> A!i = 0) & \
    4.23  \  (i = length A --> (!j. j < length A --> A!j ~= 0))}";
    4.24  by (hoare_tac Asm_full_simp_tac 1);
    4.25 -by(blast_tac (claset() addSEs [less_SucE]) 1);
    4.26 +by (blast_tac (claset() addSEs [less_SucE]) 1);
    4.27  qed "zero_search";
    4.28  
    4.29  (* 
    4.30 @@ -146,30 +146,30 @@
    4.31  \  OD \
    4.32  \ {leq A u & (!k. u<k & k<l --> A!k = pivot) & geq A l}";
    4.33  (* expand and delete abbreviations first *)
    4.34 -by(asm_simp_tac HOL_basic_ss 1);
    4.35 -by(REPEAT(etac thin_rl 1));
    4.36 +by (asm_simp_tac HOL_basic_ss 1);
    4.37 +by (REPEAT(etac thin_rl 1));
    4.38  by (hoare_tac Asm_full_simp_tac 1);
    4.39 -    by(asm_full_simp_tac (simpset() addsimps [neq_Nil_conv]) 1);
    4.40 -    by(Clarify_tac 1);
    4.41 -    by(asm_full_simp_tac (simpset() addsimps [nth_list_update]) 1);
    4.42 -   by(blast_tac (claset() addSEs [less_SucE] addIs [Suc_leI]) 1);
    4.43 -  br conjI 1;
    4.44 -   by(Clarify_tac 1);
    4.45 -   bd (pred_less_imp_le RS le_imp_less_Suc) 1;
    4.46 -   by(blast_tac (claset() addSEs [less_SucE]) 1);
    4.47 -  br less_imp_diff_less 1;
    4.48 -  by(Blast_tac 1);
    4.49 - by(Clarify_tac 1);
    4.50 - by(asm_simp_tac (simpset() addsimps [nth_list_update]) 1);
    4.51 - by(Clarify_tac 1);
    4.52 - by(Simp_tac 1);
    4.53 -by(Clarify_tac 1);
    4.54 -by(Asm_simp_tac 1);
    4.55 -br conjI 1;
    4.56 - by(Clarify_tac 1);
    4.57 - br order_antisym 1;
    4.58 -  by(Asm_simp_tac 1);
    4.59 - by(Asm_simp_tac 1);
    4.60 -by(Clarify_tac 1);
    4.61 -by(Asm_simp_tac 1);
    4.62 +    by (asm_full_simp_tac (simpset() addsimps [neq_Nil_conv]) 1);
    4.63 +    by (Clarify_tac 1);
    4.64 +    by (asm_full_simp_tac (simpset() addsimps [nth_list_update]) 1);
    4.65 +   by (blast_tac (claset() addSEs [less_SucE] addIs [Suc_leI]) 1);
    4.66 +  by (rtac conjI 1);
    4.67 +   by (Clarify_tac 1);
    4.68 +   by (dtac (pred_less_imp_le RS le_imp_less_Suc) 1);
    4.69 +   by (blast_tac (claset() addSEs [less_SucE]) 1);
    4.70 +  by (rtac less_imp_diff_less 1);
    4.71 +  by (Blast_tac 1);
    4.72 + by (Clarify_tac 1);
    4.73 + by (asm_simp_tac (simpset() addsimps [nth_list_update]) 1);
    4.74 + by (Clarify_tac 1);
    4.75 + by (Simp_tac 1);
    4.76 +by (Clarify_tac 1);
    4.77 +by (Asm_simp_tac 1);
    4.78 +by (rtac conjI 1);
    4.79 + by (Clarify_tac 1);
    4.80 + by (rtac order_antisym 1);
    4.81 +  by (Asm_simp_tac 1);
    4.82 + by (Asm_simp_tac 1);
    4.83 +by (Clarify_tac 1);
    4.84 +by (Asm_simp_tac 1);
    4.85  qed "Partition";
     5.1 --- a/src/HOL/Hoare/Hoare.ML	Fri Jan 29 16:23:56 1999 +0100
     5.2 +++ b/src/HOL/Hoare/Hoare.ML	Fri Jan 29 16:26:12 1999 +0100
     5.3 @@ -9,43 +9,43 @@
     5.4  (*** The proof rules ***)
     5.5  
     5.6  Goalw [Valid_def] "p <= q ==> Valid p SKIP q";
     5.7 -by(Auto_tac);
     5.8 +by (Auto_tac);
     5.9  qed "SkipRule";
    5.10  
    5.11  Goalw [Valid_def] "p <= {s. (f s):q} ==> Valid p (Basic f) q";
    5.12 -by(Auto_tac);
    5.13 +by (Auto_tac);
    5.14  qed "BasicRule";
    5.15  
    5.16  Goalw [Valid_def] "[| Valid P c1 Q; Valid Q c2 R |] ==> Valid P (c1;c2) R";
    5.17 -by(Asm_simp_tac 1);
    5.18 -by(Blast_tac 1);
    5.19 +by (Asm_simp_tac 1);
    5.20 +by (Blast_tac 1);
    5.21  qed "SeqRule";
    5.22  
    5.23  Goalw [Valid_def]
    5.24   "[| p <= {s. (s:b --> s:w) & (s~:b --> s:w')}; \
    5.25  \    Valid w c1 q; Valid w' c2 q |] \
    5.26  \ ==> Valid p (IF b THEN c1 ELSE c2 FI) q";
    5.27 -by(Asm_simp_tac 1);
    5.28 -by(Blast_tac 1);
    5.29 +by (Asm_simp_tac 1);
    5.30 +by (Blast_tac 1);
    5.31  qed "CondRule";
    5.32  
    5.33  Goal "! s s'. Sem c s s' --> s : I Int b --> s' : I ==> \
    5.34  \     ! s s'. s : I --> iter n b (Sem c) s s' --> s' : I & s' ~: b";
    5.35 -by(induct_tac "n" 1);
    5.36 - by(Asm_simp_tac 1);
    5.37 -by(Simp_tac 1);
    5.38 -by(Blast_tac 1);
    5.39 +by (induct_tac "n" 1);
    5.40 + by (Asm_simp_tac 1);
    5.41 +by (Simp_tac 1);
    5.42 +by (Blast_tac 1);
    5.43  val lemma = result() RS spec RS spec RS mp RS mp;
    5.44  
    5.45  Goalw [Valid_def]
    5.46   "[| p <= i; Valid (i Int b) c i; (i Int -b) <= q |] \
    5.47  \ ==> Valid p (WHILE b INV {i} DO c OD) q";
    5.48 -by(Asm_simp_tac 1);
    5.49 -by(Clarify_tac 1);
    5.50 -bd lemma 1;
    5.51 -ba 2;
    5.52 -by(Blast_tac 1);
    5.53 -by(Blast_tac 1);
    5.54 +by (Asm_simp_tac 1);
    5.55 +by (Clarify_tac 1);
    5.56 +by (dtac lemma 1);
    5.57 +by (assume_tac 2);
    5.58 +by (Blast_tac 1);
    5.59 +by (Blast_tac 1);
    5.60  qed "WhileRule";
    5.61  
    5.62  (*** The tactics ***)
     6.1 --- a/src/HOL/IMP/Natural.ML	Fri Jan 29 16:23:56 1999 +0100
     6.2 +++ b/src/HOL/IMP/Natural.ML	Fri Jan 29 16:26:12 1999 +0100
     6.3 @@ -31,20 +31,20 @@
     6.4  
     6.5  Goal "[| !x. P x --> Q x; <w,s> -c-> t |] ==> \
     6.6  \ !c. w = While P c --> <While Q c,t> -c-> u --> <While Q c,s> -c-> u";
     6.7 -be evalc.induct 1;
     6.8 -by(Auto_tac);
     6.9 +by (etac evalc.induct 1);
    6.10 +by (Auto_tac);
    6.11  val lemma1 = result() RS spec RS mp RS mp;
    6.12  
    6.13  Goal "[| !x. P x --> Q x; <w,s> -c-> u |] ==> \
    6.14  \ !c. w = While Q c --> <While P c; While Q c,s> -c-> u";
    6.15 -be evalc.induct 1;
    6.16 -by(ALLGOALS Asm_simp_tac);
    6.17 -by(Blast_tac 1);
    6.18 -by(case_tac "P s" 1);
    6.19 -by(Auto_tac);
    6.20 +by (etac evalc.induct 1);
    6.21 +by (ALLGOALS Asm_simp_tac);
    6.22 +by (Blast_tac 1);
    6.23 +by (case_tac "P s" 1);
    6.24 +by (Auto_tac);
    6.25  val lemma2 = result() RS spec RS mp;
    6.26  
    6.27  Goal "!x. P x --> Q x ==> \
    6.28  \ (<While P c; While Q c, s> -c-> t) = (<While Q c, s> -c-> t)";
    6.29 -by(blast_tac (claset() addIs [lemma1,lemma2]) 1);
    6.30 +by (blast_tac (claset() addIs [lemma1,lemma2]) 1);
    6.31  qed "Hoare_example";
     7.1 --- a/src/HOL/Induct/Multiset.ML	Fri Jan 29 16:23:56 1999 +0100
     7.2 +++ b/src/HOL/Induct/Multiset.ML	Fri Jan 29 16:26:12 1999 +0100
     7.3 @@ -9,39 +9,39 @@
     7.4  (** Preservation of representing set `multiset' **)
     7.5  
     7.6  Goalw [multiset_def] "(%a. 0) : multiset";
     7.7 -by(Simp_tac 1);
     7.8 +by (Simp_tac 1);
     7.9  qed "const0_in_multiset";
    7.10  Addsimps [const0_in_multiset];
    7.11  
    7.12  Goalw [multiset_def] "(%b. if b=a then 1 else 0) : multiset";
    7.13 -by(Simp_tac 1);
    7.14 +by (Simp_tac 1);
    7.15  qed "only1_in_multiset";
    7.16  Addsimps [only1_in_multiset];
    7.17  
    7.18  Goalw [multiset_def]
    7.19   "[| M : multiset; N : multiset |] ==> (%a. M a + N a) : multiset";
    7.20 -by(Asm_full_simp_tac 1);
    7.21 -bd finite_UnI 1;
    7.22 -ba 1;
    7.23 -by(asm_full_simp_tac (simpset() delsimps [finite_Un]addsimps [Un_def]) 1);
    7.24 +by (Asm_full_simp_tac 1);
    7.25 +by (dtac finite_UnI 1);
    7.26 +by (assume_tac 1);
    7.27 +by (asm_full_simp_tac (simpset() delsimps [finite_Un]addsimps [Un_def]) 1);
    7.28  qed "union_preserves_multiset";
    7.29  Addsimps [union_preserves_multiset];
    7.30  
    7.31  Goalw [multiset_def]
    7.32   "[| M : multiset |] ==> (%a. M a - N a) : multiset";
    7.33 -by(Asm_full_simp_tac 1);
    7.34 -be (rotate_prems 1 finite_subset) 1;
    7.35 -by(Auto_tac);
    7.36 +by (Asm_full_simp_tac 1);
    7.37 +by (etac (rotate_prems 1 finite_subset) 1);
    7.38 +by (Auto_tac);
    7.39  qed "diff_preserves_multiset";
    7.40  Addsimps [diff_preserves_multiset];
    7.41  
    7.42  (** Injectivity of Rep_multiset **)
    7.43  
    7.44  Goal "(M = N) = (Rep_multiset M = Rep_multiset N)";
    7.45 -br iffI 1;
    7.46 - by(Asm_simp_tac 1);
    7.47 -by(dres_inst_tac [("f","Abs_multiset")] arg_cong 1);
    7.48 -by(Asm_full_simp_tac 1);
    7.49 +by (rtac iffI 1);
    7.50 + by (Asm_simp_tac 1);
    7.51 +by (dres_inst_tac [("f","Abs_multiset")] arg_cong 1);
    7.52 +by (Asm_full_simp_tac 1);
    7.53  qed "multiset_eq_conv_Rep_eq";
    7.54  Addsimps [multiset_eq_conv_Rep_eq];
    7.55  Addsimps [expand_fun_eq];
    7.56 @@ -49,13 +49,13 @@
    7.57  Goal
    7.58   "[| f : multiset; g : multiset |] ==> \
    7.59  \ (Abs_multiset f = Abs_multiset g) = (!x. f x = g x)";
    7.60 -br iffI 1;
    7.61 - by(dres_inst_tac [("f","Rep_multiset")] arg_cong 1);
    7.62 - by(Asm_full_simp_tac 1);
    7.63 -by(subgoal_tac "f = g" 1);
    7.64 - by(Asm_simp_tac 1);
    7.65 -br ext 1;
    7.66 -by(Blast_tac 1);
    7.67 +by (rtac iffI 1);
    7.68 + by (dres_inst_tac [("f","Rep_multiset")] arg_cong 1);
    7.69 + by (Asm_full_simp_tac 1);
    7.70 +by (subgoal_tac "f = g" 1);
    7.71 + by (Asm_simp_tac 1);
    7.72 +by (rtac ext 1);
    7.73 +by (Blast_tac 1);
    7.74  qed "Abs_multiset_eq";
    7.75  Addsimps [Abs_multiset_eq];
    7.76  *)
    7.77 @@ -66,18 +66,18 @@
    7.78  
    7.79  Goalw [union_def,empty_def]
    7.80   "M + {#} = M & {#} + M = M";
    7.81 -by(Simp_tac 1);
    7.82 +by (Simp_tac 1);
    7.83  qed "union_empty";
    7.84  Addsimps [union_empty];
    7.85  
    7.86  Goalw [union_def]
    7.87   "(M::'a multiset) + N = N + M";
    7.88 -by(simp_tac (simpset() addsimps add_ac) 1);
    7.89 +by (simp_tac (simpset() addsimps add_ac) 1);
    7.90  qed "union_comm";
    7.91  
    7.92  Goalw [union_def]
    7.93   "((M::'a multiset)+N)+K = M+(N+K)";
    7.94 -by(simp_tac (simpset() addsimps add_ac) 1);
    7.95 +by (simp_tac (simpset() addsimps add_ac) 1);
    7.96  qed "union_assoc";
    7.97  
    7.98  qed_goal "union_lcomm" thy "M+(N+K) = N+((M+K)::'a multiset)"
    7.99 @@ -90,13 +90,13 @@
   7.100  
   7.101  Goalw [empty_def,diff_def]
   7.102   "M-{#} = M & {#}-M = {#}";
   7.103 -by(Simp_tac 1);
   7.104 +by (Simp_tac 1);
   7.105  qed "diff_empty";
   7.106  Addsimps [diff_empty];
   7.107  
   7.108  Goalw [union_def,diff_def]
   7.109   "M+{#a#}-{#a#} = M";
   7.110 -by(Simp_tac 1);
   7.111 +by (Simp_tac 1);
   7.112  qed "diff_union_inverse2";
   7.113  Addsimps [diff_union_inverse2];
   7.114  
   7.115 @@ -104,57 +104,57 @@
   7.116  
   7.117  Goalw [count_def,empty_def]
   7.118   "count {#} a = 0";
   7.119 -by(Simp_tac 1);
   7.120 +by (Simp_tac 1);
   7.121  qed "count_empty";
   7.122  Addsimps [count_empty];
   7.123  
   7.124  Goalw [count_def,single_def]
   7.125   "count {#b#} a = (if b=a then 1 else 0)";
   7.126 -by(Simp_tac 1);
   7.127 +by (Simp_tac 1);
   7.128  qed "count_single";
   7.129  Addsimps [count_single];
   7.130  
   7.131  Goalw [count_def,union_def]
   7.132   "count (M+N) a = count M a + count N a";
   7.133 -by(Simp_tac 1);
   7.134 +by (Simp_tac 1);
   7.135  qed "count_union";
   7.136  Addsimps [count_union];
   7.137  
   7.138  Goalw [count_def,diff_def]
   7.139   "count (M-N) a = count M a - count N a";
   7.140 -by(Simp_tac 1);
   7.141 +by (Simp_tac 1);
   7.142  qed "count_diff";
   7.143  Addsimps [count_diff];
   7.144  
   7.145  (* set_of *)
   7.146  
   7.147  Goalw [set_of_def] "set_of {#} = {}";
   7.148 -by(Simp_tac 1);
   7.149 +by (Simp_tac 1);
   7.150  qed "set_of_empty";
   7.151  Addsimps [set_of_empty];
   7.152  
   7.153  Goalw [set_of_def]
   7.154   "set_of {#b#} = {b}";
   7.155 -by(Simp_tac 1);
   7.156 +by (Simp_tac 1);
   7.157  qed "set_of_single";
   7.158  Addsimps [set_of_single];
   7.159  
   7.160  Goalw [set_of_def]
   7.161   "set_of(M+N) = set_of M Un set_of N";
   7.162 -by(Auto_tac);
   7.163 +by (Auto_tac);
   7.164  qed "set_of_union";
   7.165  Addsimps [set_of_union];
   7.166  
   7.167  (* size *)
   7.168  
   7.169  Goalw [size_def] "size {#} = 0";
   7.170 -by(Simp_tac 1);
   7.171 +by (Simp_tac 1);
   7.172  qed "size_empty";
   7.173  Addsimps [size_empty];
   7.174  
   7.175  Goalw [size_def]
   7.176   "size {#b#} = 1";
   7.177 -by(Simp_tac 1);
   7.178 +by (Simp_tac 1);
   7.179  qed "size_single";
   7.180  Addsimps [size_single];
   7.181  
   7.182 @@ -166,99 +166,99 @@
   7.183  (* equalities *)
   7.184  
   7.185  Goalw [count_def] "(M = N) = (!a. count M a = count N a)";
   7.186 -by(Simp_tac 1);
   7.187 +by (Simp_tac 1);
   7.188  qed "multiset_eq_conv_count_eq";
   7.189  
   7.190  Goalw [single_def,empty_def] "{#a#} ~= {#}  &  {#} ~= {#a#}";
   7.191 -by(Simp_tac 1);
   7.192 +by (Simp_tac 1);
   7.193  qed "single_not_empty";
   7.194  Addsimps [single_not_empty];
   7.195  
   7.196  Goalw [single_def] "({#a#}={#b#}) = (a=b)";
   7.197 -by(Auto_tac);
   7.198 +by (Auto_tac);
   7.199  qed "single_eq_single";
   7.200  Addsimps [single_eq_single];
   7.201  
   7.202  Goalw [union_def,empty_def]
   7.203   "(M+N = {#}) = (M = {#} & N = {#})";
   7.204 -by(Simp_tac 1);
   7.205 -by(Blast_tac 1);
   7.206 +by (Simp_tac 1);
   7.207 +by (Blast_tac 1);
   7.208  qed "union_eq_empty";
   7.209  AddIffs [union_eq_empty];
   7.210  
   7.211  Goalw [union_def,empty_def]
   7.212   "({#} = M+N) = (M = {#} & N = {#})";
   7.213 -by(Simp_tac 1);
   7.214 -by(Blast_tac 1);
   7.215 +by (Simp_tac 1);
   7.216 +by (Blast_tac 1);
   7.217  qed "empty_eq_union";
   7.218  AddIffs [empty_eq_union];
   7.219  
   7.220  Goalw [union_def]
   7.221   "(M+K = N+K) = (M=(N::'a multiset))";
   7.222 -by(Simp_tac 1);
   7.223 +by (Simp_tac 1);
   7.224  qed "union_right_cancel";
   7.225  Addsimps [union_right_cancel];
   7.226  
   7.227  Goalw [union_def]
   7.228   "(K+M = K+N) = (M=(N::'a multiset))";
   7.229 -by(Simp_tac 1);
   7.230 +by (Simp_tac 1);
   7.231  qed "union_left_cancel";
   7.232  Addsimps [union_left_cancel];
   7.233  
   7.234  Goalw [empty_def,single_def,union_def]
   7.235   "(M+N = {#a#}) = (M={#a#} & N={#} | M={#} & N={#a#})";
   7.236 -by(simp_tac (simpset() addsimps [add_is_1]) 1);
   7.237 -by(Blast_tac 1);
   7.238 +by (simp_tac (simpset() addsimps [add_is_1]) 1);
   7.239 +by (Blast_tac 1);
   7.240  qed "union_is_single";
   7.241  
   7.242  Goalw [empty_def,single_def,union_def]
   7.243   "({#a#} = M+N) = ({#a#}=M & N={#} | M={#} & {#a#}=N)";
   7.244 -by(simp_tac (simpset() addsimps [one_is_add]) 1);
   7.245 -by(blast_tac (claset() addDs [sym]) 1);
   7.246 +by (simp_tac (simpset() addsimps [one_is_add]) 1);
   7.247 +by (blast_tac (claset() addDs [sym]) 1);
   7.248  qed "single_is_union";
   7.249  
   7.250  Goalw [single_def,union_def,diff_def]
   7.251   "(M+{#a#} = N+{#b#}) = (M=N & a=b | M = N-{#a#}+{#b#} & N = M-{#b#}+{#a#})";
   7.252 -by(Simp_tac 1);
   7.253 -br conjI 1;
   7.254 - by(Force_tac 1);
   7.255 -by(Clarify_tac 1);
   7.256 -br conjI 1;
   7.257 - by(Blast_tac 1);
   7.258 -by(Clarify_tac 1);
   7.259 -br iffI 1;
   7.260 - br conjI 1;
   7.261 - by(Clarify_tac 1);
   7.262 -  br conjI 1;
   7.263 -   by(asm_full_simp_tac (simpset() addsimps [eq_sym_conv]) 1);
   7.264 +by (Simp_tac 1);
   7.265 +by (rtac conjI 1);
   7.266 + by (Force_tac 1);
   7.267 +by (Clarify_tac 1);
   7.268 +by (rtac conjI 1);
   7.269 + by (Blast_tac 1);
   7.270 +by (Clarify_tac 1);
   7.271 +by (rtac iffI 1);
   7.272 + by (rtac conjI 1);
   7.273 + by (Clarify_tac 1);
   7.274 +  by (rtac conjI 1);
   7.275 +   by (asm_full_simp_tac (simpset() addsimps [eq_sym_conv]) 1);
   7.276  (* PROOF FAILED:
   7.277 -by(Blast_tac 1);
   7.278 +by (Blast_tac 1);
   7.279  *)
   7.280 -  by(Fast_tac 1);
   7.281 - by(Asm_simp_tac 1);
   7.282 -by(Force_tac 1);
   7.283 +  by (Fast_tac 1);
   7.284 + by (Asm_simp_tac 1);
   7.285 +by (Force_tac 1);
   7.286  qed "add_eq_conv_diff";
   7.287  
   7.288  (* FIXME
   7.289  val prems = Goal
   7.290   "[| !!F. [| finite F; !G. G < F --> P G |] ==> P F |] ==> finite F --> P F";
   7.291 -by(res_inst_tac [("a","F"),("f","%A. if finite A then card A else 0")]
   7.292 +by (res_inst_tac [("a","F"),("f","%A. if finite A then card A else 0")]
   7.293       measure_induct 1);
   7.294 -by(Clarify_tac 1);
   7.295 -brs prems 1;
   7.296 - ba 1;
   7.297 -by(Clarify_tac 1);
   7.298 -by(subgoal_tac "finite G" 1);
   7.299 - by(fast_tac (claset() addDs [finite_subset,order_less_le RS iffD1]) 2);
   7.300 -be allE 1;
   7.301 -be impE 1;
   7.302 - by(Blast_tac 2);
   7.303 -by(asm_simp_tac (simpset() addsimps [psubset_card]) 1);
   7.304 +by (Clarify_tac 1);
   7.305 +by (resolve_tac prems 1);
   7.306 + by (assume_tac 1);
   7.307 +by (Clarify_tac 1);
   7.308 +by (subgoal_tac "finite G" 1);
   7.309 + by (fast_tac (claset() addDs [finite_subset,order_less_le RS iffD1]) 2);
   7.310 +by (etac allE 1);
   7.311 +by (etac impE 1);
   7.312 + by (Blast_tac 2);
   7.313 +by (asm_simp_tac (simpset() addsimps [psubset_card]) 1);
   7.314  val lemma = result();
   7.315  
   7.316  val prems = Goal
   7.317   "[| finite F; !!F. [| finite F; !G. G < F --> P G |] ==> P F |] ==> P F";
   7.318 -br (lemma RS mp) 1;
   7.319 +by (rtac (lemma RS mp) 1);
   7.320  by (REPEAT(ares_tac prems 1));
   7.321  qed "finite_psubset_induct";
   7.322  
   7.323 @@ -268,65 +268,65 @@
   7.324  (** Towards the induction rule **)
   7.325  
   7.326  Goal "finite F ==> (setsum f F = 0) = (!a:F. f a = 0)";
   7.327 -be finite_induct 1;
   7.328 -by(Auto_tac);
   7.329 +by (etac finite_induct 1);
   7.330 +by (Auto_tac);
   7.331  qed "setsum_0";
   7.332  Addsimps [setsum_0];
   7.333  
   7.334  Goal "finite F ==> setsum f F = Suc n --> (? a:F. 0 < f a)";
   7.335 -be finite_induct 1;
   7.336 -by(Auto_tac);
   7.337 +by (etac finite_induct 1);
   7.338 +by (Auto_tac);
   7.339  val lemma = result();
   7.340  
   7.341  Goal "[| setsum f F = Suc n; finite F |] ==> ? a:F. 0 < f a";
   7.342 -bd lemma 1;
   7.343 -by(Fast_tac 1);
   7.344 +by (dtac lemma 1);
   7.345 +by (Fast_tac 1);
   7.346  qed "setsum_SucD";
   7.347  
   7.348  Goal "[| finite F; 0 < f a |] ==> \
   7.349  \     setsum (f(a:=f(a)-1)) F = (if a:F then setsum f F - 1 else setsum f F)";
   7.350 -be finite_induct 1;
   7.351 -by(Auto_tac);
   7.352 - by(asm_simp_tac (simpset() addsimps add_ac) 1);
   7.353 -by(dres_inst_tac [("a","a")] mk_disjoint_insert 1);
   7.354 -by(Auto_tac);
   7.355 +by (etac finite_induct 1);
   7.356 +by (Auto_tac);
   7.357 + by (asm_simp_tac (simpset() addsimps add_ac) 1);
   7.358 +by (dres_inst_tac [("a","a")] mk_disjoint_insert 1);
   7.359 +by (Auto_tac);
   7.360  qed "setsum_decr";
   7.361  
   7.362  val prems = Goalw [multiset_def]
   7.363   "[| P(%a.0); \
   7.364  \    !!f b. [| f : multiset; P(f) |] ==> P(f(b:=f(b)+1)) |] \
   7.365  \  ==> !f. f : multiset --> setsum f {x. 0 < f x} = n --> P(f)";
   7.366 -by(induct_tac "n" 1);
   7.367 - by(Asm_simp_tac 1);
   7.368 - by(Clarify_tac 1);
   7.369 - by(subgoal_tac "f = (%a.0)" 1);
   7.370 -  by(Asm_simp_tac 1);
   7.371 -  brs prems 1;
   7.372 - br ext 1;
   7.373 - by(Force_tac 1);
   7.374 -by(Clarify_tac 1);
   7.375 -by(forward_tac [setsum_SucD] 1);
   7.376 - ba 1;
   7.377 -by(Clarify_tac 1);
   7.378 -by(rename_tac "a" 1);
   7.379 -by(subgoal_tac "finite{x. 0 < (f(a:=f(a)-1)) x}" 1);
   7.380 - be (rotate_prems 1 finite_subset) 2;
   7.381 - by(Simp_tac 2);
   7.382 - by(Blast_tac 2);
   7.383 -by(subgoal_tac
   7.384 +by (induct_tac "n" 1);
   7.385 + by (Asm_simp_tac 1);
   7.386 + by (Clarify_tac 1);
   7.387 + by (subgoal_tac "f = (%a.0)" 1);
   7.388 +  by (Asm_simp_tac 1);
   7.389 +  by (resolve_tac prems 1);
   7.390 + by (rtac ext 1);
   7.391 + by (Force_tac 1);
   7.392 +by (Clarify_tac 1);
   7.393 +by (forward_tac [setsum_SucD] 1);
   7.394 + by (assume_tac 1);
   7.395 +by (Clarify_tac 1);
   7.396 +by (rename_tac "a" 1);
   7.397 +by (subgoal_tac "finite{x. 0 < (f(a:=f(a)-1)) x}" 1);
   7.398 + by (etac (rotate_prems 1 finite_subset) 2);
   7.399 + by (Simp_tac 2);
   7.400 + by (Blast_tac 2);
   7.401 +by (subgoal_tac
   7.402     "f = (f(a:=f(a)-1))(a:=(f(a:=f(a)-1))a+1)" 1);
   7.403 - br ext 2;
   7.404 - by(Asm_simp_tac 2);
   7.405 -by(EVERY1[etac ssubst, resolve_tac prems]);
   7.406 - by(Blast_tac 1);
   7.407 -by(EVERY[etac allE 1, etac impE 1, etac mp 2]);
   7.408 - by(Blast_tac 1);
   7.409 -by(asm_simp_tac (simpset() addsimps [setsum_decr] delsimps [fun_upd_apply]) 1);
   7.410 -by(subgoal_tac "{x. x ~= a --> 0 < f x} = {x. 0 < f x}" 1);
   7.411 - by(Blast_tac 2);
   7.412 -by(subgoal_tac "{x. x ~= a & 0 < f x} = {x. 0 < f x} - {a}" 1);
   7.413 - by(Blast_tac 2);
   7.414 -by(asm_simp_tac (simpset() addsimps [le_imp_diff_is_add,setsum_diff1]
   7.415 + by (rtac ext 2);
   7.416 + by (Asm_simp_tac 2);
   7.417 +by (EVERY1[etac ssubst, resolve_tac prems]);
   7.418 + by (Blast_tac 1);
   7.419 +by (EVERY[etac allE 1, etac impE 1, etac mp 2]);
   7.420 + by (Blast_tac 1);
   7.421 +by (asm_simp_tac (simpset() addsimps [setsum_decr] delsimps [fun_upd_apply]) 1);
   7.422 +by (subgoal_tac "{x. x ~= a --> 0 < f x} = {x. 0 < f x}" 1);
   7.423 + by (Blast_tac 2);
   7.424 +by (subgoal_tac "{x. x ~= a & 0 < f x} = {x. 0 < f x} - {a}" 1);
   7.425 + by (Blast_tac 2);
   7.426 +by (asm_simp_tac (simpset() addsimps [le_imp_diff_is_add,setsum_diff1]
   7.427                             addcongs [conj_cong]) 1);
   7.428  val lemma = result();
   7.429  
   7.430 @@ -334,22 +334,22 @@
   7.431   "[| f : multiset; \
   7.432  \    P(%a.0); \
   7.433  \    !!f b. [| f : multiset; P(f) |] ==> P(f(b:=f(b)+1)) |] ==> P(f)";
   7.434 -by(rtac (major RSN (3, lemma RS spec RS mp RS mp)) 1);
   7.435 -by(REPEAT(ares_tac (refl::prems) 1));
   7.436 +by (rtac (major RSN (3, lemma RS spec RS mp RS mp)) 1);
   7.437 +by (REPEAT(ares_tac (refl::prems) 1));
   7.438  qed "Rep_multiset_induct";
   7.439  
   7.440  val [prem1,prem2] = Goalw [union_def,single_def,empty_def]
   7.441   "[| P({#}); !!M x. P(M) ==> P(M + {#x#}) |] ==> P(M)";
   7.442  by (rtac (Rep_multiset_inverse RS subst) 1);
   7.443  by (rtac (Rep_multiset RS Rep_multiset_induct) 1);
   7.444 - by(rtac prem1 1);
   7.445 -by(Clarify_tac 1);
   7.446 -by(subgoal_tac
   7.447 + by (rtac prem1 1);
   7.448 +by (Clarify_tac 1);
   7.449 +by (subgoal_tac
   7.450      "f(b := f b + 1) = (%a. f a + (if a = b then 1 else 0))" 1);
   7.451 - by(Simp_tac 2);
   7.452 -be ssubst 1;
   7.453 -by(etac (Abs_multiset_inverse RS subst) 1);
   7.454 -by(etac(simplify (simpset()) prem2)1);
   7.455 + by (Simp_tac 2);
   7.456 +by (etac ssubst 1);
   7.457 +by (etac (Abs_multiset_inverse RS subst) 1);
   7.458 +by (etac(simplify (simpset()) prem2)1);
   7.459  qed "multiset_induct";
   7.460  
   7.461  Delsimps [multiset_eq_conv_Rep_eq, expand_fun_eq];
   7.462 @@ -357,14 +357,14 @@
   7.463  
   7.464  Goal
   7.465   "(M+{#a#} = N+{#b#}) = (M = N & a = b | (? K. M = K+{#b#} & N = K+{#a#}))";
   7.466 -by(simp_tac (simpset() addsimps [add_eq_conv_diff]) 1);
   7.467 -by(Auto_tac);
   7.468 +by (simp_tac (simpset() addsimps [add_eq_conv_diff]) 1);
   7.469 +by (Auto_tac);
   7.470  qed "add_eq_conv_ex";
   7.471  
   7.472  (** order **)
   7.473  
   7.474  Goalw [mult1_def] "(M, {#}) ~: mult1(r)";
   7.475 -by(Simp_tac 1);
   7.476 +by (Simp_tac 1);
   7.477  qed "not_less_empty";
   7.478  AddIffs [not_less_empty];
   7.479  
   7.480 @@ -372,22 +372,22 @@
   7.481   "(N,M0 + {#a#}) : mult1(r) = \
   7.482  \ ((? M. (M,M0) : mult1(r) & N = M + {#a#}) | \
   7.483  \  (? K. (!b. elem K b --> (b,a) : r) & N = M0 + K))";
   7.484 -br iffI 1;
   7.485 - by(asm_full_simp_tac (simpset() addsimps [add_eq_conv_ex]) 1);
   7.486 - by(Clarify_tac 1);
   7.487 - be disjE 1;
   7.488 -  by(Blast_tac 1);
   7.489 - by(Clarify_tac 1);
   7.490 - by(res_inst_tac [("x","Ka+K")] exI 1);
   7.491 - by(simp_tac (simpset() addsimps union_ac) 1);
   7.492 - by(Blast_tac 1);
   7.493 -be disjE 1;
   7.494 - by(Clarify_tac 1);
   7.495 - by(res_inst_tac [("x","aa")] exI 1);
   7.496 - by(res_inst_tac [("x","M0+{#a#}")] exI 1);
   7.497 - by(res_inst_tac [("x","K")] exI 1);
   7.498 - by(simp_tac (simpset() addsimps union_ac) 1);
   7.499 -by(Blast_tac 1);
   7.500 +by (rtac iffI 1);
   7.501 + by (asm_full_simp_tac (simpset() addsimps [add_eq_conv_ex]) 1);
   7.502 + by (Clarify_tac 1);
   7.503 + by (etac disjE 1);
   7.504 +  by (Blast_tac 1);
   7.505 + by (Clarify_tac 1);
   7.506 + by (res_inst_tac [("x","Ka+K")] exI 1);
   7.507 + by (simp_tac (simpset() addsimps union_ac) 1);
   7.508 + by (Blast_tac 1);
   7.509 +by (etac disjE 1);
   7.510 + by (Clarify_tac 1);
   7.511 + by (res_inst_tac [("x","aa")] exI 1);
   7.512 + by (res_inst_tac [("x","M0+{#a#}")] exI 1);
   7.513 + by (res_inst_tac [("x","K")] exI 1);
   7.514 + by (simp_tac (simpset() addsimps union_ac) 1);
   7.515 +by (Blast_tac 1);
   7.516  qed "less_add_conv";
   7.517  
   7.518  Open_locale "MSOrd";
   7.519 @@ -398,47 +398,47 @@
   7.520   "[| !b. (b,a) : r --> (!M : W. M+{#b#} : W); M0 : W; \
   7.521  \    !M. (M,M0) : mult1(r) --> M+{#a#} : W |] \
   7.522  \ ==> M0+{#a#} : W";
   7.523 -br accI 1;
   7.524 -by(rename_tac "N" 1);
   7.525 -by(full_simp_tac (simpset() addsimps [less_add_conv]) 1);
   7.526 -be disjE 1;
   7.527 - by(Blast_tac 1);
   7.528 -by(Clarify_tac 1);
   7.529 -by(rotate_tac ~1 1);
   7.530 -be rev_mp 1;
   7.531 -by(res_inst_tac [("M","K")] multiset_induct 1);
   7.532 - by(Asm_simp_tac 1);
   7.533 -by(simp_tac (simpset() addsimps [union_assoc RS sym]) 1);
   7.534 -by(Blast_tac 1);
   7.535 +by (rtac accI 1);
   7.536 +by (rename_tac "N" 1);
   7.537 +by (full_simp_tac (simpset() addsimps [less_add_conv]) 1);
   7.538 +by (etac disjE 1);
   7.539 + by (Blast_tac 1);
   7.540 +by (Clarify_tac 1);
   7.541 +by (rotate_tac ~1 1);
   7.542 +by (etac rev_mp 1);
   7.543 +by (res_inst_tac [("M","K")] multiset_induct 1);
   7.544 + by (Asm_simp_tac 1);
   7.545 +by (simp_tac (simpset() addsimps [union_assoc RS sym]) 1);
   7.546 +by (Blast_tac 1);
   7.547  qed "lemma1";
   7.548  
   7.549  Goalw [W_def]
   7.550   "[| !b. (b,a) : r --> (!M : W. M+{#b#} : W); M : W |] ==> M+{#a#} : W";
   7.551 -be acc_induct 1;
   7.552 -by(blast_tac (claset() addIs [export lemma1]) 1);
   7.553 +by (etac acc_induct 1);
   7.554 +by (blast_tac (claset() addIs [export lemma1]) 1);
   7.555  qed "lemma2";
   7.556  
   7.557  Goalw [W_def]
   7.558   "wf(r) ==> !M:W. M+{#a#} : W";
   7.559 -by(eres_inst_tac [("a","a")] wf_induct 1);
   7.560 -by(blast_tac (claset() addIs [export lemma2]) 1);
   7.561 +by (eres_inst_tac [("a","a")] wf_induct 1);
   7.562 +by (blast_tac (claset() addIs [export lemma2]) 1);
   7.563  qed "lemma3";
   7.564  
   7.565  Goalw [W_def] "wf(r) ==> M : W";
   7.566 -by(res_inst_tac [("M","M")] multiset_induct 1);
   7.567 - br accI 1;
   7.568 - by(Asm_full_simp_tac 1);
   7.569 -by(blast_tac (claset() addDs [export lemma3]) 1);
   7.570 +by (res_inst_tac [("M","M")] multiset_induct 1);
   7.571 + by (rtac accI 1);
   7.572 + by (Asm_full_simp_tac 1);
   7.573 +by (blast_tac (claset() addDs [export lemma3]) 1);
   7.574  qed "all_accessible";
   7.575  
   7.576  Close_locale "MSOrd";
   7.577  
   7.578  Goal "wf(r) ==> wf(mult1 r)";
   7.579 -by(blast_tac (claset() addIs [acc_wfI, export all_accessible]) 1);
   7.580 +by (blast_tac (claset() addIs [acc_wfI, export all_accessible]) 1);
   7.581  qed "wf_mult1";
   7.582  
   7.583  Goalw [mult_def] "wf(r) ==> wf(mult r)";
   7.584 -by(blast_tac (claset() addIs [wf_trancl,wf_mult1]) 1);
   7.585 +by (blast_tac (claset() addIs [wf_trancl,wf_mult1]) 1);
   7.586  qed "wf_mult";
   7.587  
   7.588  (** Equivalence of mult with the usual (closure-free) def **)
   7.589 @@ -446,7 +446,7 @@
   7.590  (* Badly needed: a linear arithmetic tactic for multisets *)
   7.591  
   7.592  Goal "elem J a ==> I+J - {#a#} = I + (J-{#a#})";
   7.593 -by(asm_simp_tac (simpset() addsimps [multiset_eq_conv_count_eq]) 1);
   7.594 +by (asm_simp_tac (simpset() addsimps [multiset_eq_conv_count_eq]) 1);
   7.595  qed "diff_union_single_conv";
   7.596  
   7.597  (* One direction *)
   7.598 @@ -454,35 +454,35 @@
   7.599   "trans r ==> \
   7.600  \ (M,N) : mult r ==> (? I J K. N = I+J & M = I+K & J ~= {#} & \
   7.601  \                            (!k : set_of K. ? j : set_of J. (k,j) : r))";
   7.602 -be converse_trancl_induct 1;
   7.603 - by(Clarify_tac 1);
   7.604 - by(res_inst_tac [("x","M0")] exI 1);
   7.605 - by(Simp_tac 1);
   7.606 -by(Clarify_tac 1);
   7.607 -by(case_tac "elem K a" 1);
   7.608 - by(res_inst_tac [("x","I")] exI 1);
   7.609 - by(Simp_tac 1);
   7.610 - by(res_inst_tac [("x","(K - {#a#}) + Ka")] exI 1);
   7.611 - by(asm_simp_tac (simpset() addsimps [union_assoc RS sym]) 1);
   7.612 - by(dres_inst_tac[("f","%M. M-{#a#}")] arg_cong 1);
   7.613 - by(asm_full_simp_tac (simpset() addsimps [diff_union_single_conv]) 1);
   7.614 - by(full_simp_tac (simpset() addsimps [trans_def]) 1);
   7.615 - by(Blast_tac 1);
   7.616 -by(subgoal_tac "elem I a" 1);
   7.617 - by(res_inst_tac [("x","I-{#a#}")] exI 1);
   7.618 - by(res_inst_tac [("x","J+{#a#}")] exI 1);
   7.619 - by(res_inst_tac [("x","K + Ka")] exI 1);
   7.620 - br conjI 1;
   7.621 -  by(asm_simp_tac (simpset() addsimps [multiset_eq_conv_count_eq]
   7.622 +by (etac converse_trancl_induct 1);
   7.623 + by (Clarify_tac 1);
   7.624 + by (res_inst_tac [("x","M0")] exI 1);
   7.625 + by (Simp_tac 1);
   7.626 +by (Clarify_tac 1);
   7.627 +by (case_tac "elem K a" 1);
   7.628 + by (res_inst_tac [("x","I")] exI 1);
   7.629 + by (Simp_tac 1);
   7.630 + by (res_inst_tac [("x","(K - {#a#}) + Ka")] exI 1);
   7.631 + by (asm_simp_tac (simpset() addsimps [union_assoc RS sym]) 1);
   7.632 + by (dres_inst_tac[("f","%M. M-{#a#}")] arg_cong 1);
   7.633 + by (asm_full_simp_tac (simpset() addsimps [diff_union_single_conv]) 1);
   7.634 + by (full_simp_tac (simpset() addsimps [trans_def]) 1);
   7.635 + by (Blast_tac 1);
   7.636 +by (subgoal_tac "elem I a" 1);
   7.637 + by (res_inst_tac [("x","I-{#a#}")] exI 1);
   7.638 + by (res_inst_tac [("x","J+{#a#}")] exI 1);
   7.639 + by (res_inst_tac [("x","K + Ka")] exI 1);
   7.640 + by (rtac conjI 1);
   7.641 +  by (asm_simp_tac (simpset() addsimps [multiset_eq_conv_count_eq]
   7.642                               addsplits [nat_diff_split]) 1);
   7.643 - br conjI 1;
   7.644 -  by(dres_inst_tac[("f","%M. M-{#a#}")] arg_cong 1);
   7.645 -  by(Asm_full_simp_tac 1);
   7.646 -  by(asm_simp_tac (simpset() addsimps [multiset_eq_conv_count_eq]
   7.647 + by (rtac conjI 1);
   7.648 +  by (dres_inst_tac[("f","%M. M-{#a#}")] arg_cong 1);
   7.649 +  by (Asm_full_simp_tac 1);
   7.650 +  by (asm_simp_tac (simpset() addsimps [multiset_eq_conv_count_eq]
   7.651                               addsplits [nat_diff_split]) 1);
   7.652 - by(full_simp_tac (simpset() addsimps [trans_def]) 1);
   7.653 - by(Blast_tac 1);
   7.654 -by(subgoal_tac "elem (M0 +{#a#}) a" 1);
   7.655 - by(Asm_full_simp_tac 1);
   7.656 -by(Simp_tac 1);
   7.657 + by (full_simp_tac (simpset() addsimps [trans_def]) 1);
   7.658 + by (Blast_tac 1);
   7.659 +by (subgoal_tac "elem (M0 +{#a#}) a" 1);
   7.660 + by (Asm_full_simp_tac 1);
   7.661 +by (Simp_tac 1);
   7.662  qed "mult_implies_one_step";
     8.1 --- a/src/HOL/Lex/RegExp2NA.ML	Fri Jan 29 16:23:56 1999 +0100
     8.2 +++ b/src/HOL/Lex/RegExp2NA.ML	Fri Jan 29 16:26:12 1999 +0100
     8.3 @@ -9,37 +9,37 @@
     8.4  (******************************************************)
     8.5  
     8.6  Goalw [atom_def] "(fin (atom a) q) = (q = [False])";
     8.7 -by(Simp_tac 1);
     8.8 +by (Simp_tac 1);
     8.9  qed "fin_atom";
    8.10  
    8.11  Goalw [atom_def] "start (atom a) = [True]";
    8.12 -by(Simp_tac 1);
    8.13 +by (Simp_tac 1);
    8.14  qed "start_atom";
    8.15  
    8.16  Goalw [atom_def,step_def]
    8.17   "(p,q) : step (atom a) b = (p=[True] & q=[False] & b=a)";
    8.18 -by(Simp_tac 1);
    8.19 +by (Simp_tac 1);
    8.20  qed "in_step_atom_Some";
    8.21  Addsimps [in_step_atom_Some];
    8.22  
    8.23  Goal
    8.24   "([False],[False]) : steps (atom a) w = (w = [])";
    8.25  by (induct_tac "w" 1);
    8.26 - by(Simp_tac 1);
    8.27 -by(asm_simp_tac (simpset() addsimps [comp_def]) 1);
    8.28 + by (Simp_tac 1);
    8.29 +by (asm_simp_tac (simpset() addsimps [comp_def]) 1);
    8.30  qed "False_False_in_steps_atom";
    8.31  
    8.32  Goal
    8.33   "(start (atom a), [False]) : steps (atom a) w = (w = [a])";
    8.34  by (induct_tac "w" 1);
    8.35 - by(asm_simp_tac (simpset() addsimps [start_atom]) 1);
    8.36 -by(asm_full_simp_tac (simpset()
    8.37 + by (asm_simp_tac (simpset() addsimps [start_atom]) 1);
    8.38 +by (asm_full_simp_tac (simpset()
    8.39       addsimps [False_False_in_steps_atom,comp_def,start_atom]) 1);
    8.40  qed "start_fin_in_steps_atom";
    8.41  
    8.42  Goal
    8.43   "accepts (atom a) w = (w = [a])";
    8.44 -by(simp_tac(simpset() addsimps
    8.45 +by (simp_tac(simpset() addsimps
    8.46         [accepts_conv_steps,start_fin_in_steps_atom,fin_atom]) 1);
    8.47  qed "accepts_atom";
    8.48  
    8.49 @@ -67,13 +67,13 @@
    8.50  Goalw [union_def,step_def]
    8.51  "!L R. (True#p,q) : step (union L R) a = (? r. q = True#r & (p,r) : step L a)";
    8.52  by (Simp_tac 1);
    8.53 -by(Blast_tac 1);
    8.54 +by (Blast_tac 1);
    8.55  qed_spec_mp "True_in_step_union";
    8.56  
    8.57  Goalw [union_def,step_def]
    8.58  "!L R. (False#p,q) : step (union L R) a = (? r. q = False#r & (p,r) : step R a)";
    8.59  by (Simp_tac 1);
    8.60 -by(Blast_tac 1);
    8.61 +by (Blast_tac 1);
    8.62  qed_spec_mp "False_in_step_union";
    8.63  
    8.64  AddIffs [True_in_step_union,False_in_step_union];
    8.65 @@ -102,8 +102,8 @@
    8.66   "!L R. (start(union L R),q) : step(union L R) a = \
    8.67  \       (? p. (q = True#p & (start L,p) : step L a) | \
    8.68  \             (q = False#p & (start R,p) : step R a))";
    8.69 -by(Simp_tac 1);
    8.70 -by(Blast_tac 1);
    8.71 +by (Simp_tac 1);
    8.72 +by (Blast_tac 1);
    8.73  qed_spec_mp "start_step_union";
    8.74  AddIffs [start_step_union];
    8.75  
    8.76 @@ -112,17 +112,17 @@
    8.77  \ ( (w = [] & q = start(union L R)) | \
    8.78  \   (w ~= [] & (? p.  q = True  # p & (start L,p) : steps L w | \
    8.79  \                     q = False # p & (start R,p) : steps R w)))";
    8.80 -by(exhaust_tac "w" 1);
    8.81 +by (exhaust_tac "w" 1);
    8.82   by (Asm_simp_tac 1);
    8.83 - by(Blast_tac 1);
    8.84 + by (Blast_tac 1);
    8.85  by (Asm_simp_tac 1);
    8.86 -by(Blast_tac 1);
    8.87 +by (Blast_tac 1);
    8.88  qed "steps_union";
    8.89  
    8.90  Goalw [union_def]
    8.91   "!L R. fin (union L R) (start(union L R)) = \
    8.92  \       (fin L (start L) | fin R (start R))";
    8.93 -by(Simp_tac 1);
    8.94 +by (Simp_tac 1);
    8.95  qed_spec_mp "fin_start_union";
    8.96  AddIffs [fin_start_union];
    8.97  
    8.98 @@ -130,8 +130,8 @@
    8.99   "accepts (union L R) w = (accepts L w | accepts R w)";
   8.100  by (simp_tac (simpset() addsimps [accepts_conv_steps,steps_union]) 1);
   8.101  (* get rid of case_tac: *)
   8.102 -by(case_tac "w = []" 1);
   8.103 -by(Auto_tac);
   8.104 +by (case_tac "w = []" 1);
   8.105 +by (Auto_tac);
   8.106  qed "accepts_union";
   8.107  AddIffs [accepts_union];
   8.108  
   8.109 @@ -160,14 +160,14 @@
   8.110  \       ((? r. q=True#r & (p,r): step L a) | \
   8.111  \        (fin L p & (? r. q=False#r & (start R,r) : step R a)))";
   8.112  by (Simp_tac 1);
   8.113 -by(Blast_tac 1);
   8.114 +by (Blast_tac 1);
   8.115  qed_spec_mp "True_step_conc";
   8.116  
   8.117  Goalw [conc_def,step_def]
   8.118   "!L R. (False#p,q) : step (conc L R) a = \
   8.119  \       (? r. q = False#r & (p,r) : step R a)";
   8.120  by (Simp_tac 1);
   8.121 -by(Blast_tac 1);
   8.122 +by (Blast_tac 1);
   8.123  qed_spec_mp "False_step_conc";
   8.124  
   8.125  AddIffs [True_step_conc, False_step_conc];
   8.126 @@ -185,16 +185,16 @@
   8.127  
   8.128  Goal
   8.129   "!!L R. !p. (p,q) : steps L w --> (True#p,True#q) : steps (conc L R) w";
   8.130 -by(induct_tac "w" 1);
   8.131 +by (induct_tac "w" 1);
   8.132   by (Simp_tac 1);
   8.133  by (Simp_tac 1);
   8.134 -by(Blast_tac 1);
   8.135 +by (Blast_tac 1);
   8.136  qed_spec_mp "True_True_steps_concI";
   8.137  
   8.138  Goal
   8.139   "!L R. (True#p,False#q) : step (conc L R) a = \
   8.140  \       (fin L p & (start R,q) : step R a)";
   8.141 -by(Simp_tac 1);
   8.142 +by (Simp_tac 1);
   8.143  qed "True_False_step_conc";
   8.144  AddIffs [True_False_step_conc];
   8.145  
   8.146 @@ -205,26 +205,26 @@
   8.147  \            (? r. (p,r) : steps L u & fin L r & \
   8.148  \            (? s. (start R,s) : step R a & \
   8.149  \            (? t. (s,t) : steps R v & q = False#t)))))";
   8.150 -by(induct_tac "w" 1);
   8.151 - by(Simp_tac 1);
   8.152 -by(Simp_tac 1);
   8.153 -by(clarify_tac (claset() delrules [disjCI]) 1);
   8.154 -be disjE 1;
   8.155 - by(clarify_tac (claset() delrules [disjCI]) 1);
   8.156 - by(etac allE 1 THEN mp_tac 1);
   8.157 - be disjE 1;
   8.158 +by (induct_tac "w" 1);
   8.159 + by (Simp_tac 1);
   8.160 +by (Simp_tac 1);
   8.161 +by (clarify_tac (claset() delrules [disjCI]) 1);
   8.162 +by (etac disjE 1);
   8.163 + by (clarify_tac (claset() delrules [disjCI]) 1);
   8.164 + by (etac allE 1 THEN mp_tac 1);
   8.165 + by (etac disjE 1);
   8.166    by (Blast_tac 1);
   8.167 - br disjI2 1;
   8.168 + by (rtac disjI2 1);
   8.169   by (Clarify_tac 1);
   8.170 - by(Simp_tac 1);
   8.171 - by(res_inst_tac[("x","a#u")] exI 1);
   8.172 - by(Simp_tac 1);
   8.173 + by (Simp_tac 1);
   8.174 + by (res_inst_tac[("x","a#u")] exI 1);
   8.175 + by (Simp_tac 1);
   8.176   by (Blast_tac 1);
   8.177 -br disjI2 1;
   8.178 +by (rtac disjI2 1);
   8.179  by (Clarify_tac 1);
   8.180 -by(Simp_tac 1);
   8.181 -by(res_inst_tac[("x","[]")] exI 1);
   8.182 -by(Simp_tac 1);
   8.183 +by (Simp_tac 1);
   8.184 +by (res_inst_tac[("x","[]")] exI 1);
   8.185 +by (Simp_tac 1);
   8.186  by (Blast_tac 1);
   8.187  qed_spec_mp "True_steps_concD";
   8.188  
   8.189 @@ -235,7 +235,7 @@
   8.190  \            (? r. (p,r) : steps L u & fin L r & \
   8.191  \            (? s. (start R,s) : step R a & \
   8.192  \            (? t. (s,t) : steps R v & q = False#t)))))";
   8.193 -by(force_tac (claset() addDs [True_steps_concD]
   8.194 +by (force_tac (claset() addDs [True_steps_concD]
   8.195       addIs [True_True_steps_concI],simpset()) 1);
   8.196  qed "True_steps_conc";
   8.197  
   8.198 @@ -243,7 +243,7 @@
   8.199  
   8.200  Goalw [conc_def]
   8.201    "!L R. start(conc L R) = True#start L";
   8.202 -by(Simp_tac 1);
   8.203 +by (Simp_tac 1);
   8.204  qed_spec_mp "start_conc";
   8.205  
   8.206  Goalw [conc_def]
   8.207 @@ -257,27 +257,27 @@
   8.208   "accepts (conc L R) w = (? u v. w = u@v & accepts L u & accepts R v)";
   8.209  by (simp_tac (simpset() addsimps
   8.210       [accepts_conv_steps,True_steps_conc,final_conc,start_conc]) 1);
   8.211 -br iffI 1;
   8.212 +by (rtac iffI 1);
   8.213   by (Clarify_tac 1);
   8.214 - be disjE 1;
   8.215 + by (etac disjE 1);
   8.216    by (Clarify_tac 1);
   8.217 -  be disjE 1;
   8.218 -   by(res_inst_tac [("x","w")] exI 1);
   8.219 -   by(Simp_tac 1);
   8.220 -   by(Blast_tac 1);
   8.221 -  by(Blast_tac 1);
   8.222 - be disjE 1;
   8.223 -  by(Blast_tac 1);
   8.224 +  by (etac disjE 1);
   8.225 +   by (res_inst_tac [("x","w")] exI 1);
   8.226 +   by (Simp_tac 1);
   8.227 +   by (Blast_tac 1);
   8.228 +  by (Blast_tac 1);
   8.229 + by (etac disjE 1);
   8.230 +  by (Blast_tac 1);
   8.231   by (Clarify_tac 1);
   8.232 - by(res_inst_tac [("x","u")] exI 1);
   8.233 - by(Simp_tac 1);
   8.234 - by(Blast_tac 1);
   8.235 + by (res_inst_tac [("x","u")] exI 1);
   8.236 + by (Simp_tac 1);
   8.237 + by (Blast_tac 1);
   8.238  by (Clarify_tac 1);
   8.239 -by(exhaust_tac "v" 1);
   8.240 - by(Asm_full_simp_tac 1);
   8.241 - by(Blast_tac 1);
   8.242 -by(Asm_full_simp_tac 1);
   8.243 -by(Blast_tac 1);
   8.244 +by (exhaust_tac "v" 1);
   8.245 + by (Asm_full_simp_tac 1);
   8.246 + by (Blast_tac 1);
   8.247 +by (Asm_full_simp_tac 1);
   8.248 +by (Blast_tac 1);
   8.249  qed "accepts_conc";
   8.250  
   8.251  (******************************************************)
   8.252 @@ -285,19 +285,19 @@
   8.253  (******************************************************)
   8.254  
   8.255  Goalw [epsilon_def,step_def] "step epsilon a = {}";
   8.256 -by(Simp_tac 1);
   8.257 -by(Blast_tac 1);
   8.258 +by (Simp_tac 1);
   8.259 +by (Blast_tac 1);
   8.260  qed "step_epsilon";
   8.261  Addsimps [step_epsilon];
   8.262  
   8.263  Goal "((p,q) : steps epsilon w) = (w=[] & p=q)";
   8.264 -by(induct_tac "w" 1);
   8.265 -by(Auto_tac);
   8.266 +by (induct_tac "w" 1);
   8.267 +by (Auto_tac);
   8.268  qed "steps_epsilon";
   8.269  
   8.270  Goal "accepts epsilon w = (w = [])";
   8.271 -by(simp_tac (simpset() addsimps [steps_epsilon,accepts_conv_steps]) 1);
   8.272 -by(simp_tac (simpset() addsimps [epsilon_def]) 1);
   8.273 +by (simp_tac (simpset() addsimps [steps_epsilon,accepts_conv_steps]) 1);
   8.274 +by (simp_tac (simpset() addsimps [epsilon_def]) 1);
   8.275  qed "accepts_epsilon";
   8.276  AddIffs [accepts_epsilon];
   8.277  
   8.278 @@ -306,41 +306,41 @@
   8.279  (******************************************************)
   8.280  
   8.281  Goalw [plus_def] "!A. start (plus A) = start A";
   8.282 -by(Simp_tac 1);
   8.283 +by (Simp_tac 1);
   8.284  qed_spec_mp "start_plus";
   8.285  Addsimps [start_plus];
   8.286  
   8.287  Goalw [plus_def] "!A. fin (plus A) = fin A";
   8.288 -by(Simp_tac 1);
   8.289 +by (Simp_tac 1);
   8.290  qed_spec_mp "fin_plus";
   8.291  AddIffs [fin_plus];
   8.292  
   8.293  Goalw [plus_def,step_def]
   8.294    "!A. (p,q) : step A a --> (p,q) : step (plus A) a";
   8.295 -by(Simp_tac 1);
   8.296 +by (Simp_tac 1);
   8.297  qed_spec_mp "step_plusI";
   8.298  
   8.299  Goal "!p. (p,q) : steps A w --> (p,q) : steps (plus A) w";
   8.300 -by(induct_tac "w" 1);
   8.301 - by(Simp_tac 1);
   8.302 -by(Simp_tac 1);
   8.303 -by(blast_tac (claset() addIs [step_plusI]) 1);
   8.304 +by (induct_tac "w" 1);
   8.305 + by (Simp_tac 1);
   8.306 +by (Simp_tac 1);
   8.307 +by (blast_tac (claset() addIs [step_plusI]) 1);
   8.308  qed_spec_mp "steps_plusI";
   8.309  
   8.310  Goalw [plus_def,step_def]
   8.311   "!A. (p,r): step (plus A) a = \
   8.312  \     ( (p,r): step A a | fin A p & (start A,r) : step A a )";
   8.313 -by(Simp_tac 1);
   8.314 +by (Simp_tac 1);
   8.315  qed_spec_mp "step_plus_conv";
   8.316  AddIffs [step_plus_conv];
   8.317  
   8.318  Goal
   8.319   "[| (start A,q) : steps A u; u ~= []; fin A p |] \
   8.320  \ ==> (p,q) : steps (plus A) u";
   8.321 -by(exhaust_tac "u" 1);
   8.322 - by(Blast_tac 1);
   8.323 -by(Asm_full_simp_tac 1);
   8.324 -by(blast_tac (claset() addIs [steps_plusI]) 1);
   8.325 +by (exhaust_tac "u" 1);
   8.326 + by (Blast_tac 1);
   8.327 +by (Asm_full_simp_tac 1);
   8.328 +by (blast_tac (claset() addIs [steps_plusI]) 1);
   8.329  qed "fin_steps_plusI";
   8.330  
   8.331  (* reverse list induction! Complicates matters for conc? *)
   8.332 @@ -349,24 +349,24 @@
   8.333  \     (? us v. w = concat us @ v & \
   8.334  \              (!u:set us. u ~= [] & accepts A u) & \
   8.335  \              (start A,r) : steps A v)";
   8.336 -by(rev_induct_tac "w" 1);
   8.337 +by (rev_induct_tac "w" 1);
   8.338   by (Simp_tac 1);
   8.339 - by(res_inst_tac [("x","[]")] exI 1);
   8.340 + by (res_inst_tac [("x","[]")] exI 1);
   8.341   by (Simp_tac 1);
   8.342  by (Simp_tac 1);
   8.343  by (Clarify_tac 1);
   8.344 -by(etac allE 1 THEN mp_tac 1);
   8.345 +by (etac allE 1 THEN mp_tac 1);
   8.346  by (Clarify_tac 1);
   8.347 -be disjE 1;
   8.348 - by(res_inst_tac [("x","us")] exI 1);
   8.349 - by(Asm_simp_tac 1);
   8.350 - by(Blast_tac 1);
   8.351 -by(exhaust_tac "v" 1);
   8.352 - by(res_inst_tac [("x","us")] exI 1);
   8.353 - by(Asm_full_simp_tac 1);
   8.354 -by(res_inst_tac [("x","us@[v]")] exI 1);
   8.355 -by(asm_full_simp_tac (simpset() addsimps [accepts_conv_steps]) 1);
   8.356 -by(Blast_tac 1);
   8.357 +by (etac disjE 1);
   8.358 + by (res_inst_tac [("x","us")] exI 1);
   8.359 + by (Asm_simp_tac 1);
   8.360 + by (Blast_tac 1);
   8.361 +by (exhaust_tac "v" 1);
   8.362 + by (res_inst_tac [("x","us")] exI 1);
   8.363 + by (Asm_full_simp_tac 1);
   8.364 +by (res_inst_tac [("x","us@[v]")] exI 1);
   8.365 +by (asm_full_simp_tac (simpset() addsimps [accepts_conv_steps]) 1);
   8.366 +by (Blast_tac 1);
   8.367  qed_spec_mp "start_steps_plusD";
   8.368  
   8.369  Goal
   8.370 @@ -374,54 +374,54 @@
   8.371  \     (? us v. w = concat us @ v & \
   8.372  \              (!u:set us. accepts A u) & \
   8.373  \              (start A,r) : steps A v)";
   8.374 -by(rev_induct_tac "w" 1);
   8.375 +by (rev_induct_tac "w" 1);
   8.376   by (Simp_tac 1);
   8.377 - by(res_inst_tac [("x","[]")] exI 1);
   8.378 + by (res_inst_tac [("x","[]")] exI 1);
   8.379   by (Simp_tac 1);
   8.380  by (Simp_tac 1);
   8.381  by (Clarify_tac 1);
   8.382 -by(etac allE 1 THEN mp_tac 1);
   8.383 +by (etac allE 1 THEN mp_tac 1);
   8.384  by (Clarify_tac 1);
   8.385 -be disjE 1;
   8.386 - by(res_inst_tac [("x","us")] exI 1);
   8.387 - by(Asm_simp_tac 1);
   8.388 - by(Blast_tac 1);
   8.389 -by(res_inst_tac [("x","us@[v]")] exI 1);
   8.390 -by(asm_full_simp_tac (simpset() addsimps [accepts_conv_steps]) 1);
   8.391 -by(Blast_tac 1);
   8.392 +by (etac disjE 1);
   8.393 + by (res_inst_tac [("x","us")] exI 1);
   8.394 + by (Asm_simp_tac 1);
   8.395 + by (Blast_tac 1);
   8.396 +by (res_inst_tac [("x","us@[v]")] exI 1);
   8.397 +by (asm_full_simp_tac (simpset() addsimps [accepts_conv_steps]) 1);
   8.398 +by (Blast_tac 1);
   8.399  qed_spec_mp "start_steps_plusD";
   8.400  
   8.401  Goal
   8.402   "us ~= [] --> (!u : set us. accepts A u) --> accepts (plus A) (concat us)";
   8.403 -by(simp_tac (simpset() addsimps [accepts_conv_steps]) 1);
   8.404 -by(rev_induct_tac "us" 1);
   8.405 - by(Simp_tac 1);
   8.406 -by(rename_tac "u us" 1);
   8.407 -by(Simp_tac 1);
   8.408 +by (simp_tac (simpset() addsimps [accepts_conv_steps]) 1);
   8.409 +by (rev_induct_tac "us" 1);
   8.410 + by (Simp_tac 1);
   8.411 +by (rename_tac "u us" 1);
   8.412 +by (Simp_tac 1);
   8.413  by (Clarify_tac 1);
   8.414 -by(case_tac "us = []" 1);
   8.415 - by(Asm_full_simp_tac 1);
   8.416 - by(blast_tac (claset() addIs [steps_plusI,fin_steps_plusI]) 1);
   8.417 +by (case_tac "us = []" 1);
   8.418 + by (Asm_full_simp_tac 1);
   8.419 + by (blast_tac (claset() addIs [steps_plusI,fin_steps_plusI]) 1);
   8.420  by (Clarify_tac 1);
   8.421 -by(case_tac "u = []" 1);
   8.422 - by(Asm_full_simp_tac 1);
   8.423 - by(blast_tac (claset() addIs [steps_plusI,fin_steps_plusI]) 1);
   8.424 -by(Asm_full_simp_tac 1);
   8.425 -by(blast_tac (claset() addIs [steps_plusI,fin_steps_plusI]) 1);
   8.426 +by (case_tac "u = []" 1);
   8.427 + by (Asm_full_simp_tac 1);
   8.428 + by (blast_tac (claset() addIs [steps_plusI,fin_steps_plusI]) 1);
   8.429 +by (Asm_full_simp_tac 1);
   8.430 +by (blast_tac (claset() addIs [steps_plusI,fin_steps_plusI]) 1);
   8.431  qed_spec_mp "steps_star_cycle";
   8.432  
   8.433  Goal
   8.434   "accepts (plus A) w = \
   8.435  \ (? us. us ~= [] & w = concat us & (!u : set us. accepts A u))";
   8.436 -br iffI 1;
   8.437 - by(asm_full_simp_tac (simpset() addsimps [accepts_conv_steps]) 1);
   8.438 +by (rtac iffI 1);
   8.439 + by (asm_full_simp_tac (simpset() addsimps [accepts_conv_steps]) 1);
   8.440   by (Clarify_tac 1);
   8.441 - bd start_steps_plusD 1;
   8.442 + by (dtac start_steps_plusD 1);
   8.443   by (Clarify_tac 1);
   8.444 - by(res_inst_tac [("x","us@[v]")] exI 1);
   8.445 - by(asm_full_simp_tac (simpset() addsimps [accepts_conv_steps]) 1);
   8.446 - by(Blast_tac 1);
   8.447 -by(blast_tac (claset() addIs [steps_star_cycle]) 1);
   8.448 + by (res_inst_tac [("x","us@[v]")] exI 1);
   8.449 + by (asm_full_simp_tac (simpset() addsimps [accepts_conv_steps]) 1);
   8.450 + by (Blast_tac 1);
   8.451 +by (blast_tac (claset() addIs [steps_star_cycle]) 1);
   8.452  qed "accepts_plus";
   8.453  AddIffs [accepts_plus];
   8.454  
   8.455 @@ -432,24 +432,24 @@
   8.456  Goalw [star_def]
   8.457  "accepts (star A) w = \
   8.458  \ (? us. (!u : set us. accepts A u) & w = concat us)";
   8.459 -br iffI 1;
   8.460 +by (rtac iffI 1);
   8.461   by (Clarify_tac 1);
   8.462 - be disjE 1;
   8.463 -  by(res_inst_tac [("x","[]")] exI 1);
   8.464 -  by(Simp_tac 1);
   8.465 -  by(Blast_tac 1);
   8.466 - by(Blast_tac 1);
   8.467 -by(Force_tac 1);
   8.468 + by (etac disjE 1);
   8.469 +  by (res_inst_tac [("x","[]")] exI 1);
   8.470 +  by (Simp_tac 1);
   8.471 +  by (Blast_tac 1);
   8.472 + by (Blast_tac 1);
   8.473 +by (Force_tac 1);
   8.474  qed "accepts_star";
   8.475  
   8.476  (***** Correctness of r2n *****)
   8.477  
   8.478  Goal
   8.479   "!w. accepts (rexp2na r) w = (w : lang r)";
   8.480 -by(induct_tac "r" 1);
   8.481 -    by(simp_tac (simpset() addsimps [accepts_conv_steps]) 1);
   8.482 -   by(simp_tac(simpset() addsimps [accepts_atom]) 1);
   8.483 -  by(Asm_simp_tac 1);
   8.484 - by(asm_simp_tac (simpset() addsimps [accepts_conc,RegSet.conc_def]) 1);
   8.485 -by(asm_simp_tac (simpset() addsimps [accepts_star,in_star]) 1);
   8.486 +by (induct_tac "r" 1);
   8.487 +    by (simp_tac (simpset() addsimps [accepts_conv_steps]) 1);
   8.488 +   by (simp_tac(simpset() addsimps [accepts_atom]) 1);
   8.489 +  by (Asm_simp_tac 1);
   8.490 + by (asm_simp_tac (simpset() addsimps [accepts_conc,RegSet.conc_def]) 1);
   8.491 +by (asm_simp_tac (simpset() addsimps [accepts_star,in_star]) 1);
   8.492  qed_spec_mp "accepts_rexp2na";
     9.1 --- a/src/HOL/Lex/RegSet.ML	Fri Jan 29 16:23:56 1999 +0100
     9.2 +++ b/src/HOL/Lex/RegSet.ML	Fri Jan 29 16:26:12 1999 +0100
     9.3 @@ -16,7 +16,7 @@
     9.4  Goal
     9.5   "w : star U = (? us. (!u : set(us). u : U) & (w = concat us))";
     9.6  by (rtac iffI 1);
     9.7 - be star.induct 1;
     9.8 + by (etac star.induct 1);
     9.9    by (res_inst_tac [("x","[]")] exI 1);
    9.10    by (Simp_tac 1);
    9.11   by (Clarify_tac 1);
    10.1 --- a/src/HOL/List.ML	Fri Jan 29 16:23:56 1999 +0100
    10.2 +++ b/src/HOL/List.ML	Fri Jan 29 16:26:12 1999 +0100
    10.3 @@ -384,7 +384,7 @@
    10.4  
    10.5  val prems = Goal "[| P []; !!x xs. P xs ==> P(xs@[x]) |] ==> P xs";
    10.6  by (stac (rev_rev_ident RS sym) 1);
    10.7 -br(read_instantiate [("P","%xs. ?P(rev xs)")]list.induct)1;
    10.8 +by (res_inst_tac [("list", "rev xs")] list.induct 1);
    10.9  by (ALLGOALS Simp_tac);
   10.10  by (resolve_tac prems 1);
   10.11  by (eresolve_tac prems 1);
   10.12 @@ -571,7 +571,7 @@
   10.13  section "nth";
   10.14  
   10.15  Goal "(x#xs)!n = (case n of 0 => x | Suc m => xs!m)";
   10.16 -by(simp_tac (simpset() addsplits [nat.split]) 1);
   10.17 +by (simp_tac (simpset() addsplits [nat.split]) 1);
   10.18  qed "nth_Cons";
   10.19  
   10.20  Goal "!xs. (xs@ys)!n = (if n < length xs then xs!n else ys!(n - length xs))";
   10.21 @@ -630,9 +630,9 @@
   10.22  Addsimps [length_list_update];
   10.23  
   10.24  Goal "!i j. i < length xs  --> (xs[i:=x])!j = (if i=j then x else xs!j)";
   10.25 -by(induct_tac "xs" 1);
   10.26 - by(Simp_tac 1);
   10.27 -by(auto_tac (claset(), simpset() addsimps [nth_Cons] addsplits [nat.split]));
   10.28 +by (induct_tac "xs" 1);
   10.29 + by (Simp_tac 1);
   10.30 +by (auto_tac (claset(), simpset() addsimps [nth_Cons] addsplits [nat.split]));
   10.31  qed_spec_mp "nth_list_update";
   10.32  
   10.33  
   10.34 @@ -874,13 +874,13 @@
   10.35  
   10.36  (* Does not terminate! *)
   10.37  Goal "[i..j(] = (if i<j then i#[Suc i..j(] else [])";
   10.38 -by(induct_tac "j" 1);
   10.39 +by (induct_tac "j" 1);
   10.40  by Auto_tac;
   10.41  qed "upt_rec";
   10.42  
   10.43  Goal "j<=i ==> [i..j(] = []";
   10.44 -by(stac upt_rec 1);
   10.45 -by(Asm_simp_tac 1);
   10.46 +by (stac upt_rec 1);
   10.47 +by (Asm_simp_tac 1);
   10.48  qed "upt_conv_Nil";
   10.49  Addsimps [upt_conv_Nil];
   10.50  
   10.51 @@ -889,27 +889,27 @@
   10.52  qed "upt_Suc";
   10.53  
   10.54  Goal "i<j ==> [i..j(] = i#[Suc i..j(]";
   10.55 -br trans 1;
   10.56 -by(stac upt_rec 1);
   10.57 -br refl 2;
   10.58 +by (rtac trans 1);
   10.59 +by (stac upt_rec 1);
   10.60 +by (rtac refl 2);
   10.61  by (Asm_simp_tac 1);
   10.62  qed "upt_conv_Cons";
   10.63  
   10.64  Goal "length [i..j(] = j-i";
   10.65 -by(induct_tac "j" 1);
   10.66 +by (induct_tac "j" 1);
   10.67   by (Simp_tac 1);
   10.68 -by(asm_simp_tac (simpset() addsimps [Suc_diff_le]) 1);
   10.69 +by (asm_simp_tac (simpset() addsimps [Suc_diff_le]) 1);
   10.70  qed "length_upt";
   10.71  Addsimps [length_upt];
   10.72  
   10.73  Goal "i+k < j --> [i..j(] ! k = i+k";
   10.74 -by(induct_tac "j" 1);
   10.75 - by(Simp_tac 1);
   10.76 -by(asm_simp_tac (simpset() addsimps [nth_append,less_diff_conv]@add_ac) 1);
   10.77 -by(Clarify_tac 1);
   10.78 -by(subgoal_tac "n=i+k" 1);
   10.79 - by(Asm_simp_tac 2);
   10.80 -by(Asm_simp_tac 1);
   10.81 +by (induct_tac "j" 1);
   10.82 + by (Simp_tac 1);
   10.83 +by (asm_simp_tac (simpset() addsimps [nth_append,less_diff_conv]@add_ac) 1);
   10.84 +by (Clarify_tac 1);
   10.85 +by (subgoal_tac "n=i+k" 1);
   10.86 + by (Asm_simp_tac 2);
   10.87 +by (Asm_simp_tac 1);
   10.88  qed_spec_mp "nth_upt";
   10.89  Addsimps [nth_upt];
   10.90  
    11.1 --- a/src/HOL/Quot/FRACT.ML	Fri Jan 29 16:23:56 1999 +0100
    11.2 +++ b/src/HOL/Quot/FRACT.ML	Fri Jan 29 16:26:12 1999 +0100
    11.3 @@ -7,11 +7,11 @@
    11.4  
    11.5  Goalw [per_def,per_NP_def]
    11.6  "(op ===)=(%x y. fst(rep_NP x)*snd(rep_NP y)=fst(rep_NP y)*snd(rep_NP x))";
    11.7 -br refl 1;
    11.8 +by (rtac refl 1);
    11.9  qed "inst_NP_per";
   11.10  
   11.11  
   11.12  Goalw [half_def] "half = <[abs_NP(n,2*n)]>";
   11.13 -br per_class_eqI 1;
   11.14 +by (rtac per_class_eqI 1);
   11.15  by (simp_tac (simpset() addsimps [inst_NP_per]) 1);
   11.16  qed "test";
    12.1 --- a/src/HOL/Quot/HQUOT.ML	Fri Jan 29 16:23:56 1999 +0100
    12.2 +++ b/src/HOL/Quot/HQUOT.ML	Fri Jan 29 16:26:12 1999 +0100
    12.3 @@ -124,33 +124,33 @@
    12.4  
    12.5  (* theorems for any_in *)
    12.6  Goalw [any_in_def,peclass_def] "any_in<[(s::'a::er)]>===s";
    12.7 -br selectI2 1;
    12.8 -br refl 1;
    12.9 +by (rtac selectI2 1);
   12.10 +by (rtac refl 1);
   12.11  by (fold_goals_tac [peclass_def]);
   12.12 -be er_class_eqE 1;
   12.13 +by (etac er_class_eqE 1);
   12.14  qed "er_any_in_class";
   12.15  
   12.16  Goalw [any_in_def,peclass_def] "s:D==>any_in<[s]>===s";
   12.17 -br selectI2 1;
   12.18 -br refl 1;
   12.19 +by (rtac selectI2 1);
   12.20 +by (rtac refl 1);
   12.21  by (fold_goals_tac [peclass_def]);
   12.22 -br per_sym 1;
   12.23 -be per_class_eqE 1;
   12.24 -be sym 1;
   12.25 +by (rtac per_sym 1);
   12.26 +by (etac per_class_eqE 1);
   12.27 +by (etac sym 1);
   12.28  qed "per_any_in_class";
   12.29  
   12.30  Goal "<[any_in (s::'a::er quot)]> = s";
   12.31 -br per_class_all 1;
   12.32 -br allI 1;
   12.33 -br (er_any_in_class RS per_class_eqI) 1;
   12.34 +by (rtac per_class_all 1);
   12.35 +by (rtac allI 1);
   12.36 +by (rtac (er_any_in_class RS per_class_eqI) 1);
   12.37  qed "er_class_any_in";
   12.38  
   12.39  (* equivalent theorem for per would need !x.x:D *)
   12.40  Goal "!x::'a::per. x:D==><[any_in (q::'a::per quot)]> = q";
   12.41 -br per_class_all 1;
   12.42 -br allI 1;
   12.43 -br (per_any_in_class RS per_class_eqI) 1;
   12.44 -be spec 1;
   12.45 +by (rtac per_class_all 1);
   12.46 +by (rtac allI 1);
   12.47 +by (rtac (per_any_in_class RS per_class_eqI) 1);
   12.48 +by (etac spec 1);
   12.49  qed "per_class_any_in";
   12.50  
   12.51  (* is like theorem for class er *)
    13.1 --- a/src/HOL/Quot/PER.ML	Fri Jan 29 16:23:56 1999 +0100
    13.2 +++ b/src/HOL/Quot/PER.ML	Fri Jan 29 16:26:12 1999 +0100
    13.3 @@ -12,7 +12,7 @@
    13.4  
    13.5  (* Witness that quot is not empty *)
    13.6  Goal "?z:{s.? r.!y. y:s=y===r}";
    13.7 -br CollectI 1;
    13.8 +by (rtac CollectI 1);
    13.9  by (res_inst_tac [("x","x")] exI 1);
   13.10  by (rtac allI 1);
   13.11  by (rtac mem_Collect_eq 1);
    14.1 --- a/src/HOL/Real/Real.ML	Fri Jan 29 16:23:56 1999 +0100
    14.2 +++ b/src/HOL/Real/Real.ML	Fri Jan 29 16:26:12 1999 +0100
    14.3 @@ -243,8 +243,8 @@
    14.4  qed "real_less_add_left_cancel";
    14.5  
    14.6  Goal "[| 0r < x; 0r < y |] ==> 0r < x + y";
    14.7 -be real_less_trans 1;
    14.8 -bd real_add_less_mono2 1;
    14.9 +by (etac real_less_trans 1);
   14.10 +by (dtac real_add_less_mono2 1);
   14.11  by (Full_simp_tac 1);
   14.12  qed "real_add_order";
   14.13  
   14.14 @@ -255,9 +255,9 @@
   14.15  qed "real_le_add_order";
   14.16  
   14.17  Goal "[| R1 < S1; R2 < S2 |] ==> R1 + R2 < S1 + (S2::real)";
   14.18 -bd real_add_less_mono1 1;
   14.19 -be real_less_trans 1;
   14.20 -be real_add_less_mono2 1;
   14.21 +by (dtac real_add_less_mono1 1);
   14.22 +by (etac real_less_trans 1);
   14.23 +by (etac real_add_less_mono2 1);
   14.24  qed "real_add_less_mono";
   14.25  
   14.26  Goal "!!(q1::real). q1 <= q2  ==> x + q1 <= x + q2";
   14.27 @@ -265,8 +265,8 @@
   14.28  qed "real_add_left_le_mono1";
   14.29  
   14.30  Goal "[|i<=j;  k<=l |] ==> i + k <= j + (l::real)";
   14.31 -bd real_add_le_mono1 1;
   14.32 -be real_le_trans 1;
   14.33 +by (dtac real_add_le_mono1 1);
   14.34 +by (etac real_le_trans 1);
   14.35  by (Simp_tac 1);
   14.36  qed "real_add_le_mono";
   14.37  
    15.1 --- a/src/HOL/Trancl.ML	Fri Jan 29 16:23:56 1999 +0100
    15.2 +++ b/src/HOL/Trancl.ML	Fri Jan 29 16:26:12 1999 +0100
    15.3 @@ -312,7 +312,7 @@
    15.4  \     ==> P(a)";
    15.5  by (rtac ((major RS converseI RS trancl_converseI) RS trancl_induct) 1);
    15.6   by (resolve_tac prems 1);
    15.7 - be converseD 1;
    15.8 + by (etac converseD 1);
    15.9  by (blast_tac (claset() addIs prems addSDs [trancl_converseD])1);
   15.10  qed "converse_trancl_induct";
   15.11