--- a/src/CCL/CCL.ML Tue Dec 16 15:17:26 1997 +0100
+++ b/src/CCL/CCL.ML Tue Dec 16 17:58:03 1997 +0100
@@ -166,8 +166,8 @@
\ (EX a a' b b'. t=<a,b> & t'=<a',b'> & a [= a' & b [= b') | \
\ (EX f f'. t=lam x. f(x) & t'=lam x. f'(x) & (ALL x. f(x) [= f'(x)))";
by (simp_tac (ccl_ss addsimps [PO_iff] delsimps ex_simps) 1);
-br (rewrite_rule [POgen_def,SIM_def]
- (POgen_mono RS (PO_def RS def_gfp_Tarski) RS XHlemma1)) 1;
+by (rtac (rewrite_rule [POgen_def,SIM_def]
+ (POgen_mono RS (PO_def RS def_gfp_Tarski) RS XHlemma1)) 1);
by (rtac (iff_refl RS XHlemma2) 1);
qed "poXH";
@@ -292,8 +292,8 @@
\ (EX f f'. t=lam x. f(x) & t'=lam x. f'(x) & (ALL x. <f(x),f'(x)> : EQ))" 1);
by (etac rev_mp 1);
by (simp_tac (CCL_ss addsimps [EQ_iff RS iff_sym]) 1);
-br (rewrite_rule [EQgen_def,SIM_def]
- (EQgen_mono RS (EQ_def RS def_gfp_Tarski) RS XHlemma1)) 1;
+by (rtac (rewrite_rule [EQgen_def,SIM_def]
+ (EQgen_mono RS (EQ_def RS def_gfp_Tarski) RS XHlemma1)) 1);
by (rtac (iff_refl RS XHlemma2) 1);
qed "eqXH";
--- a/src/CCL/Hered.ML Tue Dec 16 15:17:26 1997 +0100
+++ b/src/CCL/Hered.ML Tue Dec 16 17:58:03 1997 +0100
@@ -26,8 +26,8 @@
goal Hered.thy
"t : HTT <-> t=true | t=false | (EX a b. t=<a,b> & a : HTT & b : HTT) | \
\ (EX f. t=lam x. f(x) & (ALL x. f(x) : HTT))";
-br (rewrite_rule [HTTgen_def]
- (HTTgen_mono RS (HTT_def RS def_gfp_Tarski) RS XHlemma1)) 1;
+by (rtac (rewrite_rule [HTTgen_def]
+ (HTTgen_mono RS (HTT_def RS def_gfp_Tarski) RS XHlemma1)) 1);
by (fast_tac set_cs 1);
qed "HTTXH";
--- a/src/FOL/ex/Nat2.ML Tue Dec 16 15:17:26 1997 +0100
+++ b/src/FOL/ex/Nat2.ML Tue Dec 16 17:58:03 1997 +0100
@@ -134,7 +134,7 @@
by (Simp_tac 1);
by (resolve_tac [impI RS allI] 1);
by (ALL_IND_TAC nat_exh Simp_tac 1);
-by (resolve_tac [impI] 1);
+by (rtac impI 1);
by (ALL_IND_TAC nat_exh Simp_tac 1);
by (Fast_tac 1);
qed "le_trans";
--- a/src/HOL/Arith.ML Tue Dec 16 15:17:26 1997 +0100
+++ b/src/HOL/Arith.ML Tue Dec 16 17:58:03 1997 +0100
@@ -29,13 +29,13 @@
However, none of the generalizations are currently in the simpset,
and I dread to think what happens if I put them in *)
goal Arith.thy "!!n. 0 < n ==> Suc(n-1) = n";
-by(asm_simp_tac (simpset() addsplits [expand_nat_case]) 1);
+by (asm_simp_tac (simpset() addsplits [expand_nat_case]) 1);
qed "Suc_pred";
Addsimps [Suc_pred];
(* Generalize? *)
goal Arith.thy "!!n. 0<n ==> n-1 < n";
-by(asm_simp_tac (simpset() addsplits [expand_nat_case]) 1);
+by (asm_simp_tac (simpset() addsplits [expand_nat_case]) 1);
qed "pred_less";
Addsimps [pred_less];
@@ -105,7 +105,7 @@
AddIffs [add_is_0];
goal Arith.thy "(0<m+n) = (0<m | 0<n)";
-by(simp_tac (simpset() delsimps [neq0_conv] addsimps [neq0_conv RS sym]) 1);
+by (simp_tac (simpset() delsimps [neq0_conv] addsimps [neq0_conv RS sym]) 1);
qed "add_gr_0";
AddIffs [add_gr_0];
@@ -377,7 +377,7 @@
could be got rid of if diff_diff_left were in the simpset...
*)
goal Arith.thy "(Suc m - n)-1 = m - n";
-by(simp_tac (simpset() addsimps [diff_diff_left]) 1);
+by (simp_tac (simpset() addsimps [diff_diff_left]) 1);
qed "pred_Suc_diff";
Addsimps [pred_Suc_diff];
@@ -554,13 +554,13 @@
Addsimps [mult_less_cancel1, mult_less_cancel2];
goal Arith.thy "(Suc k * m < Suc k * n) = (m < n)";
-br mult_less_cancel1 1;
+by (rtac mult_less_cancel1 1);
by (Simp_tac 1);
qed "Suc_mult_less_cancel1";
goalw Arith.thy [le_def] "(Suc k * m <= Suc k * n) = (m <= n)";
by (simp_tac (simpset_of HOL.thy) 1);
-br Suc_mult_less_cancel1 1;
+by (rtac Suc_mult_less_cancel1 1);
qed "Suc_mult_le_cancel1";
goal Arith.thy "!!k. 0<k ==> (m*k = n*k) = (m=n)";
@@ -578,7 +578,7 @@
Addsimps [mult_cancel1, mult_cancel2];
goal Arith.thy "(Suc k * m = Suc k * n) = (m = n)";
-br mult_cancel1 1;
+by (rtac mult_cancel1 1);
by (Simp_tac 1);
qed "Suc_mult_cancel1";
--- a/src/HOL/Auth/Shared.ML Tue Dec 16 15:17:26 1997 +0100
+++ b/src/HOL/Auth/Shared.ML Tue Dec 16 17:58:03 1997 +0100
@@ -75,7 +75,7 @@
AddIffs [shrK_in_initState];
goal thy "Key (shrK A) : used evs";
-br initState_into_used 1;
+by (rtac initState_into_used 1);
by (Blast_tac 1);
qed "shrK_in_used";
AddIffs [shrK_in_used];
--- a/src/HOL/Auth/TLS.ML Tue Dec 16 15:17:26 1997 +0100
+++ b/src/HOL/Auth/TLS.ML Tue Dec 16 17:58:03 1997 +0100
@@ -35,13 +35,13 @@
(*** clientK and serverK make symmetric keys; no clashes with pubK or priK ***)
goal thy "pubK A ~= sessionK arg";
-br notI 1;
+by (rtac notI 1);
by (dres_inst_tac [("f","isSymKey")] arg_cong 1);
by (Full_simp_tac 1);
qed "pubK_neq_sessionK";
goal thy "priK A ~= sessionK arg";
-br notI 1;
+by (rtac notI 1);
by (dres_inst_tac [("f","isSymKey")] arg_cong 1);
by (Full_simp_tac 1);
qed "priK_neq_sessionK";
@@ -274,7 +274,7 @@
\ : parts (spies evs); \
\ evs : tls; A ~: bad |] \
\ ==> Notes A {|Agent B, Nonce PMS|} : set evs";
-be rev_mp 1;
+by (etac rev_mp 1);
by (parts_induct_tac 1);
by (Fake_parts_insert_tac 1);
val lemma = result();
--- a/src/HOL/Divides.ML Tue Dec 16 15:17:26 1997 +0100
+++ b/src/HOL/Divides.ML Tue Dec 16 17:58:03 1997 +0100
@@ -110,7 +110,7 @@
(* a simple rearrangement of mod_div_equality: *)
goal thy "!!k. 0<k ==> k*(m div k) = m - (m mod k)";
-by(dres_inst_tac [("m","m")] mod_div_equality 1);
+by (dres_inst_tac [("m","m")] mod_div_equality 1);
by (EVERY1[etac subst, simp_tac (simpset() addsimps mult_ac),
K(IF_UNSOLVED no_tac)]);
qed "mult_div_cancel";
--- a/src/HOL/Finite.ML Tue Dec 16 15:17:26 1997 +0100
+++ b/src/HOL/Finite.ML Tue Dec 16 17:58:03 1997 +0100
@@ -65,7 +65,7 @@
val lemma = result();
goal Finite.thy "!!A. [| A<=B; finite B |] ==> finite A";
-bd lemma 1;
+by (dtac lemma 1);
by (Blast_tac 1);
qed "finite_subset";
--- a/src/HOL/Integ/Group.ML Tue Dec 16 15:17:26 1997 +0100
+++ b/src/HOL/Integ/Group.ML Tue Dec 16 17:58:03 1997 +0100
@@ -103,13 +103,13 @@
but are still very useful. They also demonstrate mk_group1_tac.
*)
goal Group.thy "x-x = (zero::'a::add_group)";
-by(mk_group1_tac 1);
-by(group1_tac 1);
+by (mk_group1_tac 1);
+by (group1_tac 1);
qed "minus_self_zero";
goal Group.thy "x-zero = (x::'a::add_group)";
-by(mk_group1_tac 1);
-by(group1_tac 1);
+by (mk_group1_tac 1);
+by (group1_tac 1);
qed "minus_zero";
(*** Abelian Groups ***)
@@ -144,33 +144,33 @@
(x-y = z) = (x = z+y) and (x = y-z) = (x+z = y)
*)
goal Group.thy "x + (y - z) = (x + y) - (z::'a::add_group)";
-by(mk_group1_tac 1);
-by(group1_tac 1);
+by (mk_group1_tac 1);
+by (group1_tac 1);
qed "plus_minusR";
goal Group.thy "(x - y) + z = (x + z) - (y::'a::add_agroup)";
-by(mk_group1_tac 1);
-by(agroup1_tac 1);
+by (mk_group1_tac 1);
+by (agroup1_tac 1);
qed "plus_minusL";
goal Group.thy "(x - y) - z = x - (y + (z::'a::add_agroup))";
-by(mk_group1_tac 1);
-by(agroup1_tac 1);
+by (mk_group1_tac 1);
+by (agroup1_tac 1);
qed "minus_minusL";
goal Group.thy "x - (y - z) = (x + z) - (y::'a::add_agroup)";
-by(mk_group1_tac 1);
-by(agroup1_tac 1);
+by (mk_group1_tac 1);
+by (agroup1_tac 1);
qed "minus_minusR";
goal Group.thy "!!x::'a::add_group. (x-y = z) = (x = z+y)";
-by(stac minus_inv 1);
-by(fast_tac (claset() addss (HOL_basic_ss addsimps group1_simps)) 1);
+by (stac minus_inv 1);
+by (fast_tac (claset() addss (HOL_basic_ss addsimps group1_simps)) 1);
qed "minusL_iff";
goal Group.thy "!!x::'a::add_group. (x = y-z) = (x+z = y)";
-by(stac minus_inv 1);
-by(fast_tac (claset() addss (HOL_basic_ss addsimps group1_simps)) 1);
+by (stac minus_inv 1);
+by (fast_tac (claset() addss (HOL_basic_ss addsimps group1_simps)) 1);
qed "minusR_iff";
val agroup2_simps =
--- a/src/HOL/Integ/IntRingDefs.ML Tue Dec 16 15:17:26 1997 +0100
+++ b/src/HOL/Integ/IntRingDefs.ML Tue Dec 16 17:58:03 1997 +0100
@@ -8,9 +8,9 @@
open IntRingDefs;
goalw thy [zero_int_def,zdiff_def] "(zero-x)+(x::int) = zero";
-by(Simp_tac 1);
+by (Simp_tac 1);
qed "left_inv_int";
goalw thy [zero_int_def,zdiff_def] "x-y = (x::int) + (zero-y)";
-by(Simp_tac 1);
+by (Simp_tac 1);
qed "minus_inv_int";
--- a/src/HOL/Integ/Ring.ML Tue Dec 16 15:17:26 1997 +0100
+++ b/src/HOL/Integ/Ring.ML Tue Dec 16 17:58:03 1997 +0100
@@ -29,7 +29,7 @@
by (rtac refl 3);
by (rtac (distribR RS sym) 2);
by (rtac trans 1);
- br(plus_assoc RS sym) 2;
+ by (rtac (plus_assoc RS sym) 2);
by (rtac trans 1);
by (rtac plus_cong 2);
by (rtac refl 2);
@@ -49,7 +49,7 @@
by (rtac refl 3);
by (rtac (distribL RS sym) 2);
by (rtac trans 1);
- br(plus_assoc RS sym) 2;
+ by (rtac (plus_assoc RS sym) 2);
by (rtac trans 1);
by (rtac plus_cong 2);
by (rtac refl 2);
@@ -75,7 +75,7 @@
by (rtac refl 3);
by (rtac (distribR RS sym) 2);
by (rtac trans 1);
- br(plus_assoc RS sym) 2;
+ by (rtac (plus_assoc RS sym) 2);
by (rtac trans 1);
by (rtac plus_cong 2);
by (rtac refl 2);
@@ -101,7 +101,7 @@
by (rtac refl 3);
by (rtac (distribL RS sym) 2);
by (rtac trans 1);
- br(plus_assoc RS sym) 2;
+ by (rtac (plus_assoc RS sym) 2);
by (rtac trans 1);
by (rtac plus_cong 2);
by (rtac refl 2);
@@ -110,13 +110,13 @@
qed "mult_invR";
goal Ring.thy "x*(y-z) = (x*y - x*z::'a::ring)";
-by(mk_group1_tac 1);
-by(simp_tac (HOL_basic_ss addsimps [distribL,mult_invR]) 1);
+by (mk_group1_tac 1);
+by (simp_tac (HOL_basic_ss addsimps [distribL,mult_invR]) 1);
qed "minus_distribL";
goal Ring.thy "(x-y)*z = (x*z - y*z::'a::ring)";
-by(mk_group1_tac 1);
-by(simp_tac (HOL_basic_ss addsimps [distribR,mult_invL]) 1);
+by (mk_group1_tac 1);
+by (simp_tac (HOL_basic_ss addsimps [distribR,mult_invL]) 1);
qed "minus_distribR";
val cring_simps = [times_assoc,times_commute,times_commuteL,
--- a/src/HOL/Lex/Prefix.ML Tue Dec 16 15:17:26 1997 +0100
+++ b/src/HOL/Lex/Prefix.ML Tue Dec 16 17:58:03 1997 +0100
@@ -35,7 +35,7 @@
qed "prefix_Cons";
goalw Prefix.thy [prefix_def] "(x#xs <= y#ys) = (x=y & xs<=ys)";
-by(Simp_tac 1);
+by (Simp_tac 1);
by (Fast_tac 1);
qed"Cons_prefix_Cons";
Addsimps [Cons_prefix_Cons];
--- a/src/HOL/Lex/Regset_of_auto.ML Tue Dec 16 15:17:26 1997 +0100
+++ b/src/HOL/Lex/Regset_of_auto.ML Tue Dec 16 17:58:03 1997 +0100
@@ -13,42 +13,42 @@
(* Induction over the length of a list: *)
val prems = goal thy
"(!!xs::'a list. (!ys. length ys < length xs --> P ys) ==> P xs) ==> P xs";
-by(res_inst_tac [("P","P"),("r","measure length::('a list * 'a list)set")]
+by (res_inst_tac [("P","P"),("r","measure length::('a list * 'a list)set")]
wf_induct 1);
-by(Simp_tac 1);
-by(asm_full_simp_tac (simpset() addsimps [measure_def,inv_image_def]) 1);
-bes prems 1;
+by (Simp_tac 1);
+by (asm_full_simp_tac (simpset() addsimps [measure_def,inv_image_def]) 1);
+by (eresolve_tac prems 1);
qed "list_length_induct";
*)
goal thy "(butlast xs = []) = (case xs of [] => True | y#ys => ys=[])";
-by(exhaust_tac "xs" 1);
-by(ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if])));
+by (exhaust_tac "xs" 1);
+by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if])));
qed "butlast_empty";
AddIffs [butlast_empty];
goal thy "x:set(butlast xs) --> xs:set xss --> x:set(butlast(concat xss))";
-by(induct_tac "xss" 1);
- by(Simp_tac 1);
-by(asm_simp_tac (simpset() addsimps [butlast_append] delsimps ball_simps
+by (induct_tac "xss" 1);
+ by (Simp_tac 1);
+by (asm_simp_tac (simpset() addsimps [butlast_append] delsimps ball_simps
addsplits [expand_if]) 1);
-br conjI 1;
- by(Clarify_tac 1);
- br conjI 1;
- by(Blast_tac 1);
- by(Clarify_tac 1);
- by(subgoal_tac "xs=[]" 1);
- by(rotate_tac ~1 1);
- by(Asm_full_simp_tac 1);
- by(Blast_tac 1);
-by(blast_tac (claset() addDs [in_set_butlastD]) 1);
+by (rtac conjI 1);
+ by (Clarify_tac 1);
+ by (rtac conjI 1);
+ by (Blast_tac 1);
+ by (Clarify_tac 1);
+ by (subgoal_tac "xs=[]" 1);
+ by (rotate_tac ~1 1);
+ by (Asm_full_simp_tac 1);
+ by (Blast_tac 1);
+by (blast_tac (claset() addDs [in_set_butlastD]) 1);
qed_spec_mp "in_set_butlast_concatI";
(* Regular sets *)
goal thy "(!xs: set xss. xs:A) --> concat xss : star A";
-by(induct_tac "xss" 1);
-by(ALLGOALS Asm_full_simp_tac);
+by (induct_tac "xss" 1);
+by (ALLGOALS Asm_full_simp_tac);
qed_spec_mp "concat_in_star";
(* The main lemma:
@@ -60,162 +60,162 @@
\ (!mid:set mids. (deltas A mid k = k) & \
\ (!n:set(butlast(trace A k mid)). n ~= k)) & \
\ (!n:set(butlast(trace A k suf)). n ~= k))";
-by(induct_tac "xs" 1);
- by(Simp_tac 1);
-by(rename_tac "a as" 1);
-br allI 1;
-by(case_tac "A a i = k" 1);
- by(strip_tac 1);
- by(res_inst_tac[("x","[a]")]exI 1);
- by(Asm_full_simp_tac 1);
- by(case_tac "k : set(trace A (A a i) as)" 1);
- be allE 1;
- be impE 1;
- ba 1;
- by(REPEAT(etac exE 1));
- by(res_inst_tac[("x","pref#mids")]exI 1);
- by(res_inst_tac[("x","suf")]exI 1);
- by(Asm_full_simp_tac 1);
- by(res_inst_tac[("x","[]")]exI 1);
- by(res_inst_tac[("x","as")]exI 1);
- by(Asm_full_simp_tac 1);
- by(blast_tac (claset() addDs [in_set_butlastD]) 1);
-by(Asm_simp_tac 1);
-br conjI 1;
- by(Blast_tac 1);
-by(strip_tac 1);
-be allE 1;
-be impE 1;
- ba 1;
-by(REPEAT(etac exE 1));
-by(res_inst_tac[("x","a#pref")]exI 1);
-by(res_inst_tac[("x","mids")]exI 1);
-by(res_inst_tac[("x","suf")]exI 1);
-by(asm_simp_tac (simpset() addsplits [expand_if]) 1);
+by (induct_tac "xs" 1);
+ by (Simp_tac 1);
+by (rename_tac "a as" 1);
+by (rtac allI 1);
+by (case_tac "A a i = k" 1);
+ by (strip_tac 1);
+ by (res_inst_tac[("x","[a]")]exI 1);
+ by (Asm_full_simp_tac 1);
+ by (case_tac "k : set(trace A (A a i) as)" 1);
+ by (etac allE 1);
+ by (etac impE 1);
+ by (assume_tac 1);
+ by (REPEAT(etac exE 1));
+ by (res_inst_tac[("x","pref#mids")]exI 1);
+ by (res_inst_tac[("x","suf")]exI 1);
+ by (Asm_full_simp_tac 1);
+ by (res_inst_tac[("x","[]")]exI 1);
+ by (res_inst_tac[("x","as")]exI 1);
+ by (Asm_full_simp_tac 1);
+ by (blast_tac (claset() addDs [in_set_butlastD]) 1);
+by (Asm_simp_tac 1);
+by (rtac conjI 1);
+ by (Blast_tac 1);
+by (strip_tac 1);
+by (etac allE 1);
+by (etac impE 1);
+ by (assume_tac 1);
+by (REPEAT(etac exE 1));
+by (res_inst_tac[("x","a#pref")]exI 1);
+by (res_inst_tac[("x","mids")]exI 1);
+by (res_inst_tac[("x","suf")]exI 1);
+by (asm_simp_tac (simpset() addsplits [expand_if]) 1);
qed_spec_mp "decompose";
goal thy "!i. length(trace A i xs) = length xs";
-by(induct_tac "xs" 1);
-by(ALLGOALS Asm_simp_tac);
+by (induct_tac "xs" 1);
+by (ALLGOALS Asm_simp_tac);
qed "length_trace";
Addsimps [length_trace];
goal thy "!i. deltas A (xs@ys) i = deltas A ys (deltas A xs i)";
-by(induct_tac "xs" 1);
-by(ALLGOALS Asm_simp_tac);
+by (induct_tac "xs" 1);
+by (ALLGOALS Asm_simp_tac);
qed "deltas_append";
Addsimps [deltas_append];
goal thy "!i. trace A i (xs@ys) = trace A i xs @ trace A (deltas A xs i) ys";
-by(induct_tac "xs" 1);
-by(ALLGOALS Asm_simp_tac);
+by (induct_tac "xs" 1);
+by (ALLGOALS Asm_simp_tac);
qed "trace_append";
Addsimps [trace_append];
goal thy "(!xs: set xss. deltas A xs i = i) --> \
\ trace A i (concat xss) = concat (map (trace A i) xss)";
-by(induct_tac "xss" 1);
-by(ALLGOALS Asm_simp_tac);
+by (induct_tac "xss" 1);
+by (ALLGOALS Asm_simp_tac);
qed_spec_mp "trace_concat";
Addsimps [trace_concat];
goal thy "!i. (trace A i xs = []) = (xs = [])";
-by(exhaust_tac "xs" 1);
-by(ALLGOALS Asm_simp_tac);
+by (exhaust_tac "xs" 1);
+by (ALLGOALS Asm_simp_tac);
qed "trace_is_Nil";
Addsimps [trace_is_Nil];
goal thy "(trace A i xs = n#ns) = \
\ (case xs of [] => False | y#ys => n = A y i & ns = trace A n ys)";
-by(exhaust_tac "xs" 1);
-by(ALLGOALS Asm_simp_tac);
-by(Blast_tac 1);
+by (exhaust_tac "xs" 1);
+by (ALLGOALS Asm_simp_tac);
+by (Blast_tac 1);
qed_spec_mp "trace_is_Cons_conv";
Addsimps [trace_is_Cons_conv];
goal thy "!i. set(trace A i xs) = \
\ (if xs=[] then {} else insert(deltas A xs i)(set(butlast(trace A i xs))))";
-by(induct_tac "xs" 1);
- by(Simp_tac 1);
-by(asm_simp_tac (simpset() addsimps [insert_commute] addsplits [expand_if]) 1);
+by (induct_tac "xs" 1);
+ by (Simp_tac 1);
+by (asm_simp_tac (simpset() addsimps [insert_commute] addsplits [expand_if]) 1);
qed "set_trace_conv";
goal thy
"(!mid:set mids. deltas A mid k = k) --> deltas A (concat mids) k = k";
-by(induct_tac "mids" 1);
-by(ALLGOALS Asm_simp_tac);
+by (induct_tac "mids" 1);
+by (ALLGOALS Asm_simp_tac);
qed_spec_mp "deltas_concat";
Addsimps [deltas_concat];
goal Nat.thy "!!n. [| n < Suc k; n ~= k |] ==> n < k";
-be nat_neqE 1;
-by(ALLGOALS trans_tac);
+by (etac nat_neqE 1);
+by (ALLGOALS trans_tac);
val lemma = result();
goal thy
"!i j xs. xs : regset_of A i j k = \
\ ((!n:set(butlast(trace A i xs)). n < k) & deltas A xs i = j)";
-by(induct_tac "k" 1);
- by(simp_tac (simpset() addcongs [conj_cong]
+by (induct_tac "k" 1);
+ by (simp_tac (simpset() addcongs [conj_cong]
addsplits [expand_if,split_list_case]) 1);
-by(strip_tac 1);
-by(asm_simp_tac (simpset() addsimps [conc_def]) 1);
-br iffI 1;
- be disjE 1;
- by(Asm_simp_tac 1);
- by(REPEAT(eresolve_tac[exE,conjE] 1));
- by(Asm_full_simp_tac 1);
- by(subgoal_tac
+by (strip_tac 1);
+by (asm_simp_tac (simpset() addsimps [conc_def]) 1);
+by (rtac iffI 1);
+ by (etac disjE 1);
+ by (Asm_simp_tac 1);
+ by (REPEAT(eresolve_tac[exE,conjE] 1));
+ by (Asm_full_simp_tac 1);
+ by (subgoal_tac
"(!n:set(butlast(trace A k xsb)). n < Suc k) & deltas A xsb k = k" 1);
- by(asm_simp_tac (simpset() addsplits [expand_if]
+ by (asm_simp_tac (simpset() addsplits [expand_if]
addsimps [set_trace_conv,butlast_append,ball_Un]) 1);
- be star.induct 1;
- by(Simp_tac 1);
- by(asm_full_simp_tac (simpset() addsplits [expand_if]
+ by (etac star.induct 1);
+ by (Simp_tac 1);
+ by (asm_full_simp_tac (simpset() addsplits [expand_if]
addsimps [set_trace_conv,butlast_append,ball_Un]) 1);
-by(case_tac "k : set(butlast(trace A i xs))" 1);
- br disjI1 2;
- by(blast_tac (claset() addIs [lemma]) 2);
-br disjI2 1;
-bd (in_set_butlastD RS decompose) 1;
-by(Clarify_tac 1);
-by(res_inst_tac [("x","pref")] exI 1);
-by(Asm_full_simp_tac 1);
-br conjI 1;
- br ballI 1;
- br lemma 1;
- by(Asm_simp_tac 2);
- by(EVERY[dtac bspec 1, atac 2]);
- by(Asm_simp_tac 1);
-by(res_inst_tac [("x","concat mids")] exI 1);
-by(Simp_tac 1);
-br conjI 1;
- br concat_in_star 1;
- by(Asm_simp_tac 1);
- br ballI 1;
- br ballI 1;
- br lemma 1;
- by(Asm_simp_tac 2);
- by(EVERY[dtac bspec 1, atac 2]);
- by(asm_simp_tac (simpset() addsimps [image_eqI,in_set_butlast_concatI]) 1);
-br ballI 1;
-br lemma 1;
- by(Asm_simp_tac 2);
-by(EVERY[dtac bspec 1, atac 2]);
-by(Asm_simp_tac 1);
+by (case_tac "k : set(butlast(trace A i xs))" 1);
+ by (rtac disjI1 2);
+ by (blast_tac (claset() addIs [lemma]) 2);
+by (rtac disjI2 1);
+by (dtac (in_set_butlastD RS decompose) 1);
+by (Clarify_tac 1);
+by (res_inst_tac [("x","pref")] exI 1);
+by (Asm_full_simp_tac 1);
+by (rtac conjI 1);
+ by (rtac ballI 1);
+ by (rtac lemma 1);
+ by (Asm_simp_tac 2);
+ by (EVERY[dtac bspec 1, atac 2]);
+ by (Asm_simp_tac 1);
+by (res_inst_tac [("x","concat mids")] exI 1);
+by (Simp_tac 1);
+by (rtac conjI 1);
+ by (rtac concat_in_star 1);
+ by (Asm_simp_tac 1);
+ by (rtac ballI 1);
+ by (rtac ballI 1);
+ by (rtac lemma 1);
+ by (Asm_simp_tac 2);
+ by (EVERY[dtac bspec 1, atac 2]);
+ by (asm_simp_tac (simpset() addsimps [image_eqI,in_set_butlast_concatI]) 1);
+by (rtac ballI 1);
+by (rtac lemma 1);
+ by (Asm_simp_tac 2);
+by (EVERY[dtac bspec 1, atac 2]);
+by (Asm_simp_tac 1);
qed_spec_mp "regset_of_spec";
goal thy "!!A. !n. n < k --> (!x. A x n < k) ==> \
\ !i. i < k --> (!n:set(trace A i xs). n < k)";
-by(induct_tac "xs" 1);
- by(ALLGOALS Simp_tac);
-by(Blast_tac 1);
+by (induct_tac "xs" 1);
+ by (ALLGOALS Simp_tac);
+by (Blast_tac 1);
qed_spec_mp "trace_below";
goal thy "!!A. [| !n. n < k --> (!x. A x n < k); i < k; j < k |] ==> \
\ regset_of A i j k = {xs. deltas A xs i = j}";
-br set_ext 1;
-by(simp_tac (simpset() addsimps [regset_of_spec]) 1);
-by(blast_tac (claset() addDs [trace_below,in_set_butlastD]) 1);
+by (rtac set_ext 1);
+by (simp_tac (simpset() addsimps [regset_of_spec]) 1);
+by (blast_tac (claset() addDs [trace_below,in_set_butlastD]) 1);
qed "regset_of_below";
--- a/src/HOL/List.ML Tue Dec 16 15:17:26 1997 +0100
+++ b/src/HOL/List.ML Tue Dec 16 17:58:03 1997 +0100
@@ -39,7 +39,7 @@
qed_spec_mp "lists_IntI";
goal thy "lists (A Int B) = lists A Int lists B";
-br (mono_Int RS equalityI) 1;
+by (rtac (mono_Int RS equalityI) 1);
by (simp_tac (simpset() addsimps [mono_def, lists_mono]) 1);
by (blast_tac (claset() addSIs [lists_IntI]) 1);
qed "lists_Int_eq";
@@ -85,8 +85,8 @@
Addsimps [length_rev];
goal List.thy "!!xs. xs ~= [] ==> length(tl xs) = pred(length xs)";
-by(exhaust_tac "xs" 1);
-by(ALLGOALS Asm_full_simp_tac);
+by (exhaust_tac "xs" 1);
+by (ALLGOALS Asm_full_simp_tac);
qed "length_tl";
Addsimps [length_tl];
@@ -151,17 +151,17 @@
goal thy "!ys. length xs = length ys | length us = length vs \
\ --> (xs@us = ys@vs) = (xs=ys & us=vs)";
-by(induct_tac "xs" 1);
- by(rtac allI 1);
- by(exhaust_tac "ys" 1);
- by(Asm_simp_tac 1);
- by(fast_tac (claset() addIs [less_add_Suc2] addss simpset()
+by (induct_tac "xs" 1);
+ by (rtac allI 1);
+ by (exhaust_tac "ys" 1);
+ by (Asm_simp_tac 1);
+ by (fast_tac (claset() addIs [less_add_Suc2] addss simpset()
addEs [less_not_refl2 RSN (2,rev_notE)]) 1);
-by(rtac allI 1);
-by(exhaust_tac "ys" 1);
- by(fast_tac (claset() addIs [less_add_Suc2] addss simpset()
+by (rtac allI 1);
+by (exhaust_tac "ys" 1);
+ by (fast_tac (claset() addIs [less_add_Suc2] addss simpset()
addEs [(less_not_refl2 RS not_sym) RSN (2,rev_notE)]) 1);
-by(Asm_simp_tac 1);
+by (Asm_simp_tac 1);
qed_spec_mp "append_eq_append_conv";
Addsimps [append_eq_append_conv];
@@ -246,22 +246,22 @@
(* a congruence rule for map: *)
goal thy
"(xs=ys) --> (!x. x : set ys --> f x = g x) --> map f xs = map g ys";
-by(rtac impI 1);
-by(hyp_subst_tac 1);
-by(induct_tac "ys" 1);
-by(ALLGOALS Asm_simp_tac);
+by (rtac impI 1);
+by (hyp_subst_tac 1);
+by (induct_tac "ys" 1);
+by (ALLGOALS Asm_simp_tac);
val lemma = result();
bind_thm("map_cong",impI RSN (2,allI RSN (2,lemma RS mp RS mp)));
goal List.thy "(map f xs = []) = (xs = [])";
-by(induct_tac "xs" 1);
-by(ALLGOALS Asm_simp_tac);
+by (induct_tac "xs" 1);
+by (ALLGOALS Asm_simp_tac);
qed "map_is_Nil_conv";
AddIffs [map_is_Nil_conv];
goal List.thy "([] = map f xs) = (xs = [])";
-by(induct_tac "xs" 1);
-by(ALLGOALS Asm_simp_tac);
+by (induct_tac "xs" 1);
+by (ALLGOALS Asm_simp_tac);
qed "Nil_is_map_conv";
AddIffs [Nil_is_map_conv];
@@ -283,14 +283,14 @@
Addsimps[rev_rev_ident];
goal thy "(rev xs = []) = (xs = [])";
-by(induct_tac "xs" 1);
-by(ALLGOALS Asm_simp_tac);
+by (induct_tac "xs" 1);
+by (ALLGOALS Asm_simp_tac);
qed "rev_is_Nil_conv";
AddIffs [rev_is_Nil_conv];
goal thy "([] = rev xs) = (xs = [])";
-by(induct_tac "xs" 1);
-by(ALLGOALS Asm_simp_tac);
+by (induct_tac "xs" 1);
+by (ALLGOALS Asm_simp_tac);
qed "Nil_is_rev_conv";
AddIffs [Nil_is_rev_conv];
@@ -401,14 +401,14 @@
Addsimps [concat_append];
goal thy "(concat xss = []) = (!xs:set xss. xs=[])";
-by(induct_tac "xss" 1);
-by(ALLGOALS Asm_simp_tac);
+by (induct_tac "xss" 1);
+by (ALLGOALS Asm_simp_tac);
qed "concat_eq_Nil_conv";
AddIffs [concat_eq_Nil_conv];
goal thy "([] = concat xss) = (!xs:set xss. xs=[])";
-by(induct_tac "xss" 1);
-by(ALLGOALS Asm_simp_tac);
+by (induct_tac "xss" 1);
+by (ALLGOALS Asm_simp_tac);
qed "Nil_eq_concat_conv";
AddIffs [Nil_eq_concat_conv];
@@ -488,39 +488,39 @@
(** last & butlast **)
goal thy "last(xs@[x]) = x";
-by(induct_tac "xs" 1);
-by(ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if])));
+by (induct_tac "xs" 1);
+by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if])));
qed "last_snoc";
Addsimps [last_snoc];
goal thy "butlast(xs@[x]) = xs";
-by(induct_tac "xs" 1);
-by(ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if])));
+by (induct_tac "xs" 1);
+by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if])));
qed "butlast_snoc";
Addsimps [butlast_snoc];
goal thy
"!ys. butlast (xs@ys) = (if ys=[] then butlast xs else xs@butlast ys)";
-by(induct_tac "xs" 1);
-by(ALLGOALS(asm_simp_tac (simpset() addsplits [expand_if])));
+by (induct_tac "xs" 1);
+by (ALLGOALS(asm_simp_tac (simpset() addsplits [expand_if])));
qed_spec_mp "butlast_append";
goal thy "x:set(butlast xs) --> x:set xs";
-by(induct_tac "xs" 1);
-by(ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if])));
+by (induct_tac "xs" 1);
+by (ALLGOALS (asm_simp_tac (simpset() addsplits [expand_if])));
qed_spec_mp "in_set_butlastD";
goal thy "!!xs. x:set(butlast xs) ==> x:set(butlast(xs@ys))";
-by(asm_simp_tac (simpset() addsimps [butlast_append]
+by (asm_simp_tac (simpset() addsimps [butlast_append]
addsplits [expand_if]) 1);
-by(blast_tac (claset() addDs [in_set_butlastD]) 1);
+by (blast_tac (claset() addDs [in_set_butlastD]) 1);
qed "in_set_butlast_appendI1";
goal thy "!!xs. x:set(butlast ys) ==> x:set(butlast(xs@ys))";
-by(asm_simp_tac (simpset() addsimps [butlast_append]
+by (asm_simp_tac (simpset() addsimps [butlast_append]
addsplits [expand_if]) 1);
-by(Clarify_tac 1);
-by(Full_simp_tac 1);
+by (Clarify_tac 1);
+by (Full_simp_tac 1);
qed "in_set_butlast_appendI2";
(** take & drop **)
@@ -720,11 +720,11 @@
section "replicate";
goal thy "set(replicate (Suc n) x) = {x}";
-by(induct_tac "n" 1);
-by(ALLGOALS Asm_full_simp_tac);
+by (induct_tac "n" 1);
+by (ALLGOALS Asm_full_simp_tac);
val lemma = result();
goal thy "!!n. n ~= 0 ==> set(replicate n x) = {x}";
-by(fast_tac (claset() addSDs [not0_implies_Suc] addSIs [lemma]) 1);
+by (fast_tac (claset() addSDs [not0_implies_Suc] addSIs [lemma]) 1);
qed "set_replicate";
Addsimps [set_replicate];
--- a/src/HOL/Map.ML Tue Dec 16 15:17:26 1997 +0100
+++ b/src/HOL/Map.ML Tue Dec 16 17:58:03 1997 +0100
@@ -7,72 +7,72 @@
*)
goalw thy [empty_def] "empty k = None";
-by(Simp_tac 1);
+by (Simp_tac 1);
qed "empty_def2";
Addsimps [empty_def2];
goalw thy [update_def] "(m[a|->b])x = (if x=a then Some b else m x)";
-by(Simp_tac 1);
+by (Simp_tac 1);
qed "update_def2";
Addsimps [update_def2];
section "++";
goalw thy [override_def] "m ++ empty = m";
-by(Simp_tac 1);
+by (Simp_tac 1);
qed "override_empty";
Addsimps [override_empty];
goalw thy [override_def] "empty ++ m = m";
-by(Simp_tac 1);
-br ext 1;
-by(split_tac [split_option_case] 1);
-by(Simp_tac 1);
+by (Simp_tac 1);
+by (rtac ext 1);
+by (split_tac [split_option_case] 1);
+by (Simp_tac 1);
qed "empty_override";
Addsimps [empty_override];
goalw thy [override_def]
"((m ++ n) k = Some x) = (n k = Some x | n k = None & m k = Some x)";
-by(simp_tac (simpset() addsplits [split_option_case]) 1);
+by (simp_tac (simpset() addsplits [split_option_case]) 1);
qed_spec_mp "override_Some_iff";
bind_thm("override_SomeD", standard(override_Some_iff RS iffD1));
goalw thy [override_def]
"((m ++ n) k = None) = (n k = None & m k = None)";
-by(simp_tac (simpset() addsplits [split_option_case]) 1);
+by (simp_tac (simpset() addsplits [split_option_case]) 1);
qed "override_None";
AddIffs [override_None];
goalw thy [override_def] "map_of(xs@ys) = map_of ys ++ map_of xs";
-by(induct_tac "xs" 1);
-by(Simp_tac 1);
-br ext 1;
-by(asm_simp_tac (simpset() addsplits [expand_if,split_option_case]) 1);
+by (induct_tac "xs" 1);
+by (Simp_tac 1);
+by (rtac ext 1);
+by (asm_simp_tac (simpset() addsplits [expand_if,split_option_case]) 1);
qed "map_of_append";
Addsimps [map_of_append];
section "dom";
goalw thy [dom_def] "dom empty = {}";
-by(Simp_tac 1);
+by (Simp_tac 1);
qed "dom_empty";
Addsimps [dom_empty];
goalw thy [dom_def] "dom(m[a|->b]) = insert a (dom m)";
-by(simp_tac (simpset() addsplits [expand_if]) 1);
-by(Blast_tac 1);
+by (simp_tac (simpset() addsplits [expand_if]) 1);
+by (Blast_tac 1);
qed "dom_update";
Addsimps [dom_update];
goalw thy [dom_def] "dom(m++n) = dom n Un dom m";
-by(Blast_tac 1);
+by (Blast_tac 1);
qed "dom_override";
Addsimps [dom_override];
section "ran";
goalw thy [ran_def] "ran empty = {}";
-by(Simp_tac 1);
+by (Simp_tac 1);
qed "ran_empty";
Addsimps [ran_empty];
--- a/src/HOL/MiniML/Maybe.ML Tue Dec 16 15:17:26 1997 +0100
+++ b/src/HOL/MiniML/Maybe.ML Tue Dec 16 17:58:03 1997 +0100
@@ -18,17 +18,17 @@
(* expansion of option_bind *)
goalw thy [option_bind_def] "P(option_bind res f) = \
\ ((res = None --> P None) & (!s. res = Some s --> P(f s)))";
-br split_option_case 1;
+by (rtac split_option_case 1);
qed "split_option_bind";
goal thy
"((option_bind m f) = None) = ((m=None) | (? p. m = Some p & f p = None))";
-by(simp_tac (simpset() addsplits [split_option_bind]) 1);
+by (simp_tac (simpset() addsplits [split_option_bind]) 1);
qed "option_bind_eq_None";
Addsimps [option_bind_eq_None];
(* auxiliary lemma *)
goal Maybe.thy "(y = Some x) = (Some x = y)";
-by( simp_tac (simpset() addsimps [eq_sym_conv]) 1);
+by ( simp_tac (simpset() addsimps [eq_sym_conv]) 1);
qed "rotate_Some";
--- a/src/HOL/MiniML/W.ML Tue Dec 16 15:17:26 1997 +0100
+++ b/src/HOL/MiniML/W.ML Tue Dec 16 17:58:03 1997 +0100
@@ -24,10 +24,10 @@
by (fast_tac (HOL_cs addDs [Suc_leD]) 1);
(* case App e1 e2 *)
by (simp_tac (simpset() addsplits [split_option_bind]) 1);
-by(blast_tac (claset() addIs [le_SucI,le_trans]) 1);
+by (blast_tac (claset() addIs [le_SucI,le_trans]) 1);
(* case LET e1 e2 *)
by (simp_tac (simpset() addsplits [split_option_bind]) 1);
-by(blast_tac (claset() addIs [le_trans]) 1);
+by (blast_tac (claset() addIs [le_trans]) 1);
qed_spec_mp "W_var_ge";
Addsimps [W_var_ge];
@@ -139,9 +139,9 @@
(* 41: case LET e1 e2 *)
by (simp_tac (simpset() addsplits [split_option_bind]) 1);
by (strip_tac 1);
-by(EVERY1[etac allE,etac allE,etac allE,etac allE,etac allE,mp_tac,mp_tac]);
+by (EVERY1[etac allE,etac allE,etac allE,etac allE,etac allE,mp_tac,mp_tac]);
by (etac conjE 1);
-by(EVERY[etac allE 1,etac allE 1,etac allE 1,etac allE 1,etac allE 1,
+by (EVERY[etac allE 1,etac allE 1,etac allE 1,etac allE 1,etac allE 1,
etac impE 1, mp_tac 2]);
by (SELECT_GOAL(rewtac new_tv_def)1);
by (Asm_simp_tac 1);
--- a/src/HOL/NatDef.ML Tue Dec 16 15:17:26 1997 +0100
+++ b/src/HOL/NatDef.ML Tue Dec 16 17:58:03 1997 +0100
@@ -293,12 +293,12 @@
qed "gr_implies_not0";
goal thy "(n ~= 0) = (0 < n)";
-br iffI 1;
- by(etac gr_implies_not0 2);
-by(rtac natE 1);
- by(contr_tac 1);
-by(etac ssubst 1);
-by(rtac zero_less_Suc 1);
+by (rtac iffI 1);
+ by (etac gr_implies_not0 2);
+by (rtac natE 1);
+ by (contr_tac 1);
+by (etac ssubst 1);
+by (rtac zero_less_Suc 1);
qed "neq0_conv";
Addsimps [neq0_conv];
AddSDs [neq0_conv RS iffD1];
@@ -306,9 +306,9 @@
bind_thm("gr0I", notI RS (neq0_conv RS iffD1));
goal thy "(~(0 < n)) = (n=0)";
-br iffI 1;
- be swap 1;
- by(ALLGOALS Asm_full_simp_tac);
+by (rtac iffI 1);
+ by (etac swap 1);
+ by (ALLGOALS Asm_full_simp_tac);
qed "not_gr0";
Addsimps [not_gr0];
--- a/src/HOL/Prod.ML Tue Dec 16 15:17:26 1997 +0100
+++ b/src/HOL/Prod.ML Tue Dec 16 17:58:03 1997 +0100
@@ -91,7 +91,7 @@
which cannot be solved by reflexivity.
val [prem] = goal Prod.thy "(!!x. PROP P x) ==> (!!a b. PROP P(a,b))";
-br prem 1;
+by (rtac prem 1);
val lemma1 = result();
local
@@ -106,13 +106,13 @@
val [prem] = goal Prod.thy "(!!a b. PROP P(a,b)) ==> PROP P x";
-bw adhoc;
-br prem 1;
+by (rewtac adhoc);
+by (rtac prem 1);
val lemma = result();
val [prem] = goal Prod.thy "(!!a b. PROP P(a,b)) ==> (!!x. PROP P x)";
-br lemma 1;
-br prem 1;
+by (rtac lemma 1);
+by (rtac prem 1);
val lemma2 = result();
bind_thm("split_paired_all", equal_intr lemma1 lemma2);
--- a/src/HOL/Relation.ML Tue Dec 16 15:17:26 1997 +0100
+++ b/src/HOL/Relation.ML Tue Dec 16 17:58:03 1997 +0100
@@ -109,7 +109,7 @@
Addsimps [inverse_inverse];
goal Relation.thy "(r O s)^-1 = s^-1 O r^-1";
-by(Blast_tac 1);
+by (Blast_tac 1);
qed "inverse_comp";
(** Domain **)
--- a/src/HOL/Set.ML Tue Dec 16 15:17:26 1997 +0100
+++ b/src/HOL/Set.ML Tue Dec 16 17:58:03 1997 +0100
@@ -452,7 +452,7 @@
AddSEs [singletonE];
goal Set.thy "{x. x=a} = {a}";
-by(Blast_tac 1);
+by (Blast_tac 1);
qed "singleton_conv";
Addsimps [singleton_conv];
--- a/src/HOL/TLA/TLA.ML Tue Dec 16 15:17:26 1997 +0100
+++ b/src/HOL/TLA/TLA.ML Tue Dec 16 17:58:03 1997 +0100
@@ -1046,12 +1046,12 @@
example of a history variable: existence of a clock
goal TLA.thy "(EEX h. Init($h .= #True) .& [](h$ .~= $h))";
-br tempI 1;
-br historyI 1;
-bws action_rews;
+by (rtac tempI 1);
+by (rtac historyI 1);
+by (rewrite_goals_tac action_rews);
by (TRYALL (rtac impI));
by (TRYALL (etac conjE));
-ba 3;
+by (assume_tac 3);
by (Asm_full_simp_tac 3);
by (auto_tac (temp_css addSIs2 [(temp_unlift Init_true) RS iffD2, temp_unlift BoxTrue]));
(** solved **)
--- a/src/HOL/equalities.ML Tue Dec 16 15:17:26 1997 +0100
+++ b/src/HOL/equalities.ML Tue Dec 16 17:58:03 1997 +0100
@@ -598,7 +598,7 @@
qed "subset_iff_psubset_eq";
goal thy "(!x. x ~: A) = (A={})";
-by(Blast_tac 1);
+by (Blast_tac 1);
qed "all_not_in_conv";
AddIffs [all_not_in_conv];
--- a/src/HOL/ex/Qsort.ML Tue Dec 16 15:17:26 1997 +0100
+++ b/src/HOL/ex/Qsort.ML Tue Dec 16 17:58:03 1997 +0100
@@ -15,7 +15,7 @@
val [p1] = goalw WF.thy [wf_def]
"wf(R) ==> (!Q. (? x. Q x) --> (? min. Q min & (!b. (b,min):R --> (~ Q b))))";
by (rtac allI 1);
-by(cut_inst_tac[("x","%u.~Q u")](p1 RS spec) 1);
+by (cut_inst_tac[("x","%u.~Q u")](p1 RS spec) 1);
by (fast_tac HOL_cs 1);
val wf_minimal = result();
@@ -30,7 +30,7 @@
qed "qsort_permutes";
goal Qsort.thy "set(qsort le xs) = set xs";
-by(simp_tac (simpset() addsimps [set_via_mset,qsort_permutes]) 1);
+by (simp_tac (simpset() addsimps [set_via_mset,qsort_permutes]) 1);
qed "set_qsort";
Addsimps [set_qsort];
--- a/src/HOL/ex/Recdef.ML Tue Dec 16 15:17:26 1997 +0100
+++ b/src/HOL/ex/Recdef.ML Tue Dec 16 17:58:03 1997 +0100
@@ -38,9 +38,9 @@
(* proving the termination condition: *)
val [tc] = mapf.tcs;
goalw_cterm [] (cterm_of (sign_of thy) (HOLogic.mk_Trueprop tc));
-br allI 1;
-by(case_tac "n=0" 1);
-by(ALLGOALS Asm_simp_tac);
+by (rtac allI 1);
+by (case_tac "n=0" 1);
+by (ALLGOALS Asm_simp_tac);
val lemma = result();
(* removing the termination condition from the generated thms: *)
--- a/src/HOLCF/Cfun3.ML Tue Dec 16 15:17:26 1997 +0100
+++ b/src/HOLCF/Cfun3.ML Tue Dec 16 17:58:03 1997 +0100
@@ -382,7 +382,7 @@
[
cut_facts_tac prems 1,
rtac allI 1,
- rtac (contlub_cfun_fun RS ssubst) 1,
+ stac contlub_cfun_fun 1,
atac 1,
fast_tac (HOL_cs addSIs [thelubI,chfin,lub_finch2,chfin2finch,ch2ch_fappL])1
]);
--- a/src/HOLCF/Discrete.ML Tue Dec 16 15:17:26 1997 +0100
+++ b/src/HOLCF/Discrete.ML Tue Dec 16 17:58:03 1997 +0100
@@ -5,16 +5,16 @@
*)
goalw thy [undiscr_def] "undiscr(Discr x) = x";
-by(Simp_tac 1);
+by (Simp_tac 1);
qed "undiscr_Discr";
Addsimps [undiscr_Discr];
goal thy
"!!S::nat=>('a::term)discr. is_chain(S) ==> range(%i. f(S i)) = {f(S 0)}";
-by(fast_tac (claset() addDs [discr_chain0] addEs [arg_cong]) 1);
+by (fast_tac (claset() addDs [discr_chain0] addEs [arg_cong]) 1);
qed "discr_chain_f_range0";
goalw thy [cont,is_lub,is_ub] "cont(%x::('a::term)discr. f x)";
-by(simp_tac (simpset() addsimps [discr_chain_f_range0]) 1);
+by (simp_tac (simpset() addsimps [discr_chain_f_range0]) 1);
qed "cont_discr";
AddIffs [cont_discr];
--- a/src/HOLCF/Fix.ML Tue Dec 16 15:17:26 1997 +0100
+++ b/src/HOLCF/Fix.ML Tue Dec 16 17:58:03 1997 +0100
@@ -889,7 +889,7 @@
goal Fix.thy "!! P. [| adm (%x. P x --> Q x); adm (%x. Q x --> P x) |] \
\ ==> adm (%x. P x = Q x)";
-by(subgoal_tac "(%x. P x = Q x) = (%x. (P x --> Q x) & (Q x --> P x))" 1);
+by (subgoal_tac "(%x. P x = Q x) = (%x. (P x --> Q x) & (Q x --> P x))" 1);
by (Asm_simp_tac 1);
by (rtac ext 1);
by (fast_tac HOL_cs 1);
--- a/src/HOLCF/IMP/HoareEx.ML Tue Dec 16 15:17:26 1997 +0100
+++ b/src/HOLCF/IMP/HoareEx.ML Tue Dec 16 17:58:03 1997 +0100
@@ -8,12 +8,12 @@
val prems = goalw thy [hoare_valid_def]
"|= {A} c {A} ==> |= {A} WHILE b DO c {%s. A s & ~b s}";
-by(cut_facts_tac prems 1);
+by (cut_facts_tac prems 1);
by (Simp_tac 1);
by (rtac fix_ind 1);
(* simplifier with enhanced adm-tactic: *)
by (Simp_tac 1);
by (Simp_tac 1);
by (simp_tac (simpset() setloop (split_tac[expand_if])) 1);
-by(Blast_tac 1);
+by (Blast_tac 1);
qed "WHILE_rule_sound";
--- a/src/HOLCF/IOA/ABP/Correctness.ML Tue Dec 16 15:17:26 1997 +0100
+++ b/src/HOLCF/IOA/ABP/Correctness.ML Tue Dec 16 17:58:03 1997 +0100
@@ -54,7 +54,7 @@
by (REPEAT (rtac allI 1));
by (rtac impI 1);
by (hyp_subst_tac 1);
- by (rtac (expand_if RS ssubst) 1);
+ by (stac expand_if 1);
by (Asm_full_simp_tac 1);
by (Asm_full_simp_tac 1);
val l_iff_red_nil = result();
@@ -72,7 +72,7 @@
by (asm_full_simp_tac list_ss 1);
by (REPEAT (rtac allI 1));
by (rtac impI 1);
-by (rtac (expand_if RS ssubst) 1);
+by (stac expand_if 1);
by (REPEAT(hyp_subst_tac 1));
by (etac subst 1);
by (Simp_tac 1);
@@ -91,7 +91,7 @@
by (Asm_full_simp_tac 1);
by (REPEAT (etac exE 1));
by (Asm_simp_tac 1);
-by (rtac (expand_if RS ssubst) 1);
+by (stac expand_if 1);
by (hyp_subst_tac 1);
by (asm_full_simp_tac (simpset() addsimps [reverse_Cons]) 1);
qed"rev_red_not_nil";
@@ -104,7 +104,7 @@
by (asm_full_simp_tac list_ss 1);
by (REPEAT (rtac allI 1));
by (rtac impI 1);
- by (rtac (expand_if RS ssubst) 1);
+ by (stac expand_if 1);
by (asm_full_simp_tac (list_ss addsimps [reverse_Cons,hd_append,
(rev_red_not_nil RS mp)]) 1);
qed"last_ind_on_first";
@@ -116,7 +116,7 @@
"if x=hd(reverse(reduce(l))) & reduce(l)~=[] then \
\ reduce(l@[x])=reduce(l) else \
\ reduce(l@[x])=reduce(l)@[x]";
-by (rtac (expand_if RS ssubst) 1);
+by (stac expand_if 1);
by (rtac conjI 1);
(* --> *)
by (List.list.induct_tac "l" 1);
@@ -154,7 +154,7 @@
by (Asm_full_simp_tac 1);
by (REPEAT (etac exE 1));
by (Asm_full_simp_tac 1);
-by (rtac (expand_if RS ssubst) 1);
+by (stac expand_if 1);
by (rtac conjI 1);
by (simp_tac (simpset() addsimps [and_de_morgan_and_absorbe]) 2);
by (Step_tac 1);
--- a/src/HOLCF/IOA/ABP/Lemmas.ML Tue Dec 16 15:17:26 1997 +0100
+++ b/src/HOLCF/IOA/ABP/Lemmas.ML Tue Dec 16 17:58:03 1997 +0100
@@ -8,7 +8,7 @@
(* Logic *)
val prems = goal HOL.thy "(P ==> Q-->R) ==> P&Q --> R";
- by(fast_tac (claset() addDs prems) 1);
+ by (fast_tac (claset() addDs prems) 1);
qed "imp_conj_lemma";
goal HOL.thy "(~(A&B)) = ((~A)&B| ~B)";
@@ -16,7 +16,7 @@
val and_de_morgan_and_absorbe = result();
goal HOL.thy "(if C then A else B) --> (A|B)";
-by (rtac (expand_if RS ssubst) 1);
+by (stac expand_if 1);
by (Fast_tac 1);
val bool_if_impl_or = result();
--- a/src/HOLCF/IOA/ABP/ROOT.ML Tue Dec 16 15:17:26 1997 +0100
+++ b/src/HOLCF/IOA/ABP/ROOT.ML Tue Dec 16 17:58:03 1997 +0100
@@ -3,11 +3,8 @@
Author: Olaf Mueller
Copyright 1995 TU Muenchen
-This is the ROOT file for the Alternating Bit Protocol performed in I/O-Automata.
-
-For details see the README.html file.
-
-Should be executed in the subdirectory HOLCF/IOA/examples/ABP.
+This is the ROOT file for the Alternating Bit Protocol performed in
+I/O-Automata.
*)
goals_limit := 1;
--- a/src/HOLCF/IOA/NTP/Abschannel.ML Tue Dec 16 15:17:26 1997 +0100
+++ b/src/HOLCF/IOA/NTP/Abschannel.ML Tue Dec 16 17:58:03 1997 +0100
@@ -25,7 +25,7 @@
\ C_m_r ~: actions(srch_asig) & \
\ C_r_s ~: actions(srch_asig) & C_r_r(m) ~: actions(srch_asig)";
-by(simp_tac (simpset() addsimps unfold_renaming) 1);
+by (simp_tac (simpset() addsimps unfold_renaming) 1);
qed"in_srch_asig";
goal Abschannel.thy
@@ -40,20 +40,20 @@
\ C_r_s ~: actions(rsch_asig) & \
\ C_r_r(m) ~: actions(rsch_asig)";
-by(simp_tac (simpset() addsimps unfold_renaming) 1);
+by (simp_tac (simpset() addsimps unfold_renaming) 1);
qed"in_rsch_asig";
goal Abschannel.thy "srch_ioa = \
\ (srch_asig, {{|}}, srch_trans,srch_wfair,srch_sfair)";
by (simp_tac (simpset() addsimps [srch_asig_def,srch_trans_def, asig_of_def, trans_of_def,
wfair_of_def, sfair_of_def,srch_wfair_def,srch_sfair_def]) 1);
-by(simp_tac (simpset() addsimps unfold_renaming) 1);
+by (simp_tac (simpset() addsimps unfold_renaming) 1);
qed"srch_ioa_thm";
goal Abschannel.thy "rsch_ioa = \
\ (rsch_asig, {{|}}, rsch_trans,rsch_wfair,rsch_sfair)";
by (simp_tac (simpset() addsimps [rsch_asig_def,rsch_trans_def, asig_of_def, trans_of_def,
wfair_of_def, sfair_of_def,rsch_wfair_def,rsch_sfair_def]) 1);
-by(simp_tac (simpset() addsimps unfold_renaming) 1);
+by (simp_tac (simpset() addsimps unfold_renaming) 1);
qed"rsch_ioa_thm";
--- a/src/HOLCF/IOA/NTP/Impl.ML Tue Dec 16 15:17:26 1997 +0100
+++ b/src/HOLCF/IOA/NTP/Impl.ML Tue Dec 16 17:58:03 1997 +0100
@@ -33,7 +33,7 @@
\ fst(snd(x)) = rec(x) & \
\ fst(snd(snd(x))) = srch(x) & \
\ snd(snd(snd(x))) = rsch(x)";
-by(simp_tac (simpset() addsimps
+by (simp_tac (simpset() addsimps
[sen_def,rec_def,srch_def,rsch_def]) 1);
Addsimps [result()];
@@ -41,8 +41,8 @@
\ | a:actions(receiver_asig) \
\ | a:actions(srch_asig) \
\ | a:actions(rsch_asig)";
- by(Action.action.induct_tac "a" 1);
- by(ALLGOALS (Simp_tac));
+ by (Action.action.induct_tac "a" 1);
+ by (ALLGOALS (Simp_tac));
Addsimps [result()];
Delsimps [split_paired_All];
@@ -73,18 +73,18 @@
goalw Impl.thy impl_ioas "invariant impl_ioa inv1";
by (rtac invariantI 1);
-by(asm_full_simp_tac (simpset()
+by (asm_full_simp_tac (simpset()
addsimps [inv1_def, hdr_sum_def, Sender.srcvd_def,
Sender.ssent_def, Receiver.rsent_def,Receiver.rrcvd_def]) 1);
-by(simp_tac (simpset() delsimps [trans_of_par4]
+by (simp_tac (simpset() delsimps [trans_of_par4]
addsimps [fork_lemma,inv1_def]) 1);
(* Split proof in two *)
by (rtac conjI 1);
(* First half *)
-by(asm_full_simp_tac (simpset() addsimps [Impl.inv1_def]) 1);
+by (asm_full_simp_tac (simpset() addsimps [Impl.inv1_def]) 1);
by (rtac Action.action.induct 1);
by (EVERY1[tac, tac, tac, tac]);
@@ -97,13 +97,13 @@
by (tac_ren 1);
(* 4 + 1 *)
-by(EVERY1[tac, tac, tac, tac]);
+by (EVERY1[tac, tac, tac, tac]);
(* Now the other half *)
-by(asm_full_simp_tac (simpset() addsimps [Impl.inv1_def]) 1);
+by (asm_full_simp_tac (simpset() addsimps [Impl.inv1_def]) 1);
by (rtac Action.action.induct 1);
-by(EVERY1[tac, tac]);
+by (EVERY1[tac, tac]);
(* detour 1 *)
by (tac 1);
@@ -171,7 +171,7 @@
(* 10 - 7 *)
by (EVERY1[tac2,tac2,tac2,tac2]);
(* 6 *)
- by(forward_tac [rewrite_rule [Impl.inv1_def]
+ by (forward_tac [rewrite_rule [Impl.inv1_def]
(inv1 RS invariantE) RS conjunct1] 1);
(* 6 - 5 *)
by (EVERY1[tac2,tac2]);
@@ -191,7 +191,7 @@
(* 2 *)
by (tac2 1);
- by(forward_tac [rewrite_rule [Impl.inv1_def]
+ by (forward_tac [rewrite_rule [Impl.inv1_def]
(inv1 RS invariantE) RS conjunct1] 1);
by (rtac impI 1);
by (rtac impI 1);
@@ -201,7 +201,7 @@
(* 1 *)
by (tac2 1);
- by(forward_tac [rewrite_rule [Impl.inv1_def]
+ by (forward_tac [rewrite_rule [Impl.inv1_def]
(inv1 RS invariantE) RS conjunct2] 1);
by (rtac impI 1);
by (rtac impI 1);
@@ -310,7 +310,7 @@
(* 2 b *)
by (strip_tac 1 THEN REPEAT (etac conjE 1));
- by(forward_tac [rewrite_rule [Impl.inv2_def]
+ by (forward_tac [rewrite_rule [Impl.inv2_def]
(inv2 RS invariantE)] 1);
by (tac4 1);
by (Asm_full_simp_tac 1);
@@ -319,9 +319,9 @@
by (tac4 1);
by (strip_tac 1 THEN REPEAT (etac conjE 1));
by (rtac ccontr 1);
- by(forward_tac [rewrite_rule [Impl.inv2_def]
+ by (forward_tac [rewrite_rule [Impl.inv2_def]
(inv2 RS invariantE)] 1);
- by(forward_tac [rewrite_rule [Impl.inv3_def]
+ by (forward_tac [rewrite_rule [Impl.inv3_def]
(inv3 RS invariantE)] 1);
by (Asm_full_simp_tac 1);
by (eres_inst_tac [("x","m")] allE 1);
--- a/src/HOLCF/IOA/NTP/Lemmas.ML Tue Dec 16 15:17:26 1997 +0100
+++ b/src/HOLCF/IOA/NTP/Lemmas.ML Tue Dec 16 17:58:03 1997 +0100
@@ -7,7 +7,7 @@
(* Logic *)
val prems = goal HOL.thy "(P ==> Q-->R) ==> P&Q --> R";
- by(fast_tac (claset() addDs prems) 1);
+ by (fast_tac (claset() addDs prems) 1);
qed "imp_conj_lemma";
goal HOL.thy "(A --> B & C) = ((A --> B) & (A --> C))";
@@ -35,8 +35,8 @@
(* Arithmetic *)
goal Arith.thy "!!x. 0<x ==> (x-1 = y) = (x = Suc(y))";
-by(asm_simp_tac (simpset() addsimps [diff_Suc] addsplits [expand_nat_case]) 1);
-by(Blast_tac 1);
+by (asm_simp_tac (simpset() addsimps [diff_Suc] addsplits [expand_nat_case]) 1);
+by (Blast_tac 1);
qed "pred_suc";
--- a/src/HOLCF/IOA/NTP/Multiset.ML Tue Dec 16 15:17:26 1997 +0100
+++ b/src/HOLCF/IOA/NTP/Multiset.ML Tue Dec 16 17:58:03 1997 +0100
@@ -34,7 +34,7 @@
addsimps [Multiset.delm_nonempty_def,
Multiset.countm_nonempty_def]
setloop (split_tac [expand_if])) 1);
- by (safe_tac (claset()));
+ by Safe_tac;
by (Asm_full_simp_tac 1);
qed "count_delm_simp";
--- a/src/HOLCF/IOA/NTP/ROOT.ML Tue Dec 16 15:17:26 1997 +0100
+++ b/src/HOLCF/IOA/NTP/ROOT.ML Tue Dec 16 17:58:03 1997 +0100
@@ -5,10 +5,6 @@
This is the ROOT file for a network transmission protocol (NTP subdirectory),
performed in the I/O automata formalization by Olaf Mueller.
-
-For details see the README.html file.
-
-Should be executed in the subdirectory HOLCF/IOA/examples/NTP.
*)
goals_limit := 1;
--- a/src/HOLCF/IOA/NTP/Receiver.ML Tue Dec 16 15:17:26 1997 +0100
+++ b/src/HOLCF/IOA/NTP/Receiver.ML Tue Dec 16 17:58:03 1997 +0100
@@ -15,7 +15,7 @@
\ C_m_r : actions(receiver_asig) & \
\ C_r_s ~: actions(receiver_asig) & \
\ C_r_r(m) : actions(receiver_asig)";
- by(simp_tac (simpset() addsimps (Receiver.receiver_asig_def :: actions_def ::
+ by (simp_tac (simpset() addsimps (Receiver.receiver_asig_def :: actions_def ::
asig_projections)) 1);
qed "in_receiver_asig";
--- a/src/HOLCF/IOA/NTP/Sender.ML Tue Dec 16 15:17:26 1997 +0100
+++ b/src/HOLCF/IOA/NTP/Sender.ML Tue Dec 16 17:58:03 1997 +0100
@@ -15,7 +15,7 @@
\ C_m_r ~: actions(sender_asig) & \
\ C_r_s : actions(sender_asig) & \
\ C_r_r(m) ~: actions(sender_asig)";
-by(simp_tac (simpset() addsimps
+by (simp_tac (simpset() addsimps
(Sender.sender_asig_def :: actions_def ::
asig_projections)) 1);
qed "in_sender_asig";
--- a/src/HOLCF/IOA/meta_theory/Automata.ML Tue Dec 16 15:17:26 1997 +0100
+++ b/src/HOLCF/IOA/meta_theory/Automata.ML Tue Dec 16 17:58:03 1997 +0100
@@ -50,7 +50,7 @@
\ (snd(s),a,snd(t)):trans_of(B) \
\ else snd(t) = snd(s))}";
-by(simp_tac (simpset() addsimps (par_def::ioa_projections)) 1);
+by (simp_tac (simpset() addsimps (par_def::ioa_projections)) 1);
qed "trans_of_par";
@@ -179,15 +179,15 @@
(* a:act B *)
by (eres_inst_tac [("x","a")] allE 1);
by (Asm_full_simp_tac 1);
-bd inpAAactB_is_inpBoroutB 1;
-ba 1;
-ba 1;
+by (dtac inpAAactB_is_inpBoroutB 1);
+by (assume_tac 1);
+by (assume_tac 1);
by (eres_inst_tac [("x","a")] allE 1);
by (Asm_full_simp_tac 1);
by (eres_inst_tac [("x","aa")] allE 1);
by (eres_inst_tac [("x","b")] allE 1);
-be exE 1;
-be exE 1;
+by (etac exE 1);
+by (etac exE 1);
by (res_inst_tac [("x","(s2,s2a)")] exI 1);
by (asm_full_simp_tac (simpset() addsimps [inp_is_act]) 1);
(* a~: act B*)
@@ -195,7 +195,7 @@
by (eres_inst_tac [("x","a")] allE 1);
by (Asm_full_simp_tac 1);
by (eres_inst_tac [("x","aa")] allE 1);
-be exE 1;
+by (etac exE 1);
by (res_inst_tac [("x","(s2,b)")] exI 1);
by (Asm_full_simp_tac 1);
@@ -206,17 +206,17 @@
by (eres_inst_tac [("x","a")] allE 1);
by (asm_full_simp_tac (simpset() addsimps [inp_is_act]) 1);
by (forw_inst_tac [("A2","A")] (compat_commute RS iffD1) 1);
-bd inpAAactB_is_inpBoroutB 1;
+by (dtac inpAAactB_is_inpBoroutB 1);
back();
-ba 1;
-ba 1;
+by (assume_tac 1);
+by (assume_tac 1);
by (Asm_full_simp_tac 1);
by (rotate_tac ~1 1);
by (Asm_full_simp_tac 1);
by (eres_inst_tac [("x","aa")] allE 1);
by (eres_inst_tac [("x","b")] allE 1);
-be exE 1;
-be exE 1;
+by (etac exE 1);
+by (etac exE 1);
by (res_inst_tac [("x","(s2,s2a)")] exI 1);
by (asm_full_simp_tac (simpset() addsimps [inp_is_act]) 1);
(* a~: act B*)
@@ -226,7 +226,7 @@
by (eres_inst_tac [("x","a")] allE 1);
by (Asm_full_simp_tac 1);
by (eres_inst_tac [("x","b")] allE 1);
-be exE 1;
+by (etac exE 1);
by (res_inst_tac [("x","(aa,s2)")] exI 1);
by (Asm_full_simp_tac 1);
qed"input_enabled_par";
@@ -289,7 +289,7 @@
by (simp_tac (simpset() addsimps [actions_def,asig_internals_def,
asig_outputs_def,asig_inputs_def,externals_def,asig_of_def,restrict_def,
restrict_asig_def]) 1);
-auto();
+by (Auto_tac());
qed"acts_restrict";
goal thy "starts_of(restrict ioa acts) = starts_of(ioa) & \
@@ -417,7 +417,7 @@
by (asm_full_simp_tac (simpset() addsimps [actions_def,trans_of_def,
asig_internals_def,asig_outputs_def,asig_inputs_def,externals_def,
asig_of_def,rename_def,rename_set_def]) 1);
-auto();
+by (Auto_tac());
qed"is_trans_of_rename";
goal thy "!! A. [| is_asig_of A; is_asig_of B; compatible A B|] \
@@ -426,7 +426,7 @@
asig_comp_def,compatible_def,asig_internals_def,asig_outputs_def,
asig_inputs_def,actions_def,is_asig_def]) 1);
by (asm_full_simp_tac (simpset() addsimps [asig_of_def]) 1);
-auto();
+by (Auto_tac());
by (REPEAT (best_tac (set_cs addEs [equalityCE]) 1));
qed"is_asig_of_par";
@@ -434,7 +434,7 @@
asig_internals_def,asig_outputs_def,asig_inputs_def,externals_def,o_def]
"!! A. is_asig_of A ==> is_asig_of (restrict A f)";
by (Asm_full_simp_tac 1);
-auto();
+by (Auto_tac());
by (REPEAT (best_tac (set_cs addEs [equalityCE]) 1));
qed"is_asig_of_restrict";
@@ -442,7 +442,7 @@
by (asm_full_simp_tac (simpset() addsimps [is_asig_of_def,
rename_def,rename_set_def,asig_internals_def,asig_outputs_def,
asig_inputs_def,actions_def,is_asig_def,asig_of_def]) 1);
-auto();
+by (Auto_tac());
by (dres_inst_tac [("s","Some xb")] sym 1);
by (rotate_tac ~1 1);
by (Asm_full_simp_tac 1);
@@ -466,7 +466,7 @@
"!! A. [|compatible A B; compatible A C |]==> compatible A (B||C)";
by (asm_full_simp_tac (simpset() addsimps [internals_of_par,
outputs_of_par,actions_of_par]) 1);
-auto();
+by (Auto_tac());
by (REPEAT (best_tac (set_cs addEs [equalityCE]) 1));
qed"compatible_par";
@@ -475,7 +475,7 @@
"!! A. [|compatible A C; compatible B C |]==> compatible (A||B) C";
by (asm_full_simp_tac (simpset() addsimps [internals_of_par,
outputs_of_par,actions_of_par]) 1);
-auto();
+by (Auto_tac());
by (REPEAT (best_tac (set_cs addEs [equalityCE]) 1));
qed"compatible_par2";
--- a/src/HOLCF/IOA/meta_theory/CompoExecs.ML Tue Dec 16 15:17:26 1997 +0100
+++ b/src/HOLCF/IOA/meta_theory/CompoExecs.ML Tue Dec 16 17:58:03 1997 +0100
@@ -108,7 +108,7 @@
goal thy "(stutter2 sig`(at>>xs)) s = \
\ ((if (fst at)~:actions sig then Def (s=snd at) else TT) \
\ andalso (stutter2 sig`xs) (snd at))";
-br trans 1;
+by (rtac trans 1);
by (stac stutter2_unfold 1);
by (asm_full_simp_tac (simpset() addsimps [Cons_def,flift1_def,If_and_if]) 1);
by (Simp_tac 1);
@@ -268,7 +268,7 @@
"Execs (A||B) = par_execs (Execs A) (Execs B)";
by (asm_full_simp_tac (simpset() addsimps [asig_of_par]) 1);
-br set_ext 1;
+by (rtac set_ext 1);
by (asm_full_simp_tac (simpset() addsimps [compositionality_ex,actions_of_par]) 1);
qed"compositionality_ex_modules";
--- a/src/HOLCF/IOA/meta_theory/CompoScheds.ML Tue Dec 16 15:17:26 1997 +0100
+++ b/src/HOLCF/IOA/meta_theory/CompoScheds.ML Tue Dec 16 17:58:03 1997 +0100
@@ -517,7 +517,7 @@
"Scheds (A||B) = par_scheds (Scheds A) (Scheds B)";
by (asm_full_simp_tac (simpset() addsimps [asig_of_par]) 1);
-br set_ext 1;
+by (rtac set_ext 1);
by (asm_full_simp_tac (simpset() addsimps [compositionality_sch,actions_of_par]) 1);
qed"compositionality_sch_modules";
--- a/src/HOLCF/IOA/meta_theory/CompoTraces.ML Tue Dec 16 15:17:26 1997 +0100
+++ b/src/HOLCF/IOA/meta_theory/CompoTraces.ML Tue Dec 16 17:58:03 1997 +0100
@@ -1239,7 +1239,7 @@
\==> Traces (A||B) = par_traces (Traces A) (Traces B)";
by (asm_full_simp_tac (simpset() addsimps [asig_of_par]) 1);
-br set_ext 1;
+by (rtac set_ext 1);
by (asm_full_simp_tac (simpset() addsimps [compositionality_tr,externals_of_par]) 1);
qed"compositionality_tr_modules";
--- a/src/HOLCF/IOA/meta_theory/RefMappings.ML Tue Dec 16 15:17:26 1997 +0100
+++ b/src/HOLCF/IOA/meta_theory/RefMappings.ML Tue Dec 16 17:58:03 1997 +0100
@@ -92,7 +92,7 @@
val prems = goal HOL.thy "(P ==> Q-->R) ==> P&Q --> R";
- by(fast_tac (claset() addDs prems) 1);
+ by (fast_tac (claset() addDs prems) 1);
val lemma = result();
@@ -108,7 +108,7 @@
by (simp_tac (simpset() addsimps [rename_def,rename_set_def]) 1);
by (asm_full_simp_tac (simpset() addsimps [externals_def,asig_inputs_def,
asig_outputs_def,asig_of_def,trans_of_def]) 1);
-by (safe_tac (claset()));
+by Safe_tac;
by (stac expand_if 1);
by (rtac conjI 1);
by (rtac impI 1);
--- a/src/HOLCF/IOA/meta_theory/Traces.ML Tue Dec 16 15:17:26 1997 +0100
+++ b/src/HOLCF/IOA/meta_theory/Traces.ML Tue Dec 16 17:58:03 1997 +0100
@@ -197,7 +197,7 @@
"!! A.[| x:traces A |] ==> \
\ Forall (%a. a:act A) x";
by (safe_tac set_cs );
-br ForallQFilterP 1;
+by (rtac ForallQFilterP 1);
by (fast_tac (!claset addSIs [ext_is_act]) 1);
qed"traces_in_sig";
*)
--- a/src/HOLCF/Porder0.ML Tue Dec 16 15:17:26 1997 +0100
+++ b/src/HOLCF/Porder0.ML Tue Dec 16 17:58:03 1997 +0100
@@ -48,5 +48,5 @@
]);
goal Porder0.thy "((x::'a::po)=y) = (x << y & y << x)";
-by(fast_tac (HOL_cs addSEs [antisym_less_inverse] addSIs [antisym_less]) 1);
+by (fast_tac (HOL_cs addSEs [antisym_less_inverse] addSIs [antisym_less]) 1);
qed "po_eq_conv";
--- a/src/HOLCF/Tr.ML Tue Dec 16 15:17:26 1997 +0100
+++ b/src/HOLCF/Tr.ML Tue Dec 16 17:58:03 1997 +0100
@@ -115,17 +115,17 @@
"!!t.[|t~=UU|]==> ((t andalso s)=FF)=(t=FF | s=FF)";
by (rtac iffI 1);
by (res_inst_tac [("p","t")] trE 1);
-auto();
+by (Auto_tac());
by (res_inst_tac [("p","t")] trE 1);
-auto();
+by (Auto_tac());
qed"andalso_or";
goal thy "!!t.[|t~=UU|]==> ((t andalso s)~=FF)=(t~=FF & s~=FF)";
by (rtac iffI 1);
by (res_inst_tac [("p","t")] trE 1);
-auto();
+by (Auto_tac());
by (res_inst_tac [("p","t")] trE 1);
-auto();
+by (Auto_tac());
qed"andalso_and";
goal thy "(Def x ~=FF)= x";
--- a/src/HOLCF/ex/Dnat.ML Tue Dec 16 15:17:26 1997 +0100
+++ b/src/HOLCF/ex/Dnat.ML Tue Dec 16 17:58:03 1997 +0100
@@ -22,14 +22,14 @@
qed_goal "iterator1" Dnat.thy "iterator`UU`f`x = UU"
(fn prems =>
[
- (rtac (iterator_def2 RS ssubst) 1),
+ (stac iterator_def2 1),
(simp_tac (HOLCF_ss addsimps dnat.rews) 1)
]);
qed_goal "iterator2" Dnat.thy "iterator`dzero`f`x = x"
(fn prems =>
[
- (rtac (iterator_def2 RS ssubst) 1),
+ (stac iterator_def2 1),
(simp_tac (HOLCF_ss addsimps dnat.rews) 1)
]);
@@ -39,7 +39,7 @@
[
(cut_facts_tac prems 1),
(rtac trans 1),
- (rtac (iterator_def2 RS ssubst) 1),
+ (stac iterator_def2 1),
(asm_simp_tac (HOLCF_ss addsimps dnat.rews) 1),
(rtac refl 1)
]);
--- a/src/LCF/ex/ex.ML Tue Dec 16 15:17:26 1997 +0100
+++ b/src/LCF/ex/ex.ML Tue Dec 16 17:58:03 1997 +0100
@@ -40,12 +40,12 @@
val ex_ss = ex_ss addsimps [H_strict];
goal ex_thy "ALL x. H(FIX(K,x)) = FIX(K,x)";
-by(induct_tac "K" 1);
-by(simp_tac ex_ss 1);
-by(simp_tac (ex_ss setloop (split_tac [COND_cases_iff])) 1);
-by(strip_tac 1);
-by(stac H_unfold 1);
-by(asm_simp_tac ex_ss 1);
+by (induct_tac "K" 1);
+by (simp_tac ex_ss 1);
+by (simp_tac (ex_ss setloop (split_tac [COND_cases_iff])) 1);
+by (strip_tac 1);
+by (stac H_unfold 1);
+by (asm_simp_tac ex_ss 1);
val H_idemp_lemma = topthm();
val H_idemp = rewrite_rule [mk_meta_eq (H RS sym)] H_idemp_lemma;
@@ -76,10 +76,10 @@
val ex_ss = LCF_ss addsimps [F_strict,K];
goal ex_thy "ALL x. F(H(x::'a,y::'b)) = H(x,F(y))";
-by(stac H 1);
-by(induct_tac "K::('a=>'b=>'b)=>('a=>'b=>'b)" 1);
-by(simp_tac ex_ss 1);
-by(asm_simp_tac (ex_ss setloop (split_tac [COND_cases_iff])) 1);
+by (stac H 1);
+by (induct_tac "K::('a=>'b=>'b)=>('a=>'b=>'b)" 1);
+by (simp_tac ex_ss 1);
+by (asm_simp_tac (ex_ss setloop (split_tac [COND_cases_iff])) 1);
result();
@@ -103,20 +103,20 @@
val ex_ss = LCF_ss addsimps [p_strict,p_s];
goal ex_thy "p(FIX(s),y) = FIX(s)";
-by(induct_tac "s" 1);
-by(simp_tac ex_ss 1);
-by(simp_tac ex_ss 1);
+by (induct_tac "s" 1);
+by (simp_tac ex_ss 1);
+by (simp_tac ex_ss 1);
result();
(*** Prefixpoints ***)
val asms = goal thy "[| f(p) << p; !!q. f(q) << q ==> p << q |] ==> FIX(f)=p";
-by(rewtac eq_def);
+by (rewtac eq_def);
by (rtac conjI 1);
-by(induct_tac "f" 1);
+by (induct_tac "f" 1);
by (rtac minimal 1);
-by(strip_tac 1);
+by (strip_tac 1);
by (rtac less_trans 1);
by (resolve_tac asms 2);
by (etac less_ap_term 1);