expandshort;
authorwenzelm
Tue Dec 16 17:58:03 1997 +0100 (1997-12-16)
changeset 4423a129b817b58a
parent 4422 21238c9d363e
child 4424 1f15655f7307
expandshort;
src/CCL/CCL.ML
src/CCL/Hered.ML
src/FOL/ex/Nat2.ML
src/HOL/Arith.ML
src/HOL/Auth/Shared.ML
src/HOL/Auth/TLS.ML
src/HOL/Divides.ML
src/HOL/Finite.ML
src/HOL/Integ/Group.ML
src/HOL/Integ/IntRingDefs.ML
src/HOL/Integ/Ring.ML
src/HOL/Lex/Prefix.ML
src/HOL/Lex/Regset_of_auto.ML
src/HOL/List.ML
src/HOL/Map.ML
src/HOL/MiniML/Maybe.ML
src/HOL/MiniML/W.ML
src/HOL/NatDef.ML
src/HOL/Prod.ML
src/HOL/Relation.ML
src/HOL/Set.ML
src/HOL/TLA/TLA.ML
src/HOL/equalities.ML
src/HOL/ex/Qsort.ML
src/HOL/ex/Recdef.ML
src/HOLCF/Cfun3.ML
src/HOLCF/Discrete.ML
src/HOLCF/Fix.ML
src/HOLCF/IMP/HoareEx.ML
src/HOLCF/IOA/ABP/Correctness.ML
src/HOLCF/IOA/ABP/Lemmas.ML
src/HOLCF/IOA/ABP/ROOT.ML
src/HOLCF/IOA/NTP/Abschannel.ML
src/HOLCF/IOA/NTP/Impl.ML
src/HOLCF/IOA/NTP/Lemmas.ML
src/HOLCF/IOA/NTP/Multiset.ML
src/HOLCF/IOA/NTP/ROOT.ML
src/HOLCF/IOA/NTP/Receiver.ML
src/HOLCF/IOA/NTP/Sender.ML
src/HOLCF/IOA/meta_theory/Automata.ML
src/HOLCF/IOA/meta_theory/CompoExecs.ML
src/HOLCF/IOA/meta_theory/CompoScheds.ML
src/HOLCF/IOA/meta_theory/CompoTraces.ML
src/HOLCF/IOA/meta_theory/RefMappings.ML
src/HOLCF/IOA/meta_theory/Traces.ML
src/HOLCF/Porder0.ML
src/HOLCF/Tr.ML
src/HOLCF/ex/Dnat.ML
src/LCF/ex/ex.ML
     1.1 --- a/src/CCL/CCL.ML	Tue Dec 16 15:17:26 1997 +0100
     1.2 +++ b/src/CCL/CCL.ML	Tue Dec 16 17:58:03 1997 +0100
     1.3 @@ -166,8 +166,8 @@
     1.4  \                (EX a a' b b'. t=<a,b> &  t'=<a',b'>  & a [= a' & b [= b') | \
     1.5  \                (EX f f'. t=lam x. f(x) &  t'=lam x. f'(x) & (ALL x. f(x) [= f'(x)))";
     1.6  by (simp_tac (ccl_ss addsimps [PO_iff] delsimps ex_simps) 1);
     1.7 -br (rewrite_rule [POgen_def,SIM_def] 
     1.8 -                 (POgen_mono RS (PO_def RS def_gfp_Tarski) RS XHlemma1)) 1;
     1.9 +by (rtac (rewrite_rule [POgen_def,SIM_def] 
    1.10 +                 (POgen_mono RS (PO_def RS def_gfp_Tarski) RS XHlemma1)) 1);
    1.11  by (rtac (iff_refl RS XHlemma2) 1);
    1.12  qed "poXH";
    1.13  
    1.14 @@ -292,8 +292,8 @@
    1.15  \             (EX f f'. t=lam x. f(x) &  t'=lam x. f'(x) & (ALL x. <f(x),f'(x)> : EQ))" 1);
    1.16  by (etac rev_mp 1);
    1.17  by (simp_tac (CCL_ss addsimps [EQ_iff RS iff_sym]) 1);
    1.18 -br (rewrite_rule [EQgen_def,SIM_def]
    1.19 -                 (EQgen_mono RS (EQ_def RS def_gfp_Tarski) RS XHlemma1)) 1;
    1.20 +by (rtac (rewrite_rule [EQgen_def,SIM_def]
    1.21 +                 (EQgen_mono RS (EQ_def RS def_gfp_Tarski) RS XHlemma1)) 1);
    1.22  by (rtac (iff_refl RS XHlemma2) 1);
    1.23  qed "eqXH";
    1.24  
     2.1 --- a/src/CCL/Hered.ML	Tue Dec 16 15:17:26 1997 +0100
     2.2 +++ b/src/CCL/Hered.ML	Tue Dec 16 17:58:03 1997 +0100
     2.3 @@ -26,8 +26,8 @@
     2.4  goal Hered.thy
     2.5    "t : HTT <-> t=true | t=false | (EX a b. t=<a,b> & a : HTT & b : HTT) | \
     2.6  \                                  (EX f. t=lam x. f(x) & (ALL x. f(x) : HTT))";
     2.7 -br (rewrite_rule [HTTgen_def] 
     2.8 -                 (HTTgen_mono RS (HTT_def RS def_gfp_Tarski) RS XHlemma1)) 1;
     2.9 +by (rtac (rewrite_rule [HTTgen_def] 
    2.10 +                 (HTTgen_mono RS (HTT_def RS def_gfp_Tarski) RS XHlemma1)) 1);
    2.11  by (fast_tac set_cs 1);
    2.12  qed "HTTXH";
    2.13  
     3.1 --- a/src/FOL/ex/Nat2.ML	Tue Dec 16 15:17:26 1997 +0100
     3.2 +++ b/src/FOL/ex/Nat2.ML	Tue Dec 16 17:58:03 1997 +0100
     3.3 @@ -134,7 +134,7 @@
     3.4  by (Simp_tac 1);
     3.5  by (resolve_tac [impI RS allI] 1);
     3.6  by (ALL_IND_TAC nat_exh Simp_tac 1);
     3.7 -by (resolve_tac [impI] 1);
     3.8 +by (rtac impI 1);
     3.9  by (ALL_IND_TAC nat_exh Simp_tac 1);
    3.10  by (Fast_tac 1);
    3.11  qed "le_trans";
     4.1 --- a/src/HOL/Arith.ML	Tue Dec 16 15:17:26 1997 +0100
     4.2 +++ b/src/HOL/Arith.ML	Tue Dec 16 17:58:03 1997 +0100
     4.3 @@ -29,13 +29,13 @@
     4.4     However, none of the generalizations are currently in the simpset,
     4.5     and I dread to think what happens if I put them in *)
     4.6  goal Arith.thy "!!n. 0 < n ==> Suc(n-1) = n";
     4.7 -by(asm_simp_tac (simpset() addsplits [expand_nat_case]) 1);
     4.8 +by (asm_simp_tac (simpset() addsplits [expand_nat_case]) 1);
     4.9  qed "Suc_pred";
    4.10  Addsimps [Suc_pred];
    4.11  
    4.12  (* Generalize? *)
    4.13  goal Arith.thy "!!n. 0<n ==> n-1 < n";
    4.14 -by(asm_simp_tac (simpset() addsplits [expand_nat_case]) 1);
    4.15 +by (asm_simp_tac (simpset() addsplits [expand_nat_case]) 1);
    4.16  qed "pred_less";
    4.17  Addsimps [pred_less];
    4.18  
    4.19 @@ -105,7 +105,7 @@
    4.20  AddIffs [add_is_0];
    4.21  
    4.22  goal Arith.thy "(0<m+n) = (0<m | 0<n)";
    4.23 -by(simp_tac (simpset() delsimps [neq0_conv] addsimps [neq0_conv RS sym]) 1);
    4.24 +by (simp_tac (simpset() delsimps [neq0_conv] addsimps [neq0_conv RS sym]) 1);
    4.25  qed "add_gr_0";
    4.26  AddIffs [add_gr_0];
    4.27  
    4.28 @@ -377,7 +377,7 @@
    4.29     could be got rid of if diff_diff_left were in the simpset...
    4.30  *)
    4.31  goal Arith.thy "(Suc m - n)-1 = m - n";
    4.32 -by(simp_tac (simpset() addsimps [diff_diff_left]) 1);
    4.33 +by (simp_tac (simpset() addsimps [diff_diff_left]) 1);
    4.34  qed "pred_Suc_diff";
    4.35  Addsimps [pred_Suc_diff];
    4.36  
    4.37 @@ -554,13 +554,13 @@
    4.38  Addsimps [mult_less_cancel1, mult_less_cancel2];
    4.39  
    4.40  goal Arith.thy "(Suc k * m < Suc k * n) = (m < n)";
    4.41 -br mult_less_cancel1 1;
    4.42 +by (rtac mult_less_cancel1 1);
    4.43  by (Simp_tac 1);
    4.44  qed "Suc_mult_less_cancel1";
    4.45  
    4.46  goalw Arith.thy [le_def] "(Suc k * m <= Suc k * n) = (m <= n)";
    4.47  by (simp_tac (simpset_of HOL.thy) 1);
    4.48 -br Suc_mult_less_cancel1 1;
    4.49 +by (rtac Suc_mult_less_cancel1 1);
    4.50  qed "Suc_mult_le_cancel1";
    4.51  
    4.52  goal Arith.thy "!!k. 0<k ==> (m*k = n*k) = (m=n)";
    4.53 @@ -578,7 +578,7 @@
    4.54  Addsimps [mult_cancel1, mult_cancel2];
    4.55  
    4.56  goal Arith.thy "(Suc k * m = Suc k * n) = (m = n)";
    4.57 -br mult_cancel1 1;
    4.58 +by (rtac mult_cancel1 1);
    4.59  by (Simp_tac 1);
    4.60  qed "Suc_mult_cancel1";
    4.61  
     5.1 --- a/src/HOL/Auth/Shared.ML	Tue Dec 16 15:17:26 1997 +0100
     5.2 +++ b/src/HOL/Auth/Shared.ML	Tue Dec 16 17:58:03 1997 +0100
     5.3 @@ -75,7 +75,7 @@
     5.4  AddIffs [shrK_in_initState];
     5.5  
     5.6  goal thy "Key (shrK A) : used evs";
     5.7 -br initState_into_used 1;
     5.8 +by (rtac initState_into_used 1);
     5.9  by (Blast_tac 1);
    5.10  qed "shrK_in_used";
    5.11  AddIffs [shrK_in_used];
     6.1 --- a/src/HOL/Auth/TLS.ML	Tue Dec 16 15:17:26 1997 +0100
     6.2 +++ b/src/HOL/Auth/TLS.ML	Tue Dec 16 17:58:03 1997 +0100
     6.3 @@ -35,13 +35,13 @@
     6.4  (*** clientK and serverK make symmetric keys; no clashes with pubK or priK ***)
     6.5  
     6.6  goal thy "pubK A ~= sessionK arg";
     6.7 -br notI 1;
     6.8 +by (rtac notI 1);
     6.9  by (dres_inst_tac [("f","isSymKey")] arg_cong 1);
    6.10  by (Full_simp_tac 1);
    6.11  qed "pubK_neq_sessionK";
    6.12  
    6.13  goal thy "priK A ~= sessionK arg";
    6.14 -br notI 1;
    6.15 +by (rtac notI 1);
    6.16  by (dres_inst_tac [("f","isSymKey")] arg_cong 1);
    6.17  by (Full_simp_tac 1);
    6.18  qed "priK_neq_sessionK";
    6.19 @@ -274,7 +274,7 @@
    6.20  \             : parts (spies evs);                          \
    6.21  \           evs : tls;  A ~: bad |]                         \
    6.22  \        ==> Notes A {|Agent B, Nonce PMS|} : set evs";
    6.23 -be rev_mp 1;
    6.24 +by (etac rev_mp 1);
    6.25  by (parts_induct_tac 1);
    6.26  by (Fake_parts_insert_tac 1);
    6.27  val lemma = result();
     7.1 --- a/src/HOL/Divides.ML	Tue Dec 16 15:17:26 1997 +0100
     7.2 +++ b/src/HOL/Divides.ML	Tue Dec 16 17:58:03 1997 +0100
     7.3 @@ -110,7 +110,7 @@
     7.4  
     7.5  (* a simple rearrangement of mod_div_equality: *)
     7.6  goal thy "!!k. 0<k ==> k*(m div k) = m - (m mod k)";
     7.7 -by(dres_inst_tac [("m","m")] mod_div_equality 1);
     7.8 +by (dres_inst_tac [("m","m")] mod_div_equality 1);
     7.9  by (EVERY1[etac subst, simp_tac (simpset() addsimps mult_ac),
    7.10             K(IF_UNSOLVED no_tac)]);
    7.11  qed "mult_div_cancel";
     8.1 --- a/src/HOL/Finite.ML	Tue Dec 16 15:17:26 1997 +0100
     8.2 +++ b/src/HOL/Finite.ML	Tue Dec 16 17:58:03 1997 +0100
     8.3 @@ -65,7 +65,7 @@
     8.4  val lemma = result();
     8.5  
     8.6  goal Finite.thy "!!A. [| A<=B;  finite B |] ==> finite A";
     8.7 -bd lemma 1;
     8.8 +by (dtac lemma 1);
     8.9  by (Blast_tac 1);
    8.10  qed "finite_subset";
    8.11  
     9.1 --- a/src/HOL/Integ/Group.ML	Tue Dec 16 15:17:26 1997 +0100
     9.2 +++ b/src/HOL/Integ/Group.ML	Tue Dec 16 17:58:03 1997 +0100
     9.3 @@ -103,13 +103,13 @@
     9.4     but are still very useful. They also demonstrate mk_group1_tac.
     9.5  *)
     9.6  goal Group.thy "x-x = (zero::'a::add_group)";
     9.7 -by(mk_group1_tac 1);
     9.8 -by(group1_tac 1);
     9.9 +by (mk_group1_tac 1);
    9.10 +by (group1_tac 1);
    9.11  qed "minus_self_zero";
    9.12  
    9.13  goal Group.thy "x-zero = (x::'a::add_group)";
    9.14 -by(mk_group1_tac 1);
    9.15 -by(group1_tac 1);
    9.16 +by (mk_group1_tac 1);
    9.17 +by (group1_tac 1);
    9.18  qed "minus_zero";
    9.19  
    9.20  (*** Abelian Groups ***)
    9.21 @@ -144,33 +144,33 @@
    9.22        (x-y = z) = (x = z+y) and (x = y-z) = (x+z = y)
    9.23  *)
    9.24  goal Group.thy "x + (y - z) = (x + y) - (z::'a::add_group)";
    9.25 -by(mk_group1_tac 1);
    9.26 -by(group1_tac 1);
    9.27 +by (mk_group1_tac 1);
    9.28 +by (group1_tac 1);
    9.29  qed "plus_minusR";
    9.30  
    9.31  goal Group.thy "(x - y) + z = (x + z) - (y::'a::add_agroup)";
    9.32 -by(mk_group1_tac 1);
    9.33 -by(agroup1_tac 1);
    9.34 +by (mk_group1_tac 1);
    9.35 +by (agroup1_tac 1);
    9.36  qed "plus_minusL";
    9.37  
    9.38  goal Group.thy "(x - y) - z = x - (y + (z::'a::add_agroup))";
    9.39 -by(mk_group1_tac 1);
    9.40 -by(agroup1_tac 1);
    9.41 +by (mk_group1_tac 1);
    9.42 +by (agroup1_tac 1);
    9.43  qed "minus_minusL";
    9.44  
    9.45  goal Group.thy "x - (y - z) = (x + z) - (y::'a::add_agroup)";
    9.46 -by(mk_group1_tac 1);
    9.47 -by(agroup1_tac 1);
    9.48 +by (mk_group1_tac 1);
    9.49 +by (agroup1_tac 1);
    9.50  qed "minus_minusR";
    9.51  
    9.52  goal Group.thy "!!x::'a::add_group. (x-y = z) = (x = z+y)";
    9.53 -by(stac minus_inv 1);
    9.54 -by(fast_tac (claset() addss (HOL_basic_ss addsimps group1_simps)) 1);
    9.55 +by (stac minus_inv 1);
    9.56 +by (fast_tac (claset() addss (HOL_basic_ss addsimps group1_simps)) 1);
    9.57  qed "minusL_iff";
    9.58  
    9.59  goal Group.thy "!!x::'a::add_group. (x = y-z) = (x+z = y)";
    9.60 -by(stac minus_inv 1);
    9.61 -by(fast_tac (claset() addss (HOL_basic_ss addsimps group1_simps)) 1);
    9.62 +by (stac minus_inv 1);
    9.63 +by (fast_tac (claset() addss (HOL_basic_ss addsimps group1_simps)) 1);
    9.64  qed "minusR_iff";
    9.65  
    9.66  val agroup2_simps =
    10.1 --- a/src/HOL/Integ/IntRingDefs.ML	Tue Dec 16 15:17:26 1997 +0100
    10.2 +++ b/src/HOL/Integ/IntRingDefs.ML	Tue Dec 16 17:58:03 1997 +0100
    10.3 @@ -8,9 +8,9 @@
    10.4  open IntRingDefs;
    10.5  
    10.6  goalw thy [zero_int_def,zdiff_def] "(zero-x)+(x::int) = zero";
    10.7 -by(Simp_tac 1);
    10.8 +by (Simp_tac 1);
    10.9  qed "left_inv_int";
   10.10  
   10.11  goalw thy [zero_int_def,zdiff_def] "x-y = (x::int) + (zero-y)";
   10.12 -by(Simp_tac 1);
   10.13 +by (Simp_tac 1);
   10.14  qed "minus_inv_int";
    11.1 --- a/src/HOL/Integ/Ring.ML	Tue Dec 16 15:17:26 1997 +0100
    11.2 +++ b/src/HOL/Integ/Ring.ML	Tue Dec 16 17:58:03 1997 +0100
    11.3 @@ -29,7 +29,7 @@
    11.4    by (rtac refl 3);
    11.5   by (rtac (distribR RS sym) 2);
    11.6  by (rtac trans 1);
    11.7 - br(plus_assoc RS sym) 2;
    11.8 + by (rtac (plus_assoc RS sym) 2);
    11.9  by (rtac trans 1);
   11.10   by (rtac plus_cong 2);
   11.11    by (rtac refl 2);
   11.12 @@ -49,7 +49,7 @@
   11.13    by (rtac refl 3);
   11.14   by (rtac (distribL RS sym) 2);
   11.15  by (rtac trans 1);
   11.16 - br(plus_assoc RS sym) 2;
   11.17 + by (rtac (plus_assoc RS sym) 2);
   11.18  by (rtac trans 1);
   11.19   by (rtac plus_cong 2);
   11.20    by (rtac refl 2);
   11.21 @@ -75,7 +75,7 @@
   11.22    by (rtac refl 3);
   11.23   by (rtac (distribR RS sym) 2);
   11.24  by (rtac trans 1);
   11.25 - br(plus_assoc RS sym) 2;
   11.26 + by (rtac (plus_assoc RS sym) 2);
   11.27  by (rtac trans 1);
   11.28   by (rtac plus_cong 2);
   11.29    by (rtac refl 2);
   11.30 @@ -101,7 +101,7 @@
   11.31    by (rtac refl 3);
   11.32   by (rtac (distribL RS sym) 2);
   11.33  by (rtac trans 1);
   11.34 - br(plus_assoc RS sym) 2;
   11.35 + by (rtac (plus_assoc RS sym) 2);
   11.36  by (rtac trans 1);
   11.37   by (rtac plus_cong 2);
   11.38    by (rtac refl 2);
   11.39 @@ -110,13 +110,13 @@
   11.40  qed "mult_invR";
   11.41  
   11.42  goal Ring.thy "x*(y-z) = (x*y - x*z::'a::ring)";
   11.43 -by(mk_group1_tac 1);
   11.44 -by(simp_tac (HOL_basic_ss addsimps [distribL,mult_invR]) 1);
   11.45 +by (mk_group1_tac 1);
   11.46 +by (simp_tac (HOL_basic_ss addsimps [distribL,mult_invR]) 1);
   11.47  qed "minus_distribL";
   11.48  
   11.49  goal Ring.thy "(x-y)*z = (x*z - y*z::'a::ring)";
   11.50 -by(mk_group1_tac 1);
   11.51 -by(simp_tac (HOL_basic_ss addsimps [distribR,mult_invL]) 1);
   11.52 +by (mk_group1_tac 1);
   11.53 +by (simp_tac (HOL_basic_ss addsimps [distribR,mult_invL]) 1);
   11.54  qed "minus_distribR";
   11.55  
   11.56  val cring_simps = [times_assoc,times_commute,times_commuteL,
    12.1 --- a/src/HOL/Lex/Prefix.ML	Tue Dec 16 15:17:26 1997 +0100
    12.2 +++ b/src/HOL/Lex/Prefix.ML	Tue Dec 16 17:58:03 1997 +0100
    12.3 @@ -35,7 +35,7 @@
    12.4  qed "prefix_Cons";
    12.5  
    12.6  goalw Prefix.thy [prefix_def] "(x#xs <= y#ys) = (x=y & xs<=ys)";
    12.7 -by(Simp_tac 1);
    12.8 +by (Simp_tac 1);
    12.9  by (Fast_tac 1);
   12.10  qed"Cons_prefix_Cons";
   12.11  Addsimps [Cons_prefix_Cons];
    13.1 --- a/src/HOL/Lex/Regset_of_auto.ML	Tue Dec 16 15:17:26 1997 +0100
    13.2 +++ b/src/HOL/Lex/Regset_of_auto.ML	Tue Dec 16 17:58:03 1997 +0100
    13.3 @@ -13,42 +13,42 @@
    13.4  (* Induction over the length of a list: *)
    13.5  val prems = goal thy
    13.6   "(!!xs::'a list. (!ys. length ys < length xs --> P ys) ==> P xs) ==> P xs";
    13.7 -by(res_inst_tac [("P","P"),("r","measure length::('a list * 'a list)set")]
    13.8 +by (res_inst_tac [("P","P"),("r","measure length::('a list * 'a list)set")]
    13.9       wf_induct 1);
   13.10 -by(Simp_tac 1);
   13.11 -by(asm_full_simp_tac (simpset() addsimps [measure_def,inv_image_def]) 1);
   13.12 -bes prems 1;
   13.13 +by (Simp_tac 1);
   13.14 +by (asm_full_simp_tac (simpset() addsimps [measure_def,inv_image_def]) 1);
   13.15 +by (eresolve_tac prems 1);
   13.16  qed "list_length_induct";
   13.17  *)
   13.18  
   13.19  goal thy "(butlast xs = []) = (case xs of [] => True | y#ys => ys=[])";
   13.20 -by(exhaust_tac "xs" 1);
   13.21 -by(ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if])));
   13.22 +by (exhaust_tac "xs" 1);
   13.23 +by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if])));
   13.24  qed "butlast_empty";
   13.25  AddIffs [butlast_empty];
   13.26  
   13.27  goal thy "x:set(butlast xs) --> xs:set xss --> x:set(butlast(concat xss))";
   13.28 -by(induct_tac "xss" 1);
   13.29 - by(Simp_tac 1);
   13.30 -by(asm_simp_tac (simpset() addsimps [butlast_append] delsimps ball_simps
   13.31 +by (induct_tac "xss" 1);
   13.32 + by (Simp_tac 1);
   13.33 +by (asm_simp_tac (simpset() addsimps [butlast_append] delsimps ball_simps
   13.34                             addsplits [expand_if]) 1);
   13.35 -br conjI 1;
   13.36 - by(Clarify_tac 1);
   13.37 - br conjI 1;
   13.38 -  by(Blast_tac 1);
   13.39 - by(Clarify_tac 1);
   13.40 - by(subgoal_tac "xs=[]" 1);
   13.41 -  by(rotate_tac ~1 1);
   13.42 -  by(Asm_full_simp_tac 1);
   13.43 - by(Blast_tac 1);
   13.44 -by(blast_tac (claset() addDs [in_set_butlastD]) 1);
   13.45 +by (rtac conjI 1);
   13.46 + by (Clarify_tac 1);
   13.47 + by (rtac conjI 1);
   13.48 +  by (Blast_tac 1);
   13.49 + by (Clarify_tac 1);
   13.50 + by (subgoal_tac "xs=[]" 1);
   13.51 +  by (rotate_tac ~1 1);
   13.52 +  by (Asm_full_simp_tac 1);
   13.53 + by (Blast_tac 1);
   13.54 +by (blast_tac (claset() addDs [in_set_butlastD]) 1);
   13.55  qed_spec_mp "in_set_butlast_concatI";
   13.56  
   13.57  (* Regular sets *)
   13.58  
   13.59  goal thy "(!xs: set xss. xs:A) --> concat xss : star A";
   13.60 -by(induct_tac "xss" 1);
   13.61 -by(ALLGOALS Asm_full_simp_tac);
   13.62 +by (induct_tac "xss" 1);
   13.63 +by (ALLGOALS Asm_full_simp_tac);
   13.64  qed_spec_mp "concat_in_star";
   13.65  
   13.66  (* The main lemma:
   13.67 @@ -60,162 +60,162 @@
   13.68  \ (!mid:set mids. (deltas A mid k = k) & \
   13.69  \                 (!n:set(butlast(trace A k mid)). n ~= k)) & \
   13.70  \ (!n:set(butlast(trace A k suf)). n ~= k))";
   13.71 -by(induct_tac "xs" 1);
   13.72 - by(Simp_tac 1);
   13.73 -by(rename_tac "a as" 1);
   13.74 -br allI 1;
   13.75 -by(case_tac "A a i = k" 1);
   13.76 - by(strip_tac 1);
   13.77 - by(res_inst_tac[("x","[a]")]exI 1);
   13.78 - by(Asm_full_simp_tac 1);
   13.79 - by(case_tac "k : set(trace A (A a i) as)" 1);
   13.80 -  be allE 1;
   13.81 -  be impE 1;
   13.82 -   ba 1;
   13.83 -  by(REPEAT(etac exE 1));
   13.84 -  by(res_inst_tac[("x","pref#mids")]exI 1);
   13.85 -  by(res_inst_tac[("x","suf")]exI 1);
   13.86 -  by(Asm_full_simp_tac 1);
   13.87 - by(res_inst_tac[("x","[]")]exI 1);
   13.88 - by(res_inst_tac[("x","as")]exI 1);
   13.89 - by(Asm_full_simp_tac 1);
   13.90 - by(blast_tac (claset() addDs [in_set_butlastD]) 1);
   13.91 -by(Asm_simp_tac 1);
   13.92 -br conjI 1;
   13.93 - by(Blast_tac 1);
   13.94 -by(strip_tac 1);
   13.95 -be allE 1;
   13.96 -be impE 1;
   13.97 - ba 1;
   13.98 -by(REPEAT(etac exE 1));
   13.99 -by(res_inst_tac[("x","a#pref")]exI 1);
  13.100 -by(res_inst_tac[("x","mids")]exI 1);
  13.101 -by(res_inst_tac[("x","suf")]exI 1);
  13.102 -by(asm_simp_tac (simpset() addsplits [expand_if]) 1);
  13.103 +by (induct_tac "xs" 1);
  13.104 + by (Simp_tac 1);
  13.105 +by (rename_tac "a as" 1);
  13.106 +by (rtac allI 1);
  13.107 +by (case_tac "A a i = k" 1);
  13.108 + by (strip_tac 1);
  13.109 + by (res_inst_tac[("x","[a]")]exI 1);
  13.110 + by (Asm_full_simp_tac 1);
  13.111 + by (case_tac "k : set(trace A (A a i) as)" 1);
  13.112 +  by (etac allE 1);
  13.113 +  by (etac impE 1);
  13.114 +   by (assume_tac 1);
  13.115 +  by (REPEAT(etac exE 1));
  13.116 +  by (res_inst_tac[("x","pref#mids")]exI 1);
  13.117 +  by (res_inst_tac[("x","suf")]exI 1);
  13.118 +  by (Asm_full_simp_tac 1);
  13.119 + by (res_inst_tac[("x","[]")]exI 1);
  13.120 + by (res_inst_tac[("x","as")]exI 1);
  13.121 + by (Asm_full_simp_tac 1);
  13.122 + by (blast_tac (claset() addDs [in_set_butlastD]) 1);
  13.123 +by (Asm_simp_tac 1);
  13.124 +by (rtac conjI 1);
  13.125 + by (Blast_tac 1);
  13.126 +by (strip_tac 1);
  13.127 +by (etac allE 1);
  13.128 +by (etac impE 1);
  13.129 + by (assume_tac 1);
  13.130 +by (REPEAT(etac exE 1));
  13.131 +by (res_inst_tac[("x","a#pref")]exI 1);
  13.132 +by (res_inst_tac[("x","mids")]exI 1);
  13.133 +by (res_inst_tac[("x","suf")]exI 1);
  13.134 +by (asm_simp_tac (simpset() addsplits [expand_if]) 1);
  13.135  qed_spec_mp "decompose";
  13.136  
  13.137  goal thy "!i. length(trace A i xs) = length xs";
  13.138 -by(induct_tac "xs" 1);
  13.139 -by(ALLGOALS Asm_simp_tac);
  13.140 +by (induct_tac "xs" 1);
  13.141 +by (ALLGOALS Asm_simp_tac);
  13.142  qed "length_trace";
  13.143  Addsimps [length_trace];
  13.144  
  13.145  goal thy "!i. deltas A (xs@ys) i = deltas A ys (deltas A xs i)";
  13.146 -by(induct_tac "xs" 1);
  13.147 -by(ALLGOALS Asm_simp_tac);
  13.148 +by (induct_tac "xs" 1);
  13.149 +by (ALLGOALS Asm_simp_tac);
  13.150  qed "deltas_append";
  13.151  Addsimps [deltas_append];
  13.152  
  13.153  goal thy "!i. trace A i (xs@ys) = trace A i xs @ trace A (deltas A xs i) ys";
  13.154 -by(induct_tac "xs" 1);
  13.155 -by(ALLGOALS Asm_simp_tac);
  13.156 +by (induct_tac "xs" 1);
  13.157 +by (ALLGOALS Asm_simp_tac);
  13.158  qed "trace_append";
  13.159  Addsimps [trace_append];
  13.160  
  13.161  goal thy "(!xs: set xss. deltas A xs i = i) --> \
  13.162  \         trace A i (concat xss) = concat (map (trace A i) xss)";
  13.163 -by(induct_tac "xss" 1);
  13.164 -by(ALLGOALS Asm_simp_tac);
  13.165 +by (induct_tac "xss" 1);
  13.166 +by (ALLGOALS Asm_simp_tac);
  13.167  qed_spec_mp "trace_concat";
  13.168  Addsimps [trace_concat];
  13.169  
  13.170  goal thy "!i. (trace A i xs = []) = (xs = [])";
  13.171 -by(exhaust_tac "xs" 1);
  13.172 -by(ALLGOALS Asm_simp_tac);
  13.173 +by (exhaust_tac "xs" 1);
  13.174 +by (ALLGOALS Asm_simp_tac);
  13.175  qed "trace_is_Nil";
  13.176  Addsimps [trace_is_Nil];
  13.177  
  13.178  goal thy "(trace A i xs = n#ns) = \
  13.179  \         (case xs of [] => False | y#ys => n = A y i & ns = trace A n ys)";
  13.180 -by(exhaust_tac "xs" 1);
  13.181 -by(ALLGOALS Asm_simp_tac);
  13.182 -by(Blast_tac 1);
  13.183 +by (exhaust_tac "xs" 1);
  13.184 +by (ALLGOALS Asm_simp_tac);
  13.185 +by (Blast_tac 1);
  13.186  qed_spec_mp "trace_is_Cons_conv";
  13.187  Addsimps [trace_is_Cons_conv];
  13.188  
  13.189  goal thy "!i. set(trace A i xs) = \
  13.190  \ (if xs=[] then {} else insert(deltas A xs i)(set(butlast(trace A i xs))))";
  13.191 -by(induct_tac "xs" 1);
  13.192 - by(Simp_tac 1);
  13.193 -by(asm_simp_tac (simpset() addsimps [insert_commute] addsplits [expand_if]) 1);
  13.194 +by (induct_tac "xs" 1);
  13.195 + by (Simp_tac 1);
  13.196 +by (asm_simp_tac (simpset() addsimps [insert_commute] addsplits [expand_if]) 1);
  13.197  qed "set_trace_conv";
  13.198  
  13.199  goal thy
  13.200   "(!mid:set mids. deltas A mid k = k) --> deltas A (concat mids) k = k";
  13.201 -by(induct_tac "mids" 1);
  13.202 -by(ALLGOALS Asm_simp_tac);
  13.203 +by (induct_tac "mids" 1);
  13.204 +by (ALLGOALS Asm_simp_tac);
  13.205  qed_spec_mp "deltas_concat";
  13.206  Addsimps [deltas_concat];
  13.207  
  13.208  goal Nat.thy "!!n. [| n < Suc k; n ~= k |] ==> n < k";
  13.209 -be nat_neqE 1;
  13.210 -by(ALLGOALS trans_tac);
  13.211 +by (etac nat_neqE 1);
  13.212 +by (ALLGOALS trans_tac);
  13.213  val lemma = result();
  13.214  
  13.215  
  13.216  goal thy
  13.217   "!i j xs. xs : regset_of A i j k = \
  13.218  \          ((!n:set(butlast(trace A i xs)). n < k) & deltas A xs i = j)";
  13.219 -by(induct_tac "k" 1);
  13.220 - by(simp_tac (simpset() addcongs [conj_cong]
  13.221 +by (induct_tac "k" 1);
  13.222 + by (simp_tac (simpset() addcongs [conj_cong]
  13.223                          addsplits [expand_if,split_list_case]) 1);
  13.224 -by(strip_tac 1);
  13.225 -by(asm_simp_tac (simpset() addsimps [conc_def]) 1);
  13.226 -br iffI 1;
  13.227 - be disjE 1;
  13.228 -  by(Asm_simp_tac 1);
  13.229 - by(REPEAT(eresolve_tac[exE,conjE] 1));
  13.230 - by(Asm_full_simp_tac 1);
  13.231 - by(subgoal_tac
  13.232 +by (strip_tac 1);
  13.233 +by (asm_simp_tac (simpset() addsimps [conc_def]) 1);
  13.234 +by (rtac iffI 1);
  13.235 + by (etac disjE 1);
  13.236 +  by (Asm_simp_tac 1);
  13.237 + by (REPEAT(eresolve_tac[exE,conjE] 1));
  13.238 + by (Asm_full_simp_tac 1);
  13.239 + by (subgoal_tac
  13.240        "(!n:set(butlast(trace A k xsb)). n < Suc k) & deltas A xsb k = k" 1);
  13.241 -  by(asm_simp_tac (simpset() addsplits [expand_if]
  13.242 +  by (asm_simp_tac (simpset() addsplits [expand_if]
  13.243         addsimps [set_trace_conv,butlast_append,ball_Un]) 1);
  13.244 - be star.induct 1;
  13.245 -  by(Simp_tac 1);
  13.246 - by(asm_full_simp_tac (simpset() addsplits [expand_if]
  13.247 + by (etac star.induct 1);
  13.248 +  by (Simp_tac 1);
  13.249 + by (asm_full_simp_tac (simpset() addsplits [expand_if]
  13.250         addsimps [set_trace_conv,butlast_append,ball_Un]) 1);
  13.251 -by(case_tac "k : set(butlast(trace A i xs))" 1);
  13.252 - br disjI1 2;
  13.253 - by(blast_tac (claset() addIs [lemma]) 2);
  13.254 -br disjI2 1;
  13.255 -bd (in_set_butlastD RS decompose) 1;
  13.256 -by(Clarify_tac 1);
  13.257 -by(res_inst_tac [("x","pref")] exI 1);
  13.258 -by(Asm_full_simp_tac 1);
  13.259 -br conjI 1;
  13.260 - br ballI 1;
  13.261 - br lemma 1;
  13.262 -  by(Asm_simp_tac 2);
  13.263 - by(EVERY[dtac bspec 1, atac 2]);
  13.264 - by(Asm_simp_tac 1);
  13.265 -by(res_inst_tac [("x","concat mids")] exI 1);
  13.266 -by(Simp_tac 1);
  13.267 -br conjI 1;
  13.268 - br concat_in_star 1;
  13.269 - by(Asm_simp_tac 1);
  13.270 - br ballI 1;
  13.271 - br ballI 1;
  13.272 - br lemma 1;
  13.273 -  by(Asm_simp_tac 2);
  13.274 - by(EVERY[dtac bspec 1, atac 2]);
  13.275 - by(asm_simp_tac (simpset() addsimps [image_eqI,in_set_butlast_concatI]) 1);
  13.276 -br ballI 1;
  13.277 -br lemma 1;
  13.278 - by(Asm_simp_tac 2);
  13.279 -by(EVERY[dtac bspec 1, atac 2]);
  13.280 -by(Asm_simp_tac 1);
  13.281 +by (case_tac "k : set(butlast(trace A i xs))" 1);
  13.282 + by (rtac disjI1 2);
  13.283 + by (blast_tac (claset() addIs [lemma]) 2);
  13.284 +by (rtac disjI2 1);
  13.285 +by (dtac (in_set_butlastD RS decompose) 1);
  13.286 +by (Clarify_tac 1);
  13.287 +by (res_inst_tac [("x","pref")] exI 1);
  13.288 +by (Asm_full_simp_tac 1);
  13.289 +by (rtac conjI 1);
  13.290 + by (rtac ballI 1);
  13.291 + by (rtac lemma 1);
  13.292 +  by (Asm_simp_tac 2);
  13.293 + by (EVERY[dtac bspec 1, atac 2]);
  13.294 + by (Asm_simp_tac 1);
  13.295 +by (res_inst_tac [("x","concat mids")] exI 1);
  13.296 +by (Simp_tac 1);
  13.297 +by (rtac conjI 1);
  13.298 + by (rtac concat_in_star 1);
  13.299 + by (Asm_simp_tac 1);
  13.300 + by (rtac ballI 1);
  13.301 + by (rtac ballI 1);
  13.302 + by (rtac lemma 1);
  13.303 +  by (Asm_simp_tac 2);
  13.304 + by (EVERY[dtac bspec 1, atac 2]);
  13.305 + by (asm_simp_tac (simpset() addsimps [image_eqI,in_set_butlast_concatI]) 1);
  13.306 +by (rtac ballI 1);
  13.307 +by (rtac lemma 1);
  13.308 + by (Asm_simp_tac 2);
  13.309 +by (EVERY[dtac bspec 1, atac 2]);
  13.310 +by (Asm_simp_tac 1);
  13.311  qed_spec_mp "regset_of_spec";
  13.312  
  13.313  goal thy "!!A. !n. n < k --> (!x. A x n < k) ==> \
  13.314  \         !i. i < k --> (!n:set(trace A i xs). n < k)";
  13.315 -by(induct_tac "xs" 1);
  13.316 - by(ALLGOALS Simp_tac);
  13.317 -by(Blast_tac 1);
  13.318 +by (induct_tac "xs" 1);
  13.319 + by (ALLGOALS Simp_tac);
  13.320 +by (Blast_tac 1);
  13.321  qed_spec_mp "trace_below";
  13.322  
  13.323  goal thy "!!A. [| !n. n < k --> (!x. A x n < k); i < k; j < k |] ==> \
  13.324  \         regset_of A i j k = {xs. deltas A xs i = j}";
  13.325 -br set_ext 1;
  13.326 -by(simp_tac (simpset() addsimps [regset_of_spec]) 1);
  13.327 -by(blast_tac (claset() addDs [trace_below,in_set_butlastD]) 1);
  13.328 +by (rtac set_ext 1);
  13.329 +by (simp_tac (simpset() addsimps [regset_of_spec]) 1);
  13.330 +by (blast_tac (claset() addDs [trace_below,in_set_butlastD]) 1);
  13.331  qed "regset_of_below";
    14.1 --- a/src/HOL/List.ML	Tue Dec 16 15:17:26 1997 +0100
    14.2 +++ b/src/HOL/List.ML	Tue Dec 16 17:58:03 1997 +0100
    14.3 @@ -39,7 +39,7 @@
    14.4  qed_spec_mp "lists_IntI";
    14.5  
    14.6  goal thy "lists (A Int B) = lists A Int lists B";
    14.7 -br (mono_Int RS equalityI) 1;
    14.8 +by (rtac (mono_Int RS equalityI) 1);
    14.9  by (simp_tac (simpset() addsimps [mono_def, lists_mono]) 1);
   14.10  by (blast_tac (claset() addSIs [lists_IntI]) 1);
   14.11  qed "lists_Int_eq";
   14.12 @@ -85,8 +85,8 @@
   14.13  Addsimps [length_rev];
   14.14  
   14.15  goal List.thy "!!xs. xs ~= [] ==> length(tl xs) = pred(length xs)";
   14.16 -by(exhaust_tac "xs" 1);
   14.17 -by(ALLGOALS Asm_full_simp_tac);
   14.18 +by (exhaust_tac "xs" 1);
   14.19 +by (ALLGOALS Asm_full_simp_tac);
   14.20  qed "length_tl";
   14.21  Addsimps [length_tl];
   14.22  
   14.23 @@ -151,17 +151,17 @@
   14.24  
   14.25  goal thy "!ys. length xs = length ys | length us = length vs \
   14.26  \              --> (xs@us = ys@vs) = (xs=ys & us=vs)";
   14.27 -by(induct_tac "xs" 1);
   14.28 - by(rtac allI 1);
   14.29 - by(exhaust_tac "ys" 1);
   14.30 -  by(Asm_simp_tac 1);
   14.31 - by(fast_tac (claset() addIs [less_add_Suc2] addss simpset()
   14.32 +by (induct_tac "xs" 1);
   14.33 + by (rtac allI 1);
   14.34 + by (exhaust_tac "ys" 1);
   14.35 +  by (Asm_simp_tac 1);
   14.36 + by (fast_tac (claset() addIs [less_add_Suc2] addss simpset()
   14.37                        addEs [less_not_refl2 RSN (2,rev_notE)]) 1);
   14.38 -by(rtac allI 1);
   14.39 -by(exhaust_tac "ys" 1);
   14.40 - by(fast_tac (claset() addIs [less_add_Suc2] addss simpset()
   14.41 +by (rtac allI 1);
   14.42 +by (exhaust_tac "ys" 1);
   14.43 + by (fast_tac (claset() addIs [less_add_Suc2] addss simpset()
   14.44                        addEs [(less_not_refl2 RS not_sym) RSN (2,rev_notE)]) 1);
   14.45 -by(Asm_simp_tac 1);
   14.46 +by (Asm_simp_tac 1);
   14.47  qed_spec_mp "append_eq_append_conv";
   14.48  Addsimps [append_eq_append_conv];
   14.49  
   14.50 @@ -246,22 +246,22 @@
   14.51  (* a congruence rule for map: *)
   14.52  goal thy
   14.53   "(xs=ys) --> (!x. x : set ys --> f x = g x) --> map f xs = map g ys";
   14.54 -by(rtac impI 1);
   14.55 -by(hyp_subst_tac 1);
   14.56 -by(induct_tac "ys" 1);
   14.57 -by(ALLGOALS Asm_simp_tac);
   14.58 +by (rtac impI 1);
   14.59 +by (hyp_subst_tac 1);
   14.60 +by (induct_tac "ys" 1);
   14.61 +by (ALLGOALS Asm_simp_tac);
   14.62  val lemma = result();
   14.63  bind_thm("map_cong",impI RSN (2,allI RSN (2,lemma RS mp RS mp)));
   14.64  
   14.65  goal List.thy "(map f xs = []) = (xs = [])";
   14.66 -by(induct_tac "xs" 1);
   14.67 -by(ALLGOALS Asm_simp_tac);
   14.68 +by (induct_tac "xs" 1);
   14.69 +by (ALLGOALS Asm_simp_tac);
   14.70  qed "map_is_Nil_conv";
   14.71  AddIffs [map_is_Nil_conv];
   14.72  
   14.73  goal List.thy "([] = map f xs) = (xs = [])";
   14.74 -by(induct_tac "xs" 1);
   14.75 -by(ALLGOALS Asm_simp_tac);
   14.76 +by (induct_tac "xs" 1);
   14.77 +by (ALLGOALS Asm_simp_tac);
   14.78  qed "Nil_is_map_conv";
   14.79  AddIffs [Nil_is_map_conv];
   14.80  
   14.81 @@ -283,14 +283,14 @@
   14.82  Addsimps[rev_rev_ident];
   14.83  
   14.84  goal thy "(rev xs = []) = (xs = [])";
   14.85 -by(induct_tac "xs" 1);
   14.86 -by(ALLGOALS Asm_simp_tac);
   14.87 +by (induct_tac "xs" 1);
   14.88 +by (ALLGOALS Asm_simp_tac);
   14.89  qed "rev_is_Nil_conv";
   14.90  AddIffs [rev_is_Nil_conv];
   14.91  
   14.92  goal thy "([] = rev xs) = (xs = [])";
   14.93 -by(induct_tac "xs" 1);
   14.94 -by(ALLGOALS Asm_simp_tac);
   14.95 +by (induct_tac "xs" 1);
   14.96 +by (ALLGOALS Asm_simp_tac);
   14.97  qed "Nil_is_rev_conv";
   14.98  AddIffs [Nil_is_rev_conv];
   14.99  
  14.100 @@ -401,14 +401,14 @@
  14.101  Addsimps [concat_append];
  14.102  
  14.103  goal thy "(concat xss = []) = (!xs:set xss. xs=[])";
  14.104 -by(induct_tac "xss" 1);
  14.105 -by(ALLGOALS Asm_simp_tac);
  14.106 +by (induct_tac "xss" 1);
  14.107 +by (ALLGOALS Asm_simp_tac);
  14.108  qed "concat_eq_Nil_conv";
  14.109  AddIffs [concat_eq_Nil_conv];
  14.110  
  14.111  goal thy "([] = concat xss) = (!xs:set xss. xs=[])";
  14.112 -by(induct_tac "xss" 1);
  14.113 -by(ALLGOALS Asm_simp_tac);
  14.114 +by (induct_tac "xss" 1);
  14.115 +by (ALLGOALS Asm_simp_tac);
  14.116  qed "Nil_eq_concat_conv";
  14.117  AddIffs [Nil_eq_concat_conv];
  14.118  
  14.119 @@ -488,39 +488,39 @@
  14.120  (** last & butlast **)
  14.121  
  14.122  goal thy "last(xs@[x]) = x";
  14.123 -by(induct_tac "xs" 1);
  14.124 -by(ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if])));
  14.125 +by (induct_tac "xs" 1);
  14.126 +by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if])));
  14.127  qed "last_snoc";
  14.128  Addsimps [last_snoc];
  14.129  
  14.130  goal thy "butlast(xs@[x]) = xs";
  14.131 -by(induct_tac "xs" 1);
  14.132 -by(ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if])));
  14.133 +by (induct_tac "xs" 1);
  14.134 +by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if])));
  14.135  qed "butlast_snoc";
  14.136  Addsimps [butlast_snoc];
  14.137  
  14.138  goal thy
  14.139    "!ys. butlast (xs@ys) = (if ys=[] then butlast xs else xs@butlast ys)";
  14.140 -by(induct_tac "xs" 1);
  14.141 -by(ALLGOALS(asm_simp_tac (simpset() addsplits [expand_if])));
  14.142 +by (induct_tac "xs" 1);
  14.143 +by (ALLGOALS(asm_simp_tac (simpset() addsplits [expand_if])));
  14.144  qed_spec_mp "butlast_append";
  14.145  
  14.146  goal thy "x:set(butlast xs) --> x:set xs";
  14.147 -by(induct_tac "xs" 1);
  14.148 -by(ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if])));
  14.149 +by (induct_tac "xs" 1);
  14.150 +by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if])));
  14.151  qed_spec_mp "in_set_butlastD";
  14.152  
  14.153  goal thy "!!xs. x:set(butlast xs) ==> x:set(butlast(xs@ys))";
  14.154 -by(asm_simp_tac (simpset() addsimps [butlast_append]
  14.155 +by (asm_simp_tac (simpset() addsimps [butlast_append]
  14.156                            addsplits [expand_if]) 1);
  14.157 -by(blast_tac (claset() addDs [in_set_butlastD]) 1);
  14.158 +by (blast_tac (claset() addDs [in_set_butlastD]) 1);
  14.159  qed "in_set_butlast_appendI1";
  14.160  
  14.161  goal thy "!!xs. x:set(butlast ys) ==> x:set(butlast(xs@ys))";
  14.162 -by(asm_simp_tac (simpset() addsimps [butlast_append]
  14.163 +by (asm_simp_tac (simpset() addsimps [butlast_append]
  14.164                            addsplits [expand_if]) 1);
  14.165 -by(Clarify_tac 1);
  14.166 -by(Full_simp_tac 1);
  14.167 +by (Clarify_tac 1);
  14.168 +by (Full_simp_tac 1);
  14.169  qed "in_set_butlast_appendI2";
  14.170  
  14.171  (** take  & drop **)
  14.172 @@ -720,11 +720,11 @@
  14.173  section "replicate";
  14.174  
  14.175  goal thy "set(replicate (Suc n) x) = {x}";
  14.176 -by(induct_tac "n" 1);
  14.177 -by(ALLGOALS Asm_full_simp_tac);
  14.178 +by (induct_tac "n" 1);
  14.179 +by (ALLGOALS Asm_full_simp_tac);
  14.180  val lemma = result();
  14.181  
  14.182  goal thy "!!n. n ~= 0 ==> set(replicate n x) = {x}";
  14.183 -by(fast_tac (claset() addSDs [not0_implies_Suc] addSIs [lemma]) 1);
  14.184 +by (fast_tac (claset() addSDs [not0_implies_Suc] addSIs [lemma]) 1);
  14.185  qed "set_replicate";
  14.186  Addsimps [set_replicate];
    15.1 --- a/src/HOL/Map.ML	Tue Dec 16 15:17:26 1997 +0100
    15.2 +++ b/src/HOL/Map.ML	Tue Dec 16 17:58:03 1997 +0100
    15.3 @@ -7,72 +7,72 @@
    15.4  *)
    15.5  
    15.6  goalw thy [empty_def] "empty k = None";
    15.7 -by(Simp_tac 1);
    15.8 +by (Simp_tac 1);
    15.9  qed "empty_def2";
   15.10  Addsimps [empty_def2];
   15.11  
   15.12  goalw thy [update_def] "(m[a|->b])x = (if x=a then Some b else m x)";
   15.13 -by(Simp_tac 1);
   15.14 +by (Simp_tac 1);
   15.15  qed "update_def2";
   15.16  Addsimps [update_def2];
   15.17  
   15.18  section "++";
   15.19  
   15.20  goalw thy [override_def] "m ++ empty = m";
   15.21 -by(Simp_tac 1);
   15.22 +by (Simp_tac 1);
   15.23  qed "override_empty";
   15.24  Addsimps [override_empty];
   15.25  
   15.26  goalw thy [override_def] "empty ++ m = m";
   15.27 -by(Simp_tac 1);
   15.28 -br ext 1;
   15.29 -by(split_tac [split_option_case] 1);
   15.30 -by(Simp_tac 1);
   15.31 +by (Simp_tac 1);
   15.32 +by (rtac ext 1);
   15.33 +by (split_tac [split_option_case] 1);
   15.34 +by (Simp_tac 1);
   15.35  qed "empty_override";
   15.36  Addsimps [empty_override];
   15.37  
   15.38  goalw thy [override_def]
   15.39   "((m ++ n) k = Some x) = (n k = Some x | n k = None & m k = Some x)";
   15.40 -by(simp_tac (simpset() addsplits [split_option_case]) 1);
   15.41 +by (simp_tac (simpset() addsplits [split_option_case]) 1);
   15.42  qed_spec_mp "override_Some_iff";
   15.43  
   15.44  bind_thm("override_SomeD", standard(override_Some_iff RS iffD1));
   15.45  
   15.46  goalw thy [override_def]
   15.47   "((m ++ n) k = None) = (n k = None & m k = None)";
   15.48 -by(simp_tac (simpset() addsplits [split_option_case]) 1);
   15.49 +by (simp_tac (simpset() addsplits [split_option_case]) 1);
   15.50  qed "override_None";
   15.51  AddIffs [override_None];
   15.52  
   15.53  goalw thy [override_def] "map_of(xs@ys) = map_of ys ++ map_of xs";
   15.54 -by(induct_tac "xs" 1);
   15.55 -by(Simp_tac 1);
   15.56 -br ext 1;
   15.57 -by(asm_simp_tac (simpset() addsplits [expand_if,split_option_case]) 1);
   15.58 +by (induct_tac "xs" 1);
   15.59 +by (Simp_tac 1);
   15.60 +by (rtac ext 1);
   15.61 +by (asm_simp_tac (simpset() addsplits [expand_if,split_option_case]) 1);
   15.62  qed "map_of_append";
   15.63  Addsimps [map_of_append];
   15.64  
   15.65  section "dom";
   15.66  
   15.67  goalw thy [dom_def] "dom empty = {}";
   15.68 -by(Simp_tac 1);
   15.69 +by (Simp_tac 1);
   15.70  qed "dom_empty";
   15.71  Addsimps [dom_empty];
   15.72  
   15.73  goalw thy [dom_def] "dom(m[a|->b]) = insert a (dom m)";
   15.74 -by(simp_tac (simpset() addsplits [expand_if]) 1);
   15.75 -by(Blast_tac 1);
   15.76 +by (simp_tac (simpset() addsplits [expand_if]) 1);
   15.77 +by (Blast_tac 1);
   15.78  qed "dom_update";
   15.79  Addsimps [dom_update];
   15.80  
   15.81  goalw thy [dom_def] "dom(m++n) = dom n Un dom m";
   15.82 -by(Blast_tac 1);
   15.83 +by (Blast_tac 1);
   15.84  qed "dom_override";
   15.85  Addsimps [dom_override];
   15.86  
   15.87  section "ran";
   15.88  
   15.89  goalw thy [ran_def] "ran empty = {}";
   15.90 -by(Simp_tac 1);
   15.91 +by (Simp_tac 1);
   15.92  qed "ran_empty";
   15.93  Addsimps [ran_empty];
    16.1 --- a/src/HOL/MiniML/Maybe.ML	Tue Dec 16 15:17:26 1997 +0100
    16.2 +++ b/src/HOL/MiniML/Maybe.ML	Tue Dec 16 17:58:03 1997 +0100
    16.3 @@ -18,17 +18,17 @@
    16.4  (* expansion of option_bind *)
    16.5  goalw thy [option_bind_def] "P(option_bind res f) = \
    16.6  \         ((res = None --> P None) & (!s. res = Some s --> P(f s)))";
    16.7 -br split_option_case 1;
    16.8 +by (rtac split_option_case 1);
    16.9  qed "split_option_bind";
   16.10  
   16.11  goal thy
   16.12    "((option_bind m f) = None) = ((m=None) | (? p. m = Some p & f p = None))";
   16.13 -by(simp_tac (simpset() addsplits [split_option_bind]) 1);
   16.14 +by (simp_tac (simpset() addsplits [split_option_bind]) 1);
   16.15  qed "option_bind_eq_None";
   16.16  
   16.17  Addsimps [option_bind_eq_None];
   16.18  
   16.19  (* auxiliary lemma *)
   16.20  goal Maybe.thy "(y = Some x) = (Some x = y)";
   16.21 -by( simp_tac (simpset() addsimps [eq_sym_conv]) 1);
   16.22 +by ( simp_tac (simpset() addsimps [eq_sym_conv]) 1);
   16.23  qed "rotate_Some";
    17.1 --- a/src/HOL/MiniML/W.ML	Tue Dec 16 15:17:26 1997 +0100
    17.2 +++ b/src/HOL/MiniML/W.ML	Tue Dec 16 17:58:03 1997 +0100
    17.3 @@ -24,10 +24,10 @@
    17.4  by (fast_tac (HOL_cs addDs [Suc_leD]) 1);
    17.5  (* case App e1 e2 *)
    17.6  by (simp_tac (simpset() addsplits [split_option_bind]) 1);
    17.7 -by(blast_tac (claset() addIs [le_SucI,le_trans]) 1);
    17.8 +by (blast_tac (claset() addIs [le_SucI,le_trans]) 1);
    17.9  (* case LET e1 e2 *)
   17.10  by (simp_tac (simpset() addsplits [split_option_bind]) 1);
   17.11 -by(blast_tac (claset() addIs [le_trans]) 1);
   17.12 +by (blast_tac (claset() addIs [le_trans]) 1);
   17.13  qed_spec_mp "W_var_ge";
   17.14  
   17.15  Addsimps [W_var_ge];
   17.16 @@ -139,9 +139,9 @@
   17.17  (* 41: case LET e1 e2 *)
   17.18  by (simp_tac (simpset() addsplits [split_option_bind]) 1);
   17.19  by (strip_tac 1);
   17.20 -by(EVERY1[etac allE,etac allE,etac allE,etac allE,etac allE,mp_tac,mp_tac]);
   17.21 +by (EVERY1[etac allE,etac allE,etac allE,etac allE,etac allE,mp_tac,mp_tac]);
   17.22  by (etac conjE 1);
   17.23 -by(EVERY[etac allE 1,etac allE 1,etac allE 1,etac allE 1,etac allE 1,
   17.24 +by (EVERY[etac allE 1,etac allE 1,etac allE 1,etac allE 1,etac allE 1,
   17.25           etac impE 1, mp_tac 2]);
   17.26  by (SELECT_GOAL(rewtac new_tv_def)1);
   17.27  by (Asm_simp_tac 1);
    18.1 --- a/src/HOL/NatDef.ML	Tue Dec 16 15:17:26 1997 +0100
    18.2 +++ b/src/HOL/NatDef.ML	Tue Dec 16 17:58:03 1997 +0100
    18.3 @@ -293,12 +293,12 @@
    18.4  qed "gr_implies_not0";
    18.5  
    18.6  goal thy "(n ~= 0) = (0 < n)";
    18.7 -br iffI 1;
    18.8 - by(etac gr_implies_not0 2);
    18.9 -by(rtac natE 1);
   18.10 - by(contr_tac 1);
   18.11 -by(etac ssubst 1);
   18.12 -by(rtac zero_less_Suc 1);
   18.13 +by (rtac iffI 1);
   18.14 + by (etac gr_implies_not0 2);
   18.15 +by (rtac natE 1);
   18.16 + by (contr_tac 1);
   18.17 +by (etac ssubst 1);
   18.18 +by (rtac zero_less_Suc 1);
   18.19  qed "neq0_conv";
   18.20  Addsimps [neq0_conv];
   18.21  AddSDs [neq0_conv RS iffD1];
   18.22 @@ -306,9 +306,9 @@
   18.23  bind_thm("gr0I", notI RS (neq0_conv RS iffD1));
   18.24  
   18.25  goal thy "(~(0 < n)) = (n=0)";
   18.26 -br iffI 1;
   18.27 - be swap 1;
   18.28 - by(ALLGOALS Asm_full_simp_tac);
   18.29 +by (rtac iffI 1);
   18.30 + by (etac swap 1);
   18.31 + by (ALLGOALS Asm_full_simp_tac);
   18.32  qed "not_gr0";
   18.33  Addsimps [not_gr0];
   18.34  
    19.1 --- a/src/HOL/Prod.ML	Tue Dec 16 15:17:26 1997 +0100
    19.2 +++ b/src/HOL/Prod.ML	Tue Dec 16 17:58:03 1997 +0100
    19.3 @@ -91,7 +91,7 @@
    19.4  which cannot be solved by reflexivity.
    19.5     
    19.6  val [prem] = goal Prod.thy "(!!x. PROP P x) ==> (!!a b. PROP P(a,b))";
    19.7 -br prem 1;
    19.8 +by (rtac prem 1);
    19.9  val lemma1 = result();
   19.10  
   19.11  local
   19.12 @@ -106,13 +106,13 @@
   19.13  
   19.14  
   19.15  val [prem] = goal Prod.thy "(!!a b. PROP P(a,b)) ==> PROP P x";
   19.16 -bw adhoc;
   19.17 -br prem 1;
   19.18 +by (rewtac adhoc);
   19.19 +by (rtac prem 1);
   19.20  val lemma = result();
   19.21  
   19.22  val [prem] = goal Prod.thy "(!!a b. PROP P(a,b)) ==> (!!x. PROP P x)";
   19.23 -br lemma 1;
   19.24 -br prem 1;
   19.25 +by (rtac lemma 1);
   19.26 +by (rtac prem 1);
   19.27  val lemma2 = result();
   19.28  
   19.29  bind_thm("split_paired_all", equal_intr lemma1 lemma2);
    20.1 --- a/src/HOL/Relation.ML	Tue Dec 16 15:17:26 1997 +0100
    20.2 +++ b/src/HOL/Relation.ML	Tue Dec 16 17:58:03 1997 +0100
    20.3 @@ -109,7 +109,7 @@
    20.4  Addsimps [inverse_inverse];
    20.5  
    20.6  goal Relation.thy "(r O s)^-1 = s^-1 O r^-1";
    20.7 -by(Blast_tac 1);
    20.8 +by (Blast_tac 1);
    20.9  qed "inverse_comp";
   20.10  
   20.11  (** Domain **)
    21.1 --- a/src/HOL/Set.ML	Tue Dec 16 15:17:26 1997 +0100
    21.2 +++ b/src/HOL/Set.ML	Tue Dec 16 17:58:03 1997 +0100
    21.3 @@ -452,7 +452,7 @@
    21.4  AddSEs [singletonE];
    21.5  
    21.6  goal Set.thy "{x. x=a} = {a}";
    21.7 -by(Blast_tac 1);
    21.8 +by (Blast_tac 1);
    21.9  qed "singleton_conv";
   21.10  Addsimps [singleton_conv];
   21.11  
    22.1 --- a/src/HOL/TLA/TLA.ML	Tue Dec 16 15:17:26 1997 +0100
    22.2 +++ b/src/HOL/TLA/TLA.ML	Tue Dec 16 17:58:03 1997 +0100
    22.3 @@ -1046,12 +1046,12 @@
    22.4     example of a history variable: existence of a clock
    22.5  
    22.6  goal TLA.thy "(EEX h. Init($h .= #True) .& [](h$ .~= $h))";
    22.7 -br tempI 1;
    22.8 -br historyI 1;
    22.9 -bws action_rews;
   22.10 +by (rtac tempI 1);
   22.11 +by (rtac historyI 1);
   22.12 +by (rewrite_goals_tac action_rews);
   22.13  by (TRYALL (rtac impI));
   22.14  by (TRYALL (etac conjE));
   22.15 -ba 3;
   22.16 +by (assume_tac 3);
   22.17  by (Asm_full_simp_tac 3);
   22.18  by (auto_tac (temp_css addSIs2 [(temp_unlift Init_true) RS iffD2, temp_unlift BoxTrue]));
   22.19  (** solved **)
    23.1 --- a/src/HOL/equalities.ML	Tue Dec 16 15:17:26 1997 +0100
    23.2 +++ b/src/HOL/equalities.ML	Tue Dec 16 17:58:03 1997 +0100
    23.3 @@ -598,7 +598,7 @@
    23.4  qed "subset_iff_psubset_eq";
    23.5  
    23.6  goal thy "(!x. x ~: A) = (A={})";
    23.7 -by(Blast_tac 1);
    23.8 +by (Blast_tac 1);
    23.9  qed "all_not_in_conv";
   23.10  AddIffs [all_not_in_conv];
   23.11  
    24.1 --- a/src/HOL/ex/Qsort.ML	Tue Dec 16 15:17:26 1997 +0100
    24.2 +++ b/src/HOL/ex/Qsort.ML	Tue Dec 16 17:58:03 1997 +0100
    24.3 @@ -15,7 +15,7 @@
    24.4  val [p1] = goalw WF.thy [wf_def]
    24.5  "wf(R) ==> (!Q. (? x. Q x) --> (? min. Q min & (!b. (b,min):R --> (~ Q b))))";
    24.6  by (rtac allI 1);
    24.7 -by(cut_inst_tac[("x","%u.~Q u")](p1 RS spec) 1);
    24.8 +by (cut_inst_tac[("x","%u.~Q u")](p1 RS spec) 1);
    24.9  by (fast_tac HOL_cs 1);
   24.10  val wf_minimal = result();
   24.11  
   24.12 @@ -30,7 +30,7 @@
   24.13  qed "qsort_permutes";
   24.14  
   24.15  goal Qsort.thy "set(qsort le xs) = set xs";
   24.16 -by(simp_tac (simpset() addsimps [set_via_mset,qsort_permutes]) 1);
   24.17 +by (simp_tac (simpset() addsimps [set_via_mset,qsort_permutes]) 1);
   24.18  qed "set_qsort";
   24.19  Addsimps [set_qsort];
   24.20  
    25.1 --- a/src/HOL/ex/Recdef.ML	Tue Dec 16 15:17:26 1997 +0100
    25.2 +++ b/src/HOL/ex/Recdef.ML	Tue Dec 16 17:58:03 1997 +0100
    25.3 @@ -38,9 +38,9 @@
    25.4  (* proving the termination condition: *)
    25.5  val [tc] = mapf.tcs;
    25.6  goalw_cterm [] (cterm_of (sign_of thy) (HOLogic.mk_Trueprop tc));
    25.7 -br allI 1;
    25.8 -by(case_tac "n=0" 1);
    25.9 -by(ALLGOALS Asm_simp_tac);
   25.10 +by (rtac allI 1);
   25.11 +by (case_tac "n=0" 1);
   25.12 +by (ALLGOALS Asm_simp_tac);
   25.13  val lemma = result();
   25.14  
   25.15  (* removing the termination condition from the generated thms: *)
    26.1 --- a/src/HOLCF/Cfun3.ML	Tue Dec 16 15:17:26 1997 +0100
    26.2 +++ b/src/HOLCF/Cfun3.ML	Tue Dec 16 17:58:03 1997 +0100
    26.3 @@ -382,7 +382,7 @@
    26.4  	[
    26.5  	cut_facts_tac prems 1,
    26.6  	rtac allI 1,
    26.7 -	rtac (contlub_cfun_fun RS ssubst) 1,
    26.8 +	stac contlub_cfun_fun 1,
    26.9  	 atac 1,
   26.10  	fast_tac (HOL_cs addSIs [thelubI,chfin,lub_finch2,chfin2finch,ch2ch_fappL])1
   26.11  	]);
    27.1 --- a/src/HOLCF/Discrete.ML	Tue Dec 16 15:17:26 1997 +0100
    27.2 +++ b/src/HOLCF/Discrete.ML	Tue Dec 16 17:58:03 1997 +0100
    27.3 @@ -5,16 +5,16 @@
    27.4  *)
    27.5  
    27.6  goalw thy [undiscr_def] "undiscr(Discr x) = x";
    27.7 -by(Simp_tac 1);
    27.8 +by (Simp_tac 1);
    27.9  qed "undiscr_Discr";
   27.10  Addsimps [undiscr_Discr];
   27.11  
   27.12  goal thy
   27.13   "!!S::nat=>('a::term)discr. is_chain(S) ==> range(%i. f(S i)) = {f(S 0)}";
   27.14 -by(fast_tac (claset() addDs [discr_chain0] addEs [arg_cong]) 1);
   27.15 +by (fast_tac (claset() addDs [discr_chain0] addEs [arg_cong]) 1);
   27.16  qed "discr_chain_f_range0";
   27.17  
   27.18  goalw thy [cont,is_lub,is_ub] "cont(%x::('a::term)discr. f x)";
   27.19 -by(simp_tac (simpset() addsimps [discr_chain_f_range0]) 1);
   27.20 +by (simp_tac (simpset() addsimps [discr_chain_f_range0]) 1);
   27.21  qed "cont_discr";
   27.22  AddIffs [cont_discr];
    28.1 --- a/src/HOLCF/Fix.ML	Tue Dec 16 15:17:26 1997 +0100
    28.2 +++ b/src/HOLCF/Fix.ML	Tue Dec 16 17:58:03 1997 +0100
    28.3 @@ -889,7 +889,7 @@
    28.4  
    28.5  goal Fix.thy "!! P. [| adm (%x. P x --> Q x); adm (%x. Q x --> P x) |] \
    28.6  \           ==> adm (%x. P x = Q x)";
    28.7 -by(subgoal_tac "(%x. P x = Q x) = (%x. (P x --> Q x) & (Q x --> P x))" 1);
    28.8 +by (subgoal_tac "(%x. P x = Q x) = (%x. (P x --> Q x) & (Q x --> P x))" 1);
    28.9  by (Asm_simp_tac 1);
   28.10  by (rtac ext 1);
   28.11  by (fast_tac HOL_cs 1);
    29.1 --- a/src/HOLCF/IMP/HoareEx.ML	Tue Dec 16 15:17:26 1997 +0100
    29.2 +++ b/src/HOLCF/IMP/HoareEx.ML	Tue Dec 16 17:58:03 1997 +0100
    29.3 @@ -8,12 +8,12 @@
    29.4  
    29.5  val prems = goalw thy [hoare_valid_def]
    29.6  "|= {A} c {A} ==> |= {A} WHILE b DO c {%s. A s & ~b s}";
    29.7 -by(cut_facts_tac prems 1);
    29.8 +by (cut_facts_tac prems 1);
    29.9  by (Simp_tac 1);
   29.10  by (rtac fix_ind 1);
   29.11    (* simplifier with enhanced adm-tactic: *)
   29.12    by (Simp_tac 1);
   29.13   by (Simp_tac 1);
   29.14  by (simp_tac (simpset() setloop (split_tac[expand_if])) 1);
   29.15 -by(Blast_tac 1);
   29.16 +by (Blast_tac 1);
   29.17  qed "WHILE_rule_sound";
    30.1 --- a/src/HOLCF/IOA/ABP/Correctness.ML	Tue Dec 16 15:17:26 1997 +0100
    30.2 +++ b/src/HOLCF/IOA/ABP/Correctness.ML	Tue Dec 16 17:58:03 1997 +0100
    30.3 @@ -54,7 +54,7 @@
    30.4   by (REPEAT (rtac allI 1)); 
    30.5   by (rtac impI 1); 
    30.6   by (hyp_subst_tac 1);
    30.7 - by (rtac (expand_if RS ssubst) 1);
    30.8 + by (stac expand_if 1);
    30.9   by (Asm_full_simp_tac 1);
   30.10   by (Asm_full_simp_tac 1);
   30.11  val l_iff_red_nil = result();
   30.12 @@ -72,7 +72,7 @@
   30.13  by (asm_full_simp_tac list_ss 1);
   30.14  by (REPEAT (rtac allI 1)); 
   30.15   by (rtac impI 1); 
   30.16 -by (rtac (expand_if RS ssubst) 1);
   30.17 +by (stac expand_if 1);
   30.18  by (REPEAT(hyp_subst_tac 1));
   30.19  by (etac subst 1);
   30.20  by (Simp_tac 1);
   30.21 @@ -91,7 +91,7 @@
   30.22  by (Asm_full_simp_tac 1);
   30.23  by (REPEAT (etac exE 1));
   30.24  by (Asm_simp_tac 1);
   30.25 -by (rtac (expand_if RS ssubst) 1);
   30.26 +by (stac expand_if 1);
   30.27  by (hyp_subst_tac 1);
   30.28  by (asm_full_simp_tac (simpset() addsimps [reverse_Cons]) 1); 
   30.29  qed"rev_red_not_nil";
   30.30 @@ -104,7 +104,7 @@
   30.31   by (asm_full_simp_tac list_ss 1);
   30.32   by (REPEAT (rtac allI 1)); 
   30.33   by (rtac impI 1); 
   30.34 - by (rtac (expand_if RS ssubst) 1);
   30.35 + by (stac expand_if 1);
   30.36   by (asm_full_simp_tac (list_ss addsimps [reverse_Cons,hd_append,
   30.37                            (rev_red_not_nil RS mp)])  1);
   30.38  qed"last_ind_on_first";
   30.39 @@ -116,7 +116,7 @@
   30.40     "if x=hd(reverse(reduce(l))) & reduce(l)~=[] then   \
   30.41  \      reduce(l@[x])=reduce(l) else                  \
   30.42  \      reduce(l@[x])=reduce(l)@[x]"; 
   30.43 -by (rtac (expand_if RS ssubst) 1);
   30.44 +by (stac expand_if 1);
   30.45  by (rtac conjI 1);
   30.46  (* --> *)
   30.47  by (List.list.induct_tac "l" 1);
   30.48 @@ -154,7 +154,7 @@
   30.49  by (Asm_full_simp_tac 1);
   30.50  by (REPEAT (etac exE 1));
   30.51  by (Asm_full_simp_tac 1);
   30.52 -by (rtac (expand_if RS ssubst) 1);
   30.53 +by (stac expand_if 1);
   30.54  by (rtac conjI 1);
   30.55  by (simp_tac (simpset() addsimps [and_de_morgan_and_absorbe]) 2);
   30.56  by (Step_tac 1);
    31.1 --- a/src/HOLCF/IOA/ABP/Lemmas.ML	Tue Dec 16 15:17:26 1997 +0100
    31.2 +++ b/src/HOLCF/IOA/ABP/Lemmas.ML	Tue Dec 16 17:58:03 1997 +0100
    31.3 @@ -8,7 +8,7 @@
    31.4  (* Logic *)
    31.5  
    31.6  val prems = goal HOL.thy "(P ==> Q-->R) ==> P&Q --> R";
    31.7 -  by(fast_tac (claset() addDs prems) 1);
    31.8 +  by (fast_tac (claset() addDs prems) 1);
    31.9  qed "imp_conj_lemma";
   31.10  
   31.11  goal HOL.thy "(~(A&B)) = ((~A)&B| ~B)";
   31.12 @@ -16,7 +16,7 @@
   31.13  val and_de_morgan_and_absorbe = result();
   31.14  
   31.15  goal HOL.thy "(if C then A else B) --> (A|B)";
   31.16 -by (rtac (expand_if RS ssubst) 1);
   31.17 +by (stac expand_if 1);
   31.18  by (Fast_tac 1);
   31.19  val bool_if_impl_or = result();
   31.20  
    32.1 --- a/src/HOLCF/IOA/ABP/ROOT.ML	Tue Dec 16 15:17:26 1997 +0100
    32.2 +++ b/src/HOLCF/IOA/ABP/ROOT.ML	Tue Dec 16 17:58:03 1997 +0100
    32.3 @@ -3,11 +3,8 @@
    32.4      Author:     Olaf Mueller
    32.5      Copyright   1995  TU Muenchen
    32.6  
    32.7 -This is the ROOT file for the Alternating Bit Protocol performed in I/O-Automata.
    32.8 -
    32.9 -For details see the README.html file.
   32.10 -
   32.11 -Should be executed in the subdirectory HOLCF/IOA/examples/ABP.
   32.12 +This is the ROOT file for the Alternating Bit Protocol performed in
   32.13 +I/O-Automata.
   32.14  *)
   32.15  
   32.16  goals_limit := 1;
    33.1 --- a/src/HOLCF/IOA/NTP/Abschannel.ML	Tue Dec 16 15:17:26 1997 +0100
    33.2 +++ b/src/HOLCF/IOA/NTP/Abschannel.ML	Tue Dec 16 17:58:03 1997 +0100
    33.3 @@ -25,7 +25,7 @@
    33.4       \ C_m_r ~: actions(srch_asig)           &    \
    33.5       \ C_r_s ~: actions(srch_asig)  & C_r_r(m) ~: actions(srch_asig)";
    33.6  
    33.7 -by(simp_tac (simpset() addsimps unfold_renaming) 1);
    33.8 +by (simp_tac (simpset() addsimps unfold_renaming) 1);
    33.9  qed"in_srch_asig";
   33.10  
   33.11  goal Abschannel.thy
   33.12 @@ -40,20 +40,20 @@
   33.13       \ C_r_s ~: actions(rsch_asig)            & \
   33.14       \ C_r_r(m) ~: actions(rsch_asig)";
   33.15  
   33.16 -by(simp_tac (simpset() addsimps unfold_renaming) 1);
   33.17 +by (simp_tac (simpset() addsimps unfold_renaming) 1);
   33.18  qed"in_rsch_asig";
   33.19  
   33.20  goal Abschannel.thy "srch_ioa = \
   33.21  \   (srch_asig, {{|}}, srch_trans,srch_wfair,srch_sfair)";
   33.22  by (simp_tac (simpset() addsimps [srch_asig_def,srch_trans_def, asig_of_def, trans_of_def,
   33.23                wfair_of_def, sfair_of_def,srch_wfair_def,srch_sfair_def]) 1);
   33.24 -by(simp_tac (simpset() addsimps unfold_renaming) 1);
   33.25 +by (simp_tac (simpset() addsimps unfold_renaming) 1);
   33.26  qed"srch_ioa_thm";
   33.27  
   33.28  goal Abschannel.thy "rsch_ioa = \
   33.29  \    (rsch_asig, {{|}}, rsch_trans,rsch_wfair,rsch_sfair)";
   33.30  by (simp_tac (simpset() addsimps [rsch_asig_def,rsch_trans_def, asig_of_def, trans_of_def,
   33.31                wfair_of_def, sfair_of_def,rsch_wfair_def,rsch_sfair_def]) 1);
   33.32 -by(simp_tac (simpset() addsimps unfold_renaming) 1);
   33.33 +by (simp_tac (simpset() addsimps unfold_renaming) 1);
   33.34  qed"rsch_ioa_thm";
   33.35  
    34.1 --- a/src/HOLCF/IOA/NTP/Impl.ML	Tue Dec 16 15:17:26 1997 +0100
    34.2 +++ b/src/HOLCF/IOA/NTP/Impl.ML	Tue Dec 16 17:58:03 1997 +0100
    34.3 @@ -33,7 +33,7 @@
    34.4  \  fst(snd(x)) = rec(x)       & \
    34.5  \  fst(snd(snd(x))) = srch(x) & \
    34.6  \  snd(snd(snd(x))) = rsch(x)";
    34.7 -by(simp_tac (simpset() addsimps
    34.8 +by (simp_tac (simpset() addsimps
    34.9               [sen_def,rec_def,srch_def,rsch_def]) 1);
   34.10  Addsimps [result()];
   34.11  
   34.12 @@ -41,8 +41,8 @@
   34.13  \            | a:actions(receiver_asig) \
   34.14  \            | a:actions(srch_asig)     \
   34.15  \            | a:actions(rsch_asig)";
   34.16 -  by(Action.action.induct_tac "a" 1);
   34.17 -  by(ALLGOALS (Simp_tac));
   34.18 +  by (Action.action.induct_tac "a" 1);
   34.19 +  by (ALLGOALS (Simp_tac));
   34.20  Addsimps [result()];
   34.21  
   34.22  Delsimps [split_paired_All];
   34.23 @@ -73,18 +73,18 @@
   34.24  
   34.25  goalw Impl.thy impl_ioas "invariant impl_ioa inv1";
   34.26  by (rtac invariantI 1);
   34.27 -by(asm_full_simp_tac (simpset()
   34.28 +by (asm_full_simp_tac (simpset()
   34.29     addsimps [inv1_def, hdr_sum_def, Sender.srcvd_def,
   34.30               Sender.ssent_def, Receiver.rsent_def,Receiver.rrcvd_def]) 1);
   34.31  
   34.32 -by(simp_tac (simpset() delsimps [trans_of_par4]
   34.33 +by (simp_tac (simpset() delsimps [trans_of_par4]
   34.34                  addsimps [fork_lemma,inv1_def]) 1);
   34.35  
   34.36  (* Split proof in two *)
   34.37  by (rtac conjI 1); 
   34.38  
   34.39  (* First half *)
   34.40 -by(asm_full_simp_tac (simpset() addsimps [Impl.inv1_def]) 1);
   34.41 +by (asm_full_simp_tac (simpset() addsimps [Impl.inv1_def]) 1);
   34.42  by (rtac Action.action.induct 1);
   34.43  
   34.44  by (EVERY1[tac, tac, tac, tac]);
   34.45 @@ -97,13 +97,13 @@
   34.46  by (tac_ren 1);
   34.47  
   34.48  (* 4 + 1 *)
   34.49 -by(EVERY1[tac, tac, tac, tac]);
   34.50 +by (EVERY1[tac, tac, tac, tac]);
   34.51  
   34.52  
   34.53  (* Now the other half *)
   34.54 -by(asm_full_simp_tac (simpset() addsimps [Impl.inv1_def]) 1);
   34.55 +by (asm_full_simp_tac (simpset() addsimps [Impl.inv1_def]) 1);
   34.56  by (rtac Action.action.induct 1);
   34.57 -by(EVERY1[tac, tac]);
   34.58 +by (EVERY1[tac, tac]);
   34.59  
   34.60  (* detour 1 *)
   34.61  by (tac 1);
   34.62 @@ -171,7 +171,7 @@
   34.63    (* 10 - 7 *)
   34.64    by (EVERY1[tac2,tac2,tac2,tac2]);
   34.65    (* 6 *)
   34.66 -  by(forward_tac [rewrite_rule [Impl.inv1_def]
   34.67 +  by (forward_tac [rewrite_rule [Impl.inv1_def]
   34.68                                 (inv1 RS invariantE) RS conjunct1] 1);
   34.69    (* 6 - 5 *)
   34.70    by (EVERY1[tac2,tac2]);
   34.71 @@ -191,7 +191,7 @@
   34.72  
   34.73    (* 2 *)
   34.74    by (tac2 1);
   34.75 -  by(forward_tac [rewrite_rule [Impl.inv1_def]
   34.76 +  by (forward_tac [rewrite_rule [Impl.inv1_def]
   34.77                                 (inv1 RS invariantE) RS conjunct1] 1);
   34.78    by (rtac impI 1);
   34.79    by (rtac impI 1);
   34.80 @@ -201,7 +201,7 @@
   34.81  
   34.82    (* 1 *)
   34.83    by (tac2 1);
   34.84 -  by(forward_tac [rewrite_rule [Impl.inv1_def]
   34.85 +  by (forward_tac [rewrite_rule [Impl.inv1_def]
   34.86                                 (inv1 RS invariantE) RS conjunct2] 1);
   34.87    by (rtac impI 1);
   34.88    by (rtac impI 1);
   34.89 @@ -310,7 +310,7 @@
   34.90   (* 2 b *)
   34.91   
   34.92    by (strip_tac  1 THEN REPEAT (etac conjE 1));
   34.93 -  by(forward_tac [rewrite_rule [Impl.inv2_def]
   34.94 +  by (forward_tac [rewrite_rule [Impl.inv2_def]
   34.95                                 (inv2 RS invariantE)] 1);
   34.96    by (tac4 1);
   34.97    by (Asm_full_simp_tac 1);
   34.98 @@ -319,9 +319,9 @@
   34.99    by (tac4 1);
  34.100    by (strip_tac  1 THEN REPEAT (etac conjE 1));
  34.101    by (rtac ccontr 1);
  34.102 -  by(forward_tac [rewrite_rule [Impl.inv2_def]
  34.103 +  by (forward_tac [rewrite_rule [Impl.inv2_def]
  34.104                                 (inv2 RS invariantE)] 1);
  34.105 -  by(forward_tac [rewrite_rule [Impl.inv3_def]
  34.106 +  by (forward_tac [rewrite_rule [Impl.inv3_def]
  34.107                                 (inv3 RS invariantE)] 1);
  34.108    by (Asm_full_simp_tac 1);
  34.109    by (eres_inst_tac [("x","m")] allE 1);
    35.1 --- a/src/HOLCF/IOA/NTP/Lemmas.ML	Tue Dec 16 15:17:26 1997 +0100
    35.2 +++ b/src/HOLCF/IOA/NTP/Lemmas.ML	Tue Dec 16 17:58:03 1997 +0100
    35.3 @@ -7,7 +7,7 @@
    35.4  
    35.5  (* Logic *)
    35.6  val prems = goal HOL.thy "(P ==> Q-->R) ==> P&Q --> R";
    35.7 -  by(fast_tac (claset() addDs prems) 1);
    35.8 +  by (fast_tac (claset() addDs prems) 1);
    35.9  qed "imp_conj_lemma";
   35.10  
   35.11  goal HOL.thy "(A --> B & C) = ((A --> B) & (A --> C))";
   35.12 @@ -35,8 +35,8 @@
   35.13  (* Arithmetic *)
   35.14  
   35.15  goal Arith.thy "!!x. 0<x ==> (x-1 = y) = (x = Suc(y))";
   35.16 -by(asm_simp_tac (simpset() addsimps [diff_Suc] addsplits [expand_nat_case]) 1);
   35.17 -by(Blast_tac 1);
   35.18 +by (asm_simp_tac (simpset() addsimps [diff_Suc] addsplits [expand_nat_case]) 1);
   35.19 +by (Blast_tac 1);
   35.20  qed "pred_suc";
   35.21  
   35.22  
    36.1 --- a/src/HOLCF/IOA/NTP/Multiset.ML	Tue Dec 16 15:17:26 1997 +0100
    36.2 +++ b/src/HOLCF/IOA/NTP/Multiset.ML	Tue Dec 16 17:58:03 1997 +0100
    36.3 @@ -34,7 +34,7 @@
    36.4                           addsimps [Multiset.delm_nonempty_def,
    36.5                                     Multiset.countm_nonempty_def]
    36.6                           setloop (split_tac [expand_if])) 1);
    36.7 -  by (safe_tac (claset()));
    36.8 +  by Safe_tac;
    36.9    by (Asm_full_simp_tac 1);
   36.10  qed "count_delm_simp";
   36.11  
    37.1 --- a/src/HOLCF/IOA/NTP/ROOT.ML	Tue Dec 16 15:17:26 1997 +0100
    37.2 +++ b/src/HOLCF/IOA/NTP/ROOT.ML	Tue Dec 16 17:58:03 1997 +0100
    37.3 @@ -5,10 +5,6 @@
    37.4  
    37.5  This is the ROOT file for a network transmission protocol (NTP subdirectory),
    37.6  performed in the I/O automata formalization by Olaf Mueller. 
    37.7 -
    37.8 -For details see the README.html file.
    37.9 -
   37.10 -Should be executed in the subdirectory HOLCF/IOA/examples/NTP.
   37.11  *)
   37.12  
   37.13  goals_limit := 1;
    38.1 --- a/src/HOLCF/IOA/NTP/Receiver.ML	Tue Dec 16 15:17:26 1997 +0100
    38.2 +++ b/src/HOLCF/IOA/NTP/Receiver.ML	Tue Dec 16 17:58:03 1997 +0100
    38.3 @@ -15,7 +15,7 @@
    38.4  \ C_m_r : actions(receiver_asig)          &   \
    38.5  \ C_r_s ~: actions(receiver_asig)         &   \
    38.6  \ C_r_r(m) : actions(receiver_asig)";
    38.7 -  by(simp_tac (simpset() addsimps (Receiver.receiver_asig_def :: actions_def :: 
    38.8 +  by (simp_tac (simpset() addsimps (Receiver.receiver_asig_def :: actions_def :: 
    38.9                                    asig_projections)) 1);
   38.10  qed "in_receiver_asig";
   38.11  
    39.1 --- a/src/HOLCF/IOA/NTP/Sender.ML	Tue Dec 16 15:17:26 1997 +0100
    39.2 +++ b/src/HOLCF/IOA/NTP/Sender.ML	Tue Dec 16 17:58:03 1997 +0100
    39.3 @@ -15,7 +15,7 @@
    39.4  \ C_m_r ~: actions(sender_asig)         &   \
    39.5  \ C_r_s : actions(sender_asig)          &   \
    39.6  \ C_r_r(m) ~: actions(sender_asig)";
    39.7 -by(simp_tac (simpset() addsimps 
    39.8 +by (simp_tac (simpset() addsimps 
    39.9               (Sender.sender_asig_def :: actions_def :: 
   39.10                asig_projections)) 1);
   39.11  qed "in_sender_asig";
    40.1 --- a/src/HOLCF/IOA/meta_theory/Automata.ML	Tue Dec 16 15:17:26 1997 +0100
    40.2 +++ b/src/HOLCF/IOA/meta_theory/Automata.ML	Tue Dec 16 17:58:03 1997 +0100
    40.3 @@ -50,7 +50,7 @@
    40.4  \                  (snd(s),a,snd(t)):trans_of(B)     \                
    40.5  \                else snd(t) = snd(s))}";
    40.6  
    40.7 -by(simp_tac (simpset() addsimps (par_def::ioa_projections)) 1);
    40.8 +by (simp_tac (simpset() addsimps (par_def::ioa_projections)) 1);
    40.9  qed "trans_of_par";
   40.10  
   40.11  
   40.12 @@ -179,15 +179,15 @@
   40.13  (* a:act B *)
   40.14  by (eres_inst_tac [("x","a")] allE 1);
   40.15  by (Asm_full_simp_tac 1);
   40.16 -bd inpAAactB_is_inpBoroutB 1;
   40.17 -ba 1;
   40.18 -ba 1;
   40.19 +by (dtac inpAAactB_is_inpBoroutB 1);
   40.20 +by (assume_tac 1);
   40.21 +by (assume_tac 1);
   40.22  by (eres_inst_tac [("x","a")] allE 1);
   40.23  by (Asm_full_simp_tac 1);
   40.24  by (eres_inst_tac [("x","aa")] allE 1);
   40.25  by (eres_inst_tac [("x","b")] allE 1);
   40.26 -be exE 1;
   40.27 -be exE 1;
   40.28 +by (etac exE 1);
   40.29 +by (etac exE 1);
   40.30  by (res_inst_tac [("x","(s2,s2a)")] exI 1);
   40.31  by (asm_full_simp_tac (simpset() addsimps [inp_is_act]) 1);
   40.32  (* a~: act B*)
   40.33 @@ -195,7 +195,7 @@
   40.34  by (eres_inst_tac [("x","a")] allE 1);
   40.35  by (Asm_full_simp_tac 1);
   40.36  by (eres_inst_tac [("x","aa")] allE 1);
   40.37 -be exE 1;
   40.38 +by (etac exE 1);
   40.39  by (res_inst_tac [("x","(s2,b)")] exI 1);
   40.40  by (Asm_full_simp_tac 1);
   40.41  
   40.42 @@ -206,17 +206,17 @@
   40.43  by (eres_inst_tac [("x","a")] allE 1);
   40.44  by (asm_full_simp_tac (simpset() addsimps [inp_is_act]) 1);
   40.45  by (forw_inst_tac [("A2","A")] (compat_commute RS iffD1) 1);
   40.46 -bd inpAAactB_is_inpBoroutB 1;
   40.47 +by (dtac inpAAactB_is_inpBoroutB 1);
   40.48  back();
   40.49 -ba 1;
   40.50 -ba 1;
   40.51 +by (assume_tac 1);
   40.52 +by (assume_tac 1);
   40.53  by (Asm_full_simp_tac 1);
   40.54  by (rotate_tac ~1 1);
   40.55  by (Asm_full_simp_tac 1);
   40.56  by (eres_inst_tac [("x","aa")] allE 1);
   40.57  by (eres_inst_tac [("x","b")] allE 1);
   40.58 -be exE 1;
   40.59 -be exE 1;
   40.60 +by (etac exE 1);
   40.61 +by (etac exE 1);
   40.62  by (res_inst_tac [("x","(s2,s2a)")] exI 1);
   40.63  by (asm_full_simp_tac (simpset() addsimps [inp_is_act]) 1);
   40.64  (* a~: act B*)
   40.65 @@ -226,7 +226,7 @@
   40.66  by (eres_inst_tac [("x","a")] allE 1);
   40.67  by (Asm_full_simp_tac 1);
   40.68  by (eres_inst_tac [("x","b")] allE 1);
   40.69 -be exE 1;
   40.70 +by (etac exE 1);
   40.71  by (res_inst_tac [("x","(aa,s2)")] exI 1);
   40.72  by (Asm_full_simp_tac 1);
   40.73  qed"input_enabled_par";
   40.74 @@ -289,7 +289,7 @@
   40.75  by (simp_tac (simpset() addsimps [actions_def,asig_internals_def,
   40.76          asig_outputs_def,asig_inputs_def,externals_def,asig_of_def,restrict_def,
   40.77          restrict_asig_def]) 1);
   40.78 -auto();
   40.79 +by (Auto_tac());
   40.80  qed"acts_restrict";
   40.81  
   40.82  goal thy "starts_of(restrict ioa acts) = starts_of(ioa) &     \
   40.83 @@ -417,7 +417,7 @@
   40.84  by (asm_full_simp_tac (simpset() addsimps [actions_def,trans_of_def,
   40.85      asig_internals_def,asig_outputs_def,asig_inputs_def,externals_def,
   40.86     asig_of_def,rename_def,rename_set_def]) 1);
   40.87 -auto();
   40.88 +by (Auto_tac());
   40.89  qed"is_trans_of_rename";
   40.90  
   40.91  goal thy "!! A. [| is_asig_of A; is_asig_of B; compatible A B|]  \
   40.92 @@ -426,7 +426,7 @@
   40.93         asig_comp_def,compatible_def,asig_internals_def,asig_outputs_def,
   40.94       asig_inputs_def,actions_def,is_asig_def]) 1);
   40.95  by (asm_full_simp_tac (simpset() addsimps [asig_of_def]) 1);
   40.96 -auto();
   40.97 +by (Auto_tac());
   40.98  by (REPEAT (best_tac (set_cs addEs [equalityCE]) 1));
   40.99  qed"is_asig_of_par";
  40.100  
  40.101 @@ -434,7 +434,7 @@
  40.102             asig_internals_def,asig_outputs_def,asig_inputs_def,externals_def,o_def] 
  40.103  "!! A. is_asig_of A ==> is_asig_of (restrict A f)";
  40.104  by (Asm_full_simp_tac 1);
  40.105 -auto();
  40.106 +by (Auto_tac());
  40.107  by (REPEAT (best_tac (set_cs addEs [equalityCE]) 1));
  40.108  qed"is_asig_of_restrict";
  40.109  
  40.110 @@ -442,7 +442,7 @@
  40.111  by (asm_full_simp_tac (simpset() addsimps [is_asig_of_def,
  40.112       rename_def,rename_set_def,asig_internals_def,asig_outputs_def,
  40.113       asig_inputs_def,actions_def,is_asig_def,asig_of_def]) 1);
  40.114 -auto(); 
  40.115 +by (Auto_tac()); 
  40.116  by (dres_inst_tac [("s","Some xb")] sym 1);
  40.117  by (rotate_tac ~1 1);
  40.118  by (Asm_full_simp_tac 1);
  40.119 @@ -466,7 +466,7 @@
  40.120  "!! A. [|compatible A B; compatible A C |]==> compatible A (B||C)";
  40.121  by (asm_full_simp_tac (simpset() addsimps [internals_of_par, 
  40.122     outputs_of_par,actions_of_par]) 1);
  40.123 -auto();
  40.124 +by (Auto_tac());
  40.125  by (REPEAT (best_tac (set_cs addEs [equalityCE]) 1));
  40.126  qed"compatible_par";
  40.127  
  40.128 @@ -475,7 +475,7 @@
  40.129  "!! A. [|compatible A C; compatible B C |]==> compatible (A||B) C";
  40.130  by (asm_full_simp_tac (simpset() addsimps [internals_of_par, 
  40.131     outputs_of_par,actions_of_par]) 1);
  40.132 -auto();
  40.133 +by (Auto_tac());
  40.134  by (REPEAT (best_tac (set_cs addEs [equalityCE]) 1));
  40.135  qed"compatible_par2";
  40.136  
    41.1 --- a/src/HOLCF/IOA/meta_theory/CompoExecs.ML	Tue Dec 16 15:17:26 1997 +0100
    41.2 +++ b/src/HOLCF/IOA/meta_theory/CompoExecs.ML	Tue Dec 16 17:58:03 1997 +0100
    41.3 @@ -108,7 +108,7 @@
    41.4  goal thy "(stutter2 sig`(at>>xs)) s = \
    41.5  \              ((if (fst at)~:actions sig then Def (s=snd at) else TT) \
    41.6  \                andalso (stutter2 sig`xs) (snd at))"; 
    41.7 -br trans 1;
    41.8 +by (rtac trans 1);
    41.9  by (stac stutter2_unfold 1);
   41.10  by (asm_full_simp_tac (simpset() addsimps [Cons_def,flift1_def,If_and_if]) 1);
   41.11  by (Simp_tac 1);
   41.12 @@ -268,7 +268,7 @@
   41.13  "Execs (A||B) = par_execs (Execs A) (Execs B)";
   41.14  
   41.15  by (asm_full_simp_tac (simpset() addsimps [asig_of_par]) 1);
   41.16 -br set_ext 1;
   41.17 +by (rtac set_ext 1);
   41.18  by (asm_full_simp_tac (simpset() addsimps [compositionality_ex,actions_of_par]) 1);
   41.19  qed"compositionality_ex_modules";
   41.20  
    42.1 --- a/src/HOLCF/IOA/meta_theory/CompoScheds.ML	Tue Dec 16 15:17:26 1997 +0100
    42.2 +++ b/src/HOLCF/IOA/meta_theory/CompoScheds.ML	Tue Dec 16 17:58:03 1997 +0100
    42.3 @@ -517,7 +517,7 @@
    42.4  "Scheds (A||B) = par_scheds (Scheds A) (Scheds B)";
    42.5  
    42.6  by (asm_full_simp_tac (simpset() addsimps [asig_of_par]) 1);
    42.7 -br set_ext 1;
    42.8 +by (rtac set_ext 1);
    42.9  by (asm_full_simp_tac (simpset() addsimps [compositionality_sch,actions_of_par]) 1);
   42.10  qed"compositionality_sch_modules";
   42.11  
    43.1 --- a/src/HOLCF/IOA/meta_theory/CompoTraces.ML	Tue Dec 16 15:17:26 1997 +0100
    43.2 +++ b/src/HOLCF/IOA/meta_theory/CompoTraces.ML	Tue Dec 16 17:58:03 1997 +0100
    43.3 @@ -1239,7 +1239,7 @@
    43.4  \==> Traces (A||B) = par_traces (Traces A) (Traces B)";
    43.5  
    43.6  by (asm_full_simp_tac (simpset() addsimps [asig_of_par]) 1);
    43.7 -br set_ext 1;
    43.8 +by (rtac set_ext 1);
    43.9  by (asm_full_simp_tac (simpset() addsimps [compositionality_tr,externals_of_par]) 1);
   43.10  qed"compositionality_tr_modules";
   43.11  
    44.1 --- a/src/HOLCF/IOA/meta_theory/RefMappings.ML	Tue Dec 16 15:17:26 1997 +0100
    44.2 +++ b/src/HOLCF/IOA/meta_theory/RefMappings.ML	Tue Dec 16 17:58:03 1997 +0100
    44.3 @@ -92,7 +92,7 @@
    44.4  
    44.5  
    44.6  val prems = goal HOL.thy "(P ==> Q-->R) ==> P&Q --> R";
    44.7 -  by(fast_tac (claset() addDs prems) 1);
    44.8 +  by (fast_tac (claset() addDs prems) 1);
    44.9  val lemma = result();
   44.10  
   44.11  
   44.12 @@ -108,7 +108,7 @@
   44.13  by (simp_tac (simpset() addsimps [rename_def,rename_set_def]) 1);
   44.14  by (asm_full_simp_tac (simpset() addsimps [externals_def,asig_inputs_def,
   44.15  asig_outputs_def,asig_of_def,trans_of_def]) 1);
   44.16 -by (safe_tac (claset()));
   44.17 +by Safe_tac;
   44.18  by (stac expand_if 1);
   44.19   by (rtac conjI 1);
   44.20   by (rtac impI 1);
    45.1 --- a/src/HOLCF/IOA/meta_theory/Traces.ML	Tue Dec 16 15:17:26 1997 +0100
    45.2 +++ b/src/HOLCF/IOA/meta_theory/Traces.ML	Tue Dec 16 17:58:03 1997 +0100
    45.3 @@ -197,7 +197,7 @@
    45.4    "!! A.[| x:traces A |] ==> \
    45.5  \   Forall (%a. a:act A) x";
    45.6   by (safe_tac set_cs );
    45.7 -br ForallQFilterP 1;
    45.8 +by (rtac ForallQFilterP 1);
    45.9  by (fast_tac (!claset addSIs [ext_is_act]) 1);
   45.10  qed"traces_in_sig";
   45.11  *)
    46.1 --- a/src/HOLCF/Porder0.ML	Tue Dec 16 15:17:26 1997 +0100
    46.2 +++ b/src/HOLCF/Porder0.ML	Tue Dec 16 17:58:03 1997 +0100
    46.3 @@ -48,5 +48,5 @@
    46.4          ]);
    46.5  
    46.6  goal Porder0.thy "((x::'a::po)=y) = (x << y & y << x)";
    46.7 -by(fast_tac (HOL_cs addSEs [antisym_less_inverse] addSIs [antisym_less]) 1);
    46.8 +by (fast_tac (HOL_cs addSEs [antisym_less_inverse] addSIs [antisym_less]) 1);
    46.9  qed "po_eq_conv";
    47.1 --- a/src/HOLCF/Tr.ML	Tue Dec 16 15:17:26 1997 +0100
    47.2 +++ b/src/HOLCF/Tr.ML	Tue Dec 16 17:58:03 1997 +0100
    47.3 @@ -115,17 +115,17 @@
    47.4  "!!t.[|t~=UU|]==> ((t andalso s)=FF)=(t=FF | s=FF)";
    47.5  by (rtac iffI 1);
    47.6  by (res_inst_tac [("p","t")] trE 1);
    47.7 -auto();
    47.8 +by (Auto_tac());
    47.9  by (res_inst_tac [("p","t")] trE 1);
   47.10 -auto();
   47.11 +by (Auto_tac());
   47.12  qed"andalso_or";
   47.13  
   47.14  goal thy "!!t.[|t~=UU|]==> ((t andalso s)~=FF)=(t~=FF & s~=FF)";
   47.15  by (rtac iffI 1);
   47.16  by (res_inst_tac [("p","t")] trE 1);
   47.17 -auto();
   47.18 +by (Auto_tac());
   47.19  by (res_inst_tac [("p","t")] trE 1);
   47.20 -auto();
   47.21 +by (Auto_tac());
   47.22  qed"andalso_and";
   47.23  
   47.24  goal thy "(Def x ~=FF)= x";
    48.1 --- a/src/HOLCF/ex/Dnat.ML	Tue Dec 16 15:17:26 1997 +0100
    48.2 +++ b/src/HOLCF/ex/Dnat.ML	Tue Dec 16 17:58:03 1997 +0100
    48.3 @@ -22,14 +22,14 @@
    48.4  qed_goal "iterator1" Dnat.thy "iterator`UU`f`x = UU"
    48.5   (fn prems =>
    48.6  	[
    48.7 -	(rtac (iterator_def2 RS ssubst) 1),
    48.8 +	(stac iterator_def2 1),
    48.9  	(simp_tac (HOLCF_ss addsimps dnat.rews) 1)
   48.10  	]);
   48.11  
   48.12  qed_goal "iterator2" Dnat.thy "iterator`dzero`f`x = x"
   48.13   (fn prems =>
   48.14  	[
   48.15 -	(rtac (iterator_def2 RS ssubst) 1),
   48.16 +	(stac iterator_def2 1),
   48.17  	(simp_tac (HOLCF_ss addsimps dnat.rews) 1)
   48.18  	]);
   48.19  
   48.20 @@ -39,7 +39,7 @@
   48.21  	[
   48.22  	(cut_facts_tac prems 1),
   48.23  	(rtac trans 1),
   48.24 -	(rtac (iterator_def2 RS ssubst) 1),
   48.25 +	(stac iterator_def2 1),
   48.26  	(asm_simp_tac (HOLCF_ss addsimps dnat.rews) 1),
   48.27  	(rtac refl 1)
   48.28  	]);
    49.1 --- a/src/LCF/ex/ex.ML	Tue Dec 16 15:17:26 1997 +0100
    49.2 +++ b/src/LCF/ex/ex.ML	Tue Dec 16 17:58:03 1997 +0100
    49.3 @@ -40,12 +40,12 @@
    49.4  val ex_ss = ex_ss addsimps [H_strict];
    49.5  
    49.6  goal ex_thy "ALL x. H(FIX(K,x)) = FIX(K,x)";
    49.7 -by(induct_tac "K" 1);
    49.8 -by(simp_tac ex_ss 1);
    49.9 -by(simp_tac (ex_ss setloop (split_tac [COND_cases_iff])) 1);
   49.10 -by(strip_tac 1);
   49.11 -by(stac H_unfold 1);
   49.12 -by(asm_simp_tac ex_ss 1);
   49.13 +by (induct_tac "K" 1);
   49.14 +by (simp_tac ex_ss 1);
   49.15 +by (simp_tac (ex_ss setloop (split_tac [COND_cases_iff])) 1);
   49.16 +by (strip_tac 1);
   49.17 +by (stac H_unfold 1);
   49.18 +by (asm_simp_tac ex_ss 1);
   49.19  val H_idemp_lemma = topthm();
   49.20  
   49.21  val H_idemp = rewrite_rule [mk_meta_eq (H RS sym)] H_idemp_lemma;
   49.22 @@ -76,10 +76,10 @@
   49.23  val ex_ss = LCF_ss addsimps [F_strict,K];
   49.24  
   49.25  goal ex_thy "ALL x. F(H(x::'a,y::'b)) = H(x,F(y))";
   49.26 -by(stac H 1);
   49.27 -by(induct_tac "K::('a=>'b=>'b)=>('a=>'b=>'b)" 1);
   49.28 -by(simp_tac ex_ss 1);
   49.29 -by(asm_simp_tac (ex_ss setloop (split_tac [COND_cases_iff])) 1);
   49.30 +by (stac H 1);
   49.31 +by (induct_tac "K::('a=>'b=>'b)=>('a=>'b=>'b)" 1);
   49.32 +by (simp_tac ex_ss 1);
   49.33 +by (asm_simp_tac (ex_ss setloop (split_tac [COND_cases_iff])) 1);
   49.34  result();
   49.35  
   49.36  
   49.37 @@ -103,20 +103,20 @@
   49.38  val ex_ss = LCF_ss addsimps [p_strict,p_s];
   49.39  
   49.40  goal ex_thy "p(FIX(s),y) = FIX(s)";
   49.41 -by(induct_tac "s" 1);
   49.42 -by(simp_tac ex_ss 1);
   49.43 -by(simp_tac ex_ss 1);
   49.44 +by (induct_tac "s" 1);
   49.45 +by (simp_tac ex_ss 1);
   49.46 +by (simp_tac ex_ss 1);
   49.47  result();
   49.48  
   49.49  
   49.50  (*** Prefixpoints ***)
   49.51  
   49.52  val asms = goal thy "[| f(p) << p; !!q. f(q) << q ==> p << q |] ==> FIX(f)=p";
   49.53 -by(rewtac eq_def);
   49.54 +by (rewtac eq_def);
   49.55  by (rtac conjI 1);
   49.56 -by(induct_tac "f" 1);
   49.57 +by (induct_tac "f" 1);
   49.58  by (rtac minimal 1);
   49.59 -by(strip_tac 1);
   49.60 +by (strip_tac 1);
   49.61  by (rtac less_trans 1);
   49.62  by (resolve_tac asms 2);
   49.63  by (etac less_ap_term 1);