# HG changeset patch # User wenzelm # Date 882291483 -3600 # Node ID a129b817b58a8b7a8af6cafe8675c754e8b34987 # Parent 21238c9d363e7a938e10216ca79c42e14eda7f0b expandshort; diff -r 21238c9d363e -r a129b817b58a src/CCL/CCL.ML --- 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= & t'= & 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. : 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"; diff -r 21238c9d363e -r a129b817b58a src/CCL/Hered.ML --- 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 : 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"; diff -r 21238c9d363e -r a129b817b58a src/FOL/ex/Nat2.ML --- 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"; diff -r 21238c9d363e -r a129b817b58a src/HOL/Arith.ML --- 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-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*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"; diff -r 21238c9d363e -r a129b817b58a src/HOL/Auth/Shared.ML --- 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]; diff -r 21238c9d363e -r a129b817b58a src/HOL/Auth/TLS.ML --- 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(); diff -r 21238c9d363e -r a129b817b58a src/HOL/Divides.ML --- 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*(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"; diff -r 21238c9d363e -r a129b817b58a src/HOL/Finite.ML --- 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"; diff -r 21238c9d363e -r a129b817b58a src/HOL/Integ/Group.ML --- 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 = diff -r 21238c9d363e -r a129b817b58a src/HOL/Integ/IntRingDefs.ML --- 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"; diff -r 21238c9d363e -r a129b817b58a src/HOL/Integ/Ring.ML --- 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, diff -r 21238c9d363e -r a129b817b58a src/HOL/Lex/Prefix.ML --- 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]; diff -r 21238c9d363e -r a129b817b58a src/HOL/Lex/Regset_of_auto.ML --- 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"; diff -r 21238c9d363e -r a129b817b58a src/HOL/List.ML --- 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]; diff -r 21238c9d363e -r a129b817b58a src/HOL/Map.ML --- 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]; diff -r 21238c9d363e -r a129b817b58a src/HOL/MiniML/Maybe.ML --- 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"; diff -r 21238c9d363e -r a129b817b58a src/HOL/MiniML/W.ML --- 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); diff -r 21238c9d363e -r a129b817b58a src/HOL/NatDef.ML --- 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]; diff -r 21238c9d363e -r a129b817b58a src/HOL/Prod.ML --- 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); diff -r 21238c9d363e -r a129b817b58a src/HOL/Relation.ML --- 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 **) diff -r 21238c9d363e -r a129b817b58a src/HOL/Set.ML --- 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]; diff -r 21238c9d363e -r a129b817b58a src/HOL/TLA/TLA.ML --- 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 **) diff -r 21238c9d363e -r a129b817b58a src/HOL/equalities.ML --- 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]; diff -r 21238c9d363e -r a129b817b58a src/HOL/ex/Qsort.ML --- 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]; diff -r 21238c9d363e -r a129b817b58a src/HOL/ex/Recdef.ML --- 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: *) diff -r 21238c9d363e -r a129b817b58a src/HOLCF/Cfun3.ML --- 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 ]); diff -r 21238c9d363e -r a129b817b58a src/HOLCF/Discrete.ML --- 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]; diff -r 21238c9d363e -r a129b817b58a src/HOLCF/Fix.ML --- 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); diff -r 21238c9d363e -r a129b817b58a src/HOLCF/IMP/HoareEx.ML --- 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"; diff -r 21238c9d363e -r a129b817b58a src/HOLCF/IOA/ABP/Correctness.ML --- 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); diff -r 21238c9d363e -r a129b817b58a src/HOLCF/IOA/ABP/Lemmas.ML --- 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(); diff -r 21238c9d363e -r a129b817b58a src/HOLCF/IOA/ABP/ROOT.ML --- 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; diff -r 21238c9d363e -r a129b817b58a src/HOLCF/IOA/NTP/Abschannel.ML --- 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"; diff -r 21238c9d363e -r a129b817b58a src/HOLCF/IOA/NTP/Impl.ML --- 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); diff -r 21238c9d363e -r a129b817b58a src/HOLCF/IOA/NTP/Lemmas.ML --- 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-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"; diff -r 21238c9d363e -r a129b817b58a src/HOLCF/IOA/NTP/Multiset.ML --- 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"; diff -r 21238c9d363e -r a129b817b58a src/HOLCF/IOA/NTP/ROOT.ML --- 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; diff -r 21238c9d363e -r a129b817b58a src/HOLCF/IOA/NTP/Receiver.ML --- 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"; diff -r 21238c9d363e -r a129b817b58a src/HOLCF/IOA/NTP/Sender.ML --- 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"; diff -r 21238c9d363e -r a129b817b58a src/HOLCF/IOA/meta_theory/Automata.ML --- 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"; diff -r 21238c9d363e -r a129b817b58a src/HOLCF/IOA/meta_theory/CompoExecs.ML --- 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"; diff -r 21238c9d363e -r a129b817b58a src/HOLCF/IOA/meta_theory/CompoScheds.ML --- 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"; diff -r 21238c9d363e -r a129b817b58a src/HOLCF/IOA/meta_theory/CompoTraces.ML --- 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"; diff -r 21238c9d363e -r a129b817b58a src/HOLCF/IOA/meta_theory/RefMappings.ML --- 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); diff -r 21238c9d363e -r a129b817b58a src/HOLCF/IOA/meta_theory/Traces.ML --- 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"; *) diff -r 21238c9d363e -r a129b817b58a src/HOLCF/Porder0.ML --- 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"; diff -r 21238c9d363e -r a129b817b58a src/HOLCF/Tr.ML --- 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"; diff -r 21238c9d363e -r a129b817b58a src/HOLCF/ex/Dnat.ML --- 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) ]); diff -r 21238c9d363e -r a129b817b58a src/LCF/ex/ex.ML --- 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);