# HG changeset patch # User wenzelm # Date 1283793190 -7200 # Node ID 0dec18004e75ae558da3f8b0c798dce622d7ddbc # Parent e6b96b4cde7e41f2a851d3bd2a22924732aa90b9 more antiquotations; diff -r e6b96b4cde7e -r 0dec18004e75 src/CCL/CCL.thy --- a/src/CCL/CCL.thy Mon Sep 06 19:11:01 2010 +0200 +++ b/src/CCL/CCL.thy Mon Sep 06 19:13:10 2010 +0200 @@ -238,9 +238,9 @@ fun mk_thm_str thy a b = "~ " ^ (saturate thy a "a") ^ " = " ^ (saturate thy b "b") - val lemma = thm "lem"; - val eq_lemma = thm "eq_lemma"; - val distinctness = thm "distinctness"; + val lemma = @{thm lem}; + val eq_lemma = @{thm eq_lemma}; + val distinctness = @{thm distinctness}; fun mk_lemma (ra,rb) = [lemma] RL [ra RS (rb RS eq_lemma)] RL [distinctness RS notE, @{thm sym} RS (distinctness RS notE)] in diff -r e6b96b4cde7e -r 0dec18004e75 src/CCL/Type.thy --- a/src/CCL/Type.thy Mon Sep 06 19:11:01 2010 +0200 +++ b/src/CCL/Type.thy Mon Sep 06 19:13:10 2010 +0200 @@ -99,7 +99,7 @@ unfolding simp_type_defs by blast+ ML {* -bind_thms ("case_rls", XH_to_Es (thms "XHs")); +bind_thms ("case_rls", XH_to_Es @{thms XHs}); *} @@ -260,7 +260,7 @@ lemmas iXHs = NatXH ListXH -ML {* bind_thms ("icase_rls", XH_to_Es (thms "iXHs")) *} +ML {* bind_thms ("icase_rls", XH_to_Es @{thms iXHs}) *} subsection {* Type Rules *} diff -r e6b96b4cde7e -r 0dec18004e75 src/CCL/ex/Stream.thy --- a/src/CCL/ex/Stream.thy Mon Sep 06 19:11:01 2010 +0200 +++ b/src/CCL/ex/Stream.thy Mon Sep 06 19:13:10 2010 +0200 @@ -88,7 +88,7 @@ apply (tactic "EQgen_tac @{context} [] 1") prefer 2 apply blast - apply (tactic {* DEPTH_SOLVE (etac (XH_to_E (thm "ListsXH")) 1 + apply (tactic {* DEPTH_SOLVE (etac (XH_to_E @{thm ListsXH}) 1 THEN EQgen_tac @{context} [] 1) *}) done @@ -135,7 +135,7 @@ apply (tactic {* eq_coinduct3_tac @{context} "{p. EX x y. p= & (EX n:Nat. x=iter1 (f,f^n`a) & y=map (f) ^n`iter2 (f,a))}" 1*}) apply (fast intro!: napplyBzero [symmetric] napplyBzero [symmetric, THEN arg_cong]) - apply (tactic {* EQgen_tac @{context} [thm "iter1B", thm "iter2Blemma"] 1 *}) + apply (tactic {* EQgen_tac @{context} [@{thm iter1B}, @{thm iter2Blemma}] 1 *}) apply (subst napply_f, assumption) apply (rule_tac f1 = f in napplyBsucc [THEN subst]) apply blast diff -r e6b96b4cde7e -r 0dec18004e75 src/CTT/Arith.thy --- a/src/CTT/Arith.thy Mon Sep 06 19:11:01 2010 +0200 +++ b/src/CTT/Arith.thy Mon Sep 06 19:13:10 2010 +0200 @@ -82,12 +82,12 @@ lemma mult_typing: "[| a:N; b:N |] ==> a #* b : N" apply (unfold arith_defs) -apply (tactic {* typechk_tac [thm "add_typing"] *}) +apply (tactic {* typechk_tac [@{thm add_typing}] *}) done lemma mult_typingL: "[| a=c:N; b=d:N |] ==> a #* b = c #* d : N" apply (unfold arith_defs) -apply (tactic {* equal_tac [thm "add_typingL"] *}) +apply (tactic {* equal_tac [@{thm add_typingL}] *}) done (*computation for mult: 0 and successor cases*) @@ -159,19 +159,19 @@ structure Arith_simp_data: TSIMP_DATA = struct - val refl = thm "refl_elem" - val sym = thm "sym_elem" - val trans = thm "trans_elem" - val refl_red = thm "refl_red" - val trans_red = thm "trans_red" - val red_if_equal = thm "red_if_equal" - val default_rls = thms "arithC_rls" @ thms "comp_rls" - val routine_tac = routine_tac (thms "arith_typing_rls" @ thms "routine_rls") + val refl = @{thm refl_elem} + val sym = @{thm sym_elem} + val trans = @{thm trans_elem} + val refl_red = @{thm refl_red} + val trans_red = @{thm trans_red} + val red_if_equal = @{thm red_if_equal} + val default_rls = @{thms arithC_rls} @ @{thms comp_rls} + val routine_tac = routine_tac (@{thms arith_typing_rls} @ @{thms routine_rls}) end structure Arith_simp = TSimpFun (Arith_simp_data) -local val congr_rls = thms "congr_rls" in +local val congr_rls = @{thms congr_rls} in fun arith_rew_tac prems = make_rew_tac (Arith_simp.norm_tac(congr_rls, prems)) @@ -271,7 +271,7 @@ (*Solves first 0 goal, simplifies others. Two sugbgoals remain. Both follow by rewriting, (2) using quantified induction hyp*) apply (tactic "intr_tac []") (*strips remaining PRODs*) -apply (tactic {* hyp_arith_rew_tac [thm "add_0_right"] *}) +apply (tactic {* hyp_arith_rew_tac [@{thm add_0_right}] *}) apply assumption done @@ -303,7 +303,7 @@ lemma absdiff_self_eq_0: "a:N ==> a |-| a = 0 : N" apply (unfold absdiff_def) -apply (tactic {* arith_rew_tac [thm "diff_self_eq_0"] *}) +apply (tactic {* arith_rew_tac [@{thm diff_self_eq_0}] *}) done lemma absdiffC0: "a:N ==> 0 |-| a = a : N" @@ -321,7 +321,7 @@ lemma absdiff_commute: "[| a:N; b:N |] ==> a |-| b = b |-| a : N" apply (unfold absdiff_def) apply (rule add_commute) -apply (tactic {* typechk_tac [thm "diff_typing"] *}) +apply (tactic {* typechk_tac [@{thm diff_typing}] *}) done (*If a+b=0 then a=0. Surprisingly tedious*) @@ -332,7 +332,7 @@ apply (tactic "intr_tac []") (*strips remaining PRODs*) apply (rule_tac [2] zero_ne_succ [THEN FE]) apply (erule_tac [3] EqE [THEN sym_elem]) -apply (tactic {* typechk_tac [thm "add_typing"] *}) +apply (tactic {* typechk_tac [@{thm add_typing}] *}) done (*Version of above with the premise a+b=0. @@ -354,7 +354,7 @@ apply (rule_tac [2] add_eq0) apply (rule add_eq0) apply (rule_tac [6] add_commute [THEN trans_elem]) -apply (tactic {* typechk_tac [thm "diff_typing"] *}) +apply (tactic {* typechk_tac [@{thm diff_typing}] *}) done (*if a |-| b = 0 then a = b @@ -366,7 +366,7 @@ apply (tactic eqintr_tac) apply (rule add_diff_inverse [THEN sym_elem, THEN trans_elem]) apply (rule_tac [3] EqE, tactic "assume_tac 3") -apply (tactic {* hyp_arith_rew_tac [thm "add_0_right"] *}) +apply (tactic {* hyp_arith_rew_tac [@{thm add_0_right}] *}) done @@ -376,12 +376,12 @@ lemma mod_typing: "[| a:N; b:N |] ==> a mod b : N" apply (unfold mod_def) -apply (tactic {* typechk_tac [thm "absdiff_typing"] *}) +apply (tactic {* typechk_tac [@{thm absdiff_typing}] *}) done lemma mod_typingL: "[| a=c:N; b=d:N |] ==> a mod b = c mod d : N" apply (unfold mod_def) -apply (tactic {* equal_tac [thm "absdiff_typingL"] *}) +apply (tactic {* equal_tac [@{thm absdiff_typingL}] *}) done @@ -389,13 +389,13 @@ lemma modC0: "b:N ==> 0 mod b = 0 : N" apply (unfold mod_def) -apply (tactic {* rew_tac [thm "absdiff_typing"] *}) +apply (tactic {* rew_tac [@{thm absdiff_typing}] *}) done lemma modC_succ: "[| a:N; b:N |] ==> succ(a) mod b = rec(succ(a mod b) |-| b, 0, %x y. succ(a mod b)) : N" apply (unfold mod_def) -apply (tactic {* rew_tac [thm "absdiff_typing"] *}) +apply (tactic {* rew_tac [@{thm absdiff_typing}] *}) done @@ -403,12 +403,12 @@ lemma div_typing: "[| a:N; b:N |] ==> a div b : N" apply (unfold div_def) -apply (tactic {* typechk_tac [thm "absdiff_typing", thm "mod_typing"] *}) +apply (tactic {* typechk_tac [@{thm absdiff_typing}, @{thm mod_typing}] *}) done lemma div_typingL: "[| a=c:N; b=d:N |] ==> a div b = c div d : N" apply (unfold div_def) -apply (tactic {* equal_tac [thm "absdiff_typingL", thm "mod_typingL"] *}) +apply (tactic {* equal_tac [@{thm absdiff_typingL}, @{thm mod_typingL}] *}) done lemmas div_typing_rls = mod_typing div_typing absdiff_typing @@ -418,14 +418,14 @@ lemma divC0: "b:N ==> 0 div b = 0 : N" apply (unfold div_def) -apply (tactic {* rew_tac [thm "mod_typing", thm "absdiff_typing"] *}) +apply (tactic {* rew_tac [@{thm mod_typing}, @{thm absdiff_typing}] *}) done lemma divC_succ: "[| a:N; b:N |] ==> succ(a) div b = rec(succ(a) mod b, succ(a div b), %x y. a div b) : N" apply (unfold div_def) -apply (tactic {* rew_tac [thm "mod_typing"] *}) +apply (tactic {* rew_tac [@{thm mod_typing}] *}) done @@ -433,9 +433,9 @@ lemma divC_succ2: "[| a:N; b:N |] ==> succ(a) div b =rec(succ(a mod b) |-| b, succ(a div b), %x y. a div b) : N" apply (rule divC_succ [THEN trans_elem]) -apply (tactic {* rew_tac (thms "div_typing_rls" @ [thm "modC_succ"]) *}) +apply (tactic {* rew_tac (@{thms div_typing_rls} @ [@{thm modC_succ}]) *}) apply (tactic {* NE_tac @{context} "succ (a mod b) |-|b" 1 *}) -apply (tactic {* rew_tac [thm "mod_typing", thm "div_typing", thm "absdiff_typing"] *}) +apply (tactic {* rew_tac [@{thm mod_typing}, @{thm div_typing}, @{thm absdiff_typing}] *}) done (*for case analysis on whether a number is 0 or a successor*) @@ -451,19 +451,19 @@ (*Main Result. Holds when b is 0 since a mod 0 = a and a div 0 = 0 *) lemma mod_div_equality: "[| a:N; b:N |] ==> a mod b #+ (a div b) #* b = a : N" apply (tactic {* NE_tac @{context} "a" 1 *}) -apply (tactic {* arith_rew_tac (thms "div_typing_rls" @ - [thm "modC0", thm "modC_succ", thm "divC0", thm "divC_succ2"]) *}) +apply (tactic {* arith_rew_tac (@{thms div_typing_rls} @ + [@{thm modC0}, @{thm modC_succ}, @{thm divC0}, @{thm divC_succ2}]) *}) apply (rule EqE) (*case analysis on succ(u mod b)|-|b *) apply (rule_tac a1 = "succ (u mod b) |-| b" in iszero_decidable [THEN PlusE]) apply (erule_tac [3] SumE) -apply (tactic {* hyp_arith_rew_tac (thms "div_typing_rls" @ - [thm "modC0", thm "modC_succ", thm "divC0", thm "divC_succ2"]) *}) +apply (tactic {* hyp_arith_rew_tac (@{thms div_typing_rls} @ + [@{thm modC0}, @{thm modC_succ}, @{thm divC0}, @{thm divC_succ2}]) *}) (*Replace one occurence of b by succ(u mod b). Clumsy!*) apply (rule add_typingL [THEN trans_elem]) apply (erule EqE [THEN absdiff_eq0, THEN sym_elem]) apply (rule_tac [3] refl_elem) -apply (tactic {* hyp_arith_rew_tac (thms "div_typing_rls") *}) +apply (tactic {* hyp_arith_rew_tac @{thms div_typing_rls} *}) done end diff -r e6b96b4cde7e -r 0dec18004e75 src/CTT/ex/Elimination.thy --- a/src/CTT/ex/Elimination.thy Mon Sep 06 19:11:01 2010 +0200 +++ b/src/CTT/ex/Elimination.thy Mon Sep 06 19:13:10 2010 +0200 @@ -53,7 +53,7 @@ and "!!x. x:A ==> B(x) type" and "!!x. x:A ==> C(x) type" shows "?a : (SUM x:A. B(x) + C(x)) --> (SUM x:A. B(x)) + (SUM x:A. C(x))" -apply (tactic {* pc_tac (thms "prems") 1 *}) +apply (tactic {* pc_tac @{thms assms} 1 *}) done text "Construction of the currying functional" @@ -68,7 +68,7 @@ and "!!z. z: (SUM x:A. B(x)) ==> C(z) type" shows "?a : PROD f: (PROD z : (SUM x:A . B(x)) . C(z)). (PROD x:A . PROD y:B(x) . C())" -apply (tactic {* pc_tac (thms "prems") 1 *}) +apply (tactic {* pc_tac @{thms assms} 1 *}) done text "Martin-Lof (1984), page 48: axiom of sum-elimination (uncurry)" @@ -83,7 +83,7 @@ and "!!z. z: (SUM x:A . B(x)) ==> C(z) type" shows "?a : (PROD x:A . PROD y:B(x) . C()) --> (PROD z : (SUM x:A . B(x)) . C(z))" -apply (tactic {* pc_tac (thms "prems") 1 *}) +apply (tactic {* pc_tac @{thms assms} 1 *}) done text "Function application" @@ -99,7 +99,7 @@ shows "?a : (SUM y:B . PROD x:A . C(x,y)) --> (PROD x:A . SUM y:B . C(x,y))" -apply (tactic {* pc_tac (thms "prems") 1 *}) +apply (tactic {* pc_tac @{thms assms} 1 *}) done text "Martin-Lof (1984) pages 36-7: the combinator S" @@ -109,7 +109,7 @@ and "!!x y.[| x:A; y:B(x) |] ==> C(x,y) type" shows "?a : (PROD x:A. PROD y:B(x). C(x,y)) --> (PROD f: (PROD x:A. B(x)). PROD x:A. C(x, f`x))" -apply (tactic {* pc_tac (thms "prems") 1 *}) +apply (tactic {* pc_tac @{thms assms} 1 *}) done text "Martin-Lof (1984) page 58: the axiom of disjunction elimination" @@ -119,7 +119,7 @@ and "!!z. z: A+B ==> C(z) type" shows "?a : (PROD x:A. C(inl(x))) --> (PROD y:B. C(inr(y))) --> (PROD z: A+B. C(z))" -apply (tactic {* pc_tac (thms "prems") 1 *}) +apply (tactic {* pc_tac @{thms assms} 1 *}) done (*towards AXIOM OF CHOICE*) @@ -137,7 +137,7 @@ and "!!x y.[| x:A; y:B(x) |] ==> C(x,y) type" shows "?a : PROD h: (PROD x:A. SUM y:B(x). C(x,y)). (SUM f: (PROD x:A. B(x)). PROD x:A. C(x, f`x))" -apply (tactic {* intr_tac (thms "prems") *}) +apply (tactic {* intr_tac @{thms assms} *}) apply (tactic "add_mp_tac 2") apply (tactic "add_mp_tac 1") apply (erule SumE_fst) @@ -145,7 +145,7 @@ apply (rule subst_eqtyparg) apply (rule comp_rls) apply (rule_tac [4] SumE_snd) -apply (tactic {* typechk_tac (thm "SumE_fst" :: thms "prems") *}) +apply (tactic {* typechk_tac (@{thm SumE_fst} :: @{thms prems}) *}) done text "Axiom of choice. Proof without fst, snd. Harder still!" @@ -155,7 +155,7 @@ and "!!x y.[| x:A; y:B(x) |] ==> C(x,y) type" shows "?a : PROD h: (PROD x:A. SUM y:B(x). C(x,y)). (SUM f: (PROD x:A. B(x)). PROD x:A. C(x, f`x))" -apply (tactic {* intr_tac (thms "prems") *}) +apply (tactic {* intr_tac @{thms assms} *}) (*Must not use add_mp_tac as subst_prodE hides the construction.*) apply (rule ProdE [THEN SumE], assumption) apply (tactic "TRYALL assume_tac") @@ -163,11 +163,11 @@ apply (rule subst_eqtyparg) apply (rule comp_rls) apply (erule_tac [4] ProdE [THEN SumE]) -apply (tactic {* typechk_tac (thms "prems") *}) +apply (tactic {* typechk_tac @{thms assms} *}) apply (rule replace_type) apply (rule subst_eqtyparg) apply (rule comp_rls) -apply (tactic {* typechk_tac (thms "prems") *}) +apply (tactic {* typechk_tac @{thms assms} *}) apply assumption done @@ -183,11 +183,11 @@ apply (tactic {* biresolve_tac safe_brls 2 *}) (*Now must convert assumption C(z) into antecedent C() *) apply (rule_tac [2] a = "y" in ProdE) -apply (tactic {* typechk_tac (thms "prems") *}) +apply (tactic {* typechk_tac @{thms assms} *}) apply (rule SumE, assumption) apply (tactic "intr_tac []") apply (tactic "TRYALL assume_tac") -apply (tactic {* typechk_tac (thms "prems") *}) +apply (tactic {* typechk_tac @{thms assms} *}) done end diff -r e6b96b4cde7e -r 0dec18004e75 src/CTT/ex/Typechecking.thy --- a/src/CTT/ex/Typechecking.thy Mon Sep 06 19:11:01 2010 +0200 +++ b/src/CTT/ex/Typechecking.thy Mon Sep 06 19:13:10 2010 +0200 @@ -66,7 +66,7 @@ (*Proofs involving arbitrary types. For concreteness, every type variable left over is forced to be N*) -ML {* val N_tac = TRYALL (rtac (thm "NF")) *} +ML {* val N_tac = TRYALL (rtac @{thm NF}) *} schematic_lemma "lam w. : ?A" apply (tactic "typechk_tac []") diff -r e6b96b4cde7e -r 0dec18004e75 src/CTT/rew.ML --- a/src/CTT/rew.ML Mon Sep 06 19:11:01 2010 +0200 +++ b/src/CTT/rew.ML Mon Sep 06 19:13:10 2010 +0200 @@ -8,7 +8,7 @@ (*Make list of ProdE RS ProdE ... RS ProdE RS EqE for using assumptions as rewrite rules*) fun peEs 0 = [] - | peEs n = thm "EqE" :: map (curry (op RS) (thm "ProdE")) (peEs (n-1)); + | peEs n = @{thm EqE} :: map (curry (op RS) @{thm ProdE}) (peEs (n-1)); (*Tactic used for proving conditions for the cond_rls*) val prove_cond_tac = eresolve_tac (peEs 5); @@ -16,19 +16,19 @@ structure TSimp_data: TSIMP_DATA = struct - val refl = thm "refl_elem" - val sym = thm "sym_elem" - val trans = thm "trans_elem" - val refl_red = thm "refl_red" - val trans_red = thm "trans_red" - val red_if_equal = thm "red_if_equal" - val default_rls = thms "comp_rls" - val routine_tac = routine_tac (thms "routine_rls") + val refl = @{thm refl_elem} + val sym = @{thm sym_elem} + val trans = @{thm trans_elem} + val refl_red = @{thm refl_red} + val trans_red = @{thm trans_red} + val red_if_equal = @{thm red_if_equal} + val default_rls = @{thms comp_rls} + val routine_tac = routine_tac (@{thms routine_rls}) end; structure TSimp = TSimpFun (TSimp_data); -val standard_congr_rls = thms "intrL2_rls" @ thms "elimL_rls"; +val standard_congr_rls = @{thms intrL2_rls} @ @{thms elimL_rls}; (*Make a rewriting tactic from a normalization tactic*) fun make_rew_tac ntac = diff -r e6b96b4cde7e -r 0dec18004e75 src/FOL/IFOL.thy --- a/src/FOL/IFOL.thy Mon Sep 06 19:11:01 2010 +0200 +++ b/src/FOL/IFOL.thy Mon Sep 06 19:13:10 2010 +0200 @@ -340,7 +340,7 @@ shows "(P&Q) <-> (P'&Q')" apply (insert assms) apply (assumption | rule iffI conjI | erule iffE conjE mp | - tactic {* iff_tac (thms "assms") 1 *})+ + tactic {* iff_tac @{thms assms} 1 *})+ done (*Reversed congruence rule! Used in ZF/Order*) @@ -350,7 +350,7 @@ shows "(Q&P) <-> (Q'&P')" apply (insert assms) apply (assumption | rule iffI conjI | erule iffE conjE mp | - tactic {* iff_tac (thms "assms") 1 *})+ + tactic {* iff_tac @{thms assms} 1 *})+ done lemma disj_cong: @@ -366,7 +366,7 @@ shows "(P-->Q) <-> (P'-->Q')" apply (insert assms) apply (assumption | rule iffI impI | erule iffE | erule (1) notE impE | - tactic {* iff_tac (thms "assms") 1 *})+ + tactic {* iff_tac @{thms assms} 1 *})+ done lemma iff_cong: "[| P <-> P'; Q <-> Q' |] ==> (P<->Q) <-> (P'<->Q')" @@ -381,21 +381,21 @@ assumes "!!x. P(x) <-> Q(x)" shows "(ALL x. P(x)) <-> (ALL x. Q(x))" apply (assumption | rule iffI allI | erule (1) notE impE | erule allE | - tactic {* iff_tac (thms "assms") 1 *})+ + tactic {* iff_tac @{thms assms} 1 *})+ done lemma ex_cong: assumes "!!x. P(x) <-> Q(x)" shows "(EX x. P(x)) <-> (EX x. Q(x))" apply (erule exE | assumption | rule iffI exI | erule (1) notE impE | - tactic {* iff_tac (thms "assms") 1 *})+ + tactic {* iff_tac @{thms assms} 1 *})+ done lemma ex1_cong: assumes "!!x. P(x) <-> Q(x)" shows "(EX! x. P(x)) <-> (EX! x. Q(x))" apply (erule ex1E spec [THEN mp] | assumption | rule iffI ex1I | erule (1) notE impE | - tactic {* iff_tac (thms "assms") 1 *})+ + tactic {* iff_tac @{thms assms} 1 *})+ done (*** Equality rules ***) diff -r e6b96b4cde7e -r 0dec18004e75 src/FOL/hypsubstdata.ML --- a/src/FOL/hypsubstdata.ML Mon Sep 06 19:11:01 2010 +0200 +++ b/src/FOL/hypsubstdata.ML Mon Sep 06 19:13:10 2010 +0200 @@ -6,13 +6,13 @@ val dest_eq = FOLogic.dest_eq val dest_Trueprop = FOLogic.dest_Trueprop val dest_imp = FOLogic.dest_imp - val eq_reflection = thm "eq_reflection" - val rev_eq_reflection = thm "meta_eq_to_obj_eq" - val imp_intr = thm "impI" - val rev_mp = thm "rev_mp" - val subst = thm "subst" - val sym = thm "sym" - val thin_refl = thm "thin_refl" + val eq_reflection = @{thm eq_reflection} + val rev_eq_reflection = @{thm meta_eq_to_obj_eq} + val imp_intr = @{thm impI} + val rev_mp = @{thm rev_mp} + val subst = @{thm subst} + val sym = @{thm sym} + val thin_refl = @{thm thin_refl} val prop_subst = @{lemma "PROP P(t) ==> PROP prop (x = t ==> PROP P(x))" by (unfold prop_def) (drule eq_reflection, unfold)} end; diff -r e6b96b4cde7e -r 0dec18004e75 src/HOL/Algebra/abstract/Ring2.thy --- a/src/HOL/Algebra/abstract/Ring2.thy Mon Sep 06 19:11:01 2010 +0200 +++ b/src/HOL/Algebra/abstract/Ring2.thy Mon Sep 06 19:13:10 2010 +0200 @@ -211,11 +211,11 @@ fun termless_ring (a, b) = (Term_Ord.term_lpo ring_ord (a, b) = LESS); val ring_ss = HOL_basic_ss settermless termless_ring addsimps - [thm "a_assoc", thm "l_zero", thm "l_neg", thm "a_comm", thm "m_assoc", - thm "l_one", thm "l_distr", thm "m_comm", thm "minus_def", - thm "r_zero", thm "r_neg", thm "r_neg2", thm "r_neg1", thm "minus_add", - thm "minus_minus", thm "minus0", thm "a_lcomm", thm "m_lcomm", (*thm "r_one",*) - thm "r_distr", thm "l_null", thm "r_null", thm "l_minus", thm "r_minus"]; + [@{thm a_assoc}, @{thm l_zero}, @{thm l_neg}, @{thm a_comm}, @{thm m_assoc}, + @{thm l_one}, @{thm l_distr}, @{thm m_comm}, @{thm minus_def}, + @{thm r_zero}, @{thm r_neg}, @{thm r_neg2}, @{thm r_neg1}, @{thm minus_add}, + @{thm minus_minus}, @{thm minus0}, @{thm a_lcomm}, @{thm m_lcomm}, (*@{thm r_one},*) + @{thm r_distr}, @{thm l_null}, @{thm r_null}, @{thm l_minus}, @{thm r_minus}]; *} (* Note: r_one is not necessary in ring_ss *) method_setup ring = diff -r e6b96b4cde7e -r 0dec18004e75 src/HOL/Algebra/poly/LongDiv.thy --- a/src/HOL/Algebra/poly/LongDiv.thy Mon Sep 06 19:11:01 2010 +0200 +++ b/src/HOL/Algebra/poly/LongDiv.thy Mon Sep 06 19:13:10 2010 +0200 @@ -133,8 +133,8 @@ apply (tactic {* simp_tac (@{simpset} addsimps [@{thm l_distr}, @{thm a_assoc}] delsimprocs [ring_simproc]) 1 *}) apply (tactic {* asm_simp_tac (@{simpset} delsimprocs [ring_simproc]) 1 *}) - apply (tactic {* simp_tac (@{simpset} addsimps [thm "minus_def", thm "smult_r_distr", - thm "smult_r_minus", thm "monom_mult_smult", thm "smult_assoc2"] + apply (tactic {* simp_tac (@{simpset} addsimps [@{thm minus_def}, @{thm smult_r_distr}, + @{thm smult_r_minus}, @{thm monom_mult_smult}, @{thm smult_assoc2}] delsimprocs [ring_simproc]) 1 *}) apply (simp add: smult_assoc1 [symmetric]) done @@ -169,7 +169,7 @@ apply (rule conjI) apply (drule sym) apply (tactic {* asm_simp_tac - (@{simpset} addsimps [thm "smult_r_distr" RS sym, thm "smult_assoc2"] + (@{simpset} addsimps [@{thm smult_r_distr} RS sym, @{thm smult_assoc2}] delsimprocs [ring_simproc]) 1 *}) apply (simp (no_asm_simp) add: l_inverse_ring unit_power smult_assoc1 [symmetric]) (* degree property *) @@ -216,21 +216,21 @@ apply (erule disjE) (* r2 = 0 *) apply (tactic {* asm_full_simp_tac (@{simpset} - addsimps [thm "integral_iff", thm "minus_def", thm "l_zero", thm "uminus_zero"] + addsimps [@{thm integral_iff}, @{thm minus_def}, @{thm l_zero}, @{thm uminus_zero}] delsimprocs [ring_simproc]) 1 *}) (* r2 ~= 0 *) apply (drule_tac f = "deg" and y = "r2 - r1" in arg_cong) apply (tactic {* asm_full_simp_tac (@{simpset} addsimps - [thm "minus_def", thm "l_zero", thm "uminus_zero"] delsimprocs [ring_simproc]) 1 *}) + [@{thm minus_def}, @{thm l_zero}, @{thm uminus_zero}] delsimprocs [ring_simproc]) 1 *}) (* r1 ~=0 *) apply (erule disjE) (* r2 = 0 *) apply (drule_tac f = "deg" and y = "r2 - r1" in arg_cong) apply (tactic {* asm_full_simp_tac (@{simpset} addsimps - [thm "minus_def", thm "l_zero", thm "uminus_zero"] delsimprocs [ring_simproc]) 1 *}) + [@{thm minus_def}, @{thm l_zero}, @{thm uminus_zero}] delsimprocs [ring_simproc]) 1 *}) (* r2 ~= 0 *) apply (drule_tac f = "deg" and y = "r2 - r1" in arg_cong) - apply (tactic {* asm_full_simp_tac (@{simpset} addsimps [thm "minus_def"] + apply (tactic {* asm_full_simp_tac (@{simpset} addsimps [@{thm minus_def}] delsimprocs [ring_simproc]) 1 *}) apply (drule order_eq_refl [THEN add_leD2]) apply (drule leD) diff -r e6b96b4cde7e -r 0dec18004e75 src/HOL/Bali/AxCompl.thy --- a/src/HOL/Bali/AxCompl.thy Mon Sep 06 19:11:01 2010 +0200 +++ b/src/HOL/Bali/AxCompl.thy Mon Sep 06 19:13:10 2010 +0200 @@ -1392,7 +1392,7 @@ apply - apply (induct_tac "n") apply (tactic "ALLGOALS (clarsimp_tac @{clasimpset})") -apply (tactic {* dtac (Thm.permute_prems 0 1 (thm "card_seteq")) 1 *}) +apply (tactic {* dtac (Thm.permute_prems 0 1 @{thm card_seteq}) 1 *}) apply simp apply (erule finite_imageI) apply (simp add: MGF_asm ax_derivs_asm) diff -r e6b96b4cde7e -r 0dec18004e75 src/HOL/Bali/AxSem.thy --- a/src/HOL/Bali/AxSem.thy Mon Sep 06 19:11:01 2010 +0200 +++ b/src/HOL/Bali/AxSem.thy Mon Sep 06 19:13:10 2010 +0200 @@ -671,7 +671,7 @@ (* 37 subgoals *) prefer 18 (* Methd *) apply (rule ax_derivs.Methd, drule spec, erule mp, fast) -apply (tactic {* TRYALL (resolve_tac ((funpow 5 tl) (thms "ax_derivs.intros"))) *}) +apply (tactic {* TRYALL (resolve_tac ((funpow 5 tl) @{thms ax_derivs.intros})) *}) apply auto done @@ -691,8 +691,8 @@ apply (erule ax_derivs.induct) (*42 subgoals*) apply (tactic "ALLGOALS strip_tac") -apply (tactic {* ALLGOALS(REPEAT o (EVERY'[dtac (thm "subset_singletonD"), - etac disjE, fast_tac (@{claset} addSIs [thm "ax_derivs.empty"])]))*}) +apply (tactic {* ALLGOALS(REPEAT o (EVERY'[dtac @{thm subset_singletonD}, + etac disjE, fast_tac (@{claset} addSIs @{thms ax_derivs.empty})]))*}) apply (tactic "TRYALL hyp_subst_tac") apply (simp, rule ax_derivs.empty) apply (drule subset_insertD) @@ -702,7 +702,7 @@ apply (fast intro: ax_derivs.weaken) apply (rule ax_derivs.conseq, clarify, tactic "smp_tac 3 1", blast(* unused *)) (*37 subgoals*) -apply (tactic {* TRYALL (resolve_tac ((funpow 5 tl) (thms "ax_derivs.intros")) +apply (tactic {* TRYALL (resolve_tac ((funpow 5 tl) @{thms ax_derivs.intros}) THEN_ALL_NEW fast_tac @{claset}) *}) (*1 subgoal*) apply (clarsimp simp add: subset_mtriples_iff) diff -r e6b96b4cde7e -r 0dec18004e75 src/HOL/Bali/Eval.thy --- a/src/HOL/Bali/Eval.thy Mon Sep 06 19:11:01 2010 +0200 +++ b/src/HOL/Bali/Eval.thy Mon Sep 06 19:13:10 2010 +0200 @@ -1168,7 +1168,7 @@ "G\s \t\\ (w, s') \ (\w' s''. G\s \t\\ (w', s'') \ w' = w \ s'' = s')" apply (erule eval_induct) apply (tactic {* ALLGOALS (EVERY' - [strip_tac, rotate_tac ~1, eresolve_tac (thms "eval_elim_cases")]) *}) + [strip_tac, rotate_tac ~1, eresolve_tac @{thms eval_elim_cases}]) *}) (* 31 subgoals *) prefer 28 (* Try *) apply (simp (no_asm_use) only: split add: split_if_asm) diff -r e6b96b4cde7e -r 0dec18004e75 src/HOL/Bali/Evaln.thy --- a/src/HOL/Bali/Evaln.thy Mon Sep 06 19:11:01 2010 +0200 +++ b/src/HOL/Bali/Evaln.thy Mon Sep 06 19:13:10 2010 +0200 @@ -449,9 +449,9 @@ lemma evaln_nonstrict [rule_format (no_asm), elim]: "G\s \t\\n\ (w, s') \ \m. n\m \ G\s \t\\m\ (w, s')" apply (erule evaln.induct) -apply (tactic {* ALLGOALS (EVERY'[strip_tac, TRY o etac (thm "Suc_le_D_lemma"), +apply (tactic {* ALLGOALS (EVERY'[strip_tac, TRY o etac @{thm Suc_le_D_lemma}, REPEAT o smp_tac 1, - resolve_tac (thms "evaln.intros") THEN_ALL_NEW TRY o atac]) *}) + resolve_tac @{thms evaln.intros} THEN_ALL_NEW TRY o atac]) *}) (* 3 subgoals *) apply (auto split del: split_if) done diff -r e6b96b4cde7e -r 0dec18004e75 src/HOL/Decision_Procs/mir_tac.ML --- a/src/HOL/Decision_Procs/mir_tac.ML Mon Sep 06 19:11:01 2010 +0200 +++ b/src/HOL/Decision_Procs/mir_tac.ML Mon Sep 06 19:13:10 2010 +0200 @@ -16,18 +16,18 @@ fun trace_msg s = if !trace then tracing s else (); val mir_ss = -let val ths = map thm ["real_of_int_inject", "real_of_int_less_iff", "real_of_int_le_iff"] +let val ths = [@{thm "real_of_int_inject"}, @{thm "real_of_int_less_iff"}, @{thm "real_of_int_le_iff"}] in @{simpset} delsimps ths addsimps (map (fn th => th RS sym) ths) end; val nT = HOLogic.natT; - val nat_arith = map thm ["add_nat_number_of", "diff_nat_number_of", - "mult_nat_number_of", "eq_nat_number_of", "less_nat_number_of"]; + val nat_arith = [@{thm "add_nat_number_of"}, @{thm "diff_nat_number_of"}, + @{thm "mult_nat_number_of"}, @{thm "eq_nat_number_of"}, @{thm "less_nat_number_of"}]; - val comp_arith = (map thm ["Let_def", "if_False", "if_True", "add_0", - "add_Suc", "add_number_of_left", "mult_number_of_left", - "Suc_eq_plus1"])@ - (map (fn s => thm s RS sym) ["numeral_1_eq_1", "numeral_0_eq_0"]) + val comp_arith = [@{thm "Let_def"}, @{thm "if_False"}, @{thm "if_True"}, @{thm "add_0"}, + @{thm "add_Suc"}, @{thm "add_number_of_left"}, @{thm "mult_number_of_left"}, + @{thm "Suc_eq_plus1"}] @ + (map (fn th => th RS sym) [@{thm "numeral_1_eq_1"}, @{thm "numeral_0_eq_0"}]) @ @{thms arith_simps} @ nat_arith @ @{thms rel_simps} val ths = [@{thm "mult_numeral_1"}, @{thm "mult_numeral_1_right"}, @{thm "real_of_nat_number_of"}, diff -r e6b96b4cde7e -r 0dec18004e75 src/HOL/HOL.thy --- a/src/HOL/HOL.thy Mon Sep 06 19:11:01 2010 +0200 +++ b/src/HOL/HOL.thy Mon Sep 06 19:13:10 2010 +0200 @@ -2089,47 +2089,47 @@ fun smp_tac j = EVERY'[dresolve_tac (smp j), atac]; end; -val all_conj_distrib = thm "all_conj_distrib"; -val all_simps = thms "all_simps"; -val atomize_not = thm "atomize_not"; -val case_split = thm "case_split"; -val cases_simp = thm "cases_simp"; -val choice_eq = thm "choice_eq" -val cong = thm "cong" -val conj_comms = thms "conj_comms"; -val conj_cong = thm "conj_cong"; -val de_Morgan_conj = thm "de_Morgan_conj"; -val de_Morgan_disj = thm "de_Morgan_disj"; -val disj_assoc = thm "disj_assoc"; -val disj_comms = thms "disj_comms"; -val disj_cong = thm "disj_cong"; -val eq_ac = thms "eq_ac"; -val eq_cong2 = thm "eq_cong2" -val Eq_FalseI = thm "Eq_FalseI"; -val Eq_TrueI = thm "Eq_TrueI"; -val Ex1_def = thm "Ex1_def" -val ex_disj_distrib = thm "ex_disj_distrib"; -val ex_simps = thms "ex_simps"; -val if_cancel = thm "if_cancel"; -val if_eq_cancel = thm "if_eq_cancel"; -val if_False = thm "if_False"; -val iff_conv_conj_imp = thm "iff_conv_conj_imp"; -val iff = thm "iff" -val if_splits = thms "if_splits"; -val if_True = thm "if_True"; -val if_weak_cong = thm "if_weak_cong" -val imp_all = thm "imp_all"; -val imp_cong = thm "imp_cong"; -val imp_conjL = thm "imp_conjL"; -val imp_conjR = thm "imp_conjR"; -val imp_conv_disj = thm "imp_conv_disj"; -val simp_implies_def = thm "simp_implies_def"; -val simp_thms = thms "simp_thms"; -val split_if = thm "split_if"; -val the1_equality = thm "the1_equality" -val theI = thm "theI" -val theI' = thm "theI'" -val True_implies_equals = thm "True_implies_equals"; +val all_conj_distrib = @{thm all_conj_distrib}; +val all_simps = @{thms all_simps}; +val atomize_not = @{thm atomize_not}; +val case_split = @{thm case_split}; +val cases_simp = @{thm cases_simp}; +val choice_eq = @{thm choice_eq}; +val cong = @{thm cong}; +val conj_comms = @{thms conj_comms}; +val conj_cong = @{thm conj_cong}; +val de_Morgan_conj = @{thm de_Morgan_conj}; +val de_Morgan_disj = @{thm de_Morgan_disj}; +val disj_assoc = @{thm disj_assoc}; +val disj_comms = @{thms disj_comms}; +val disj_cong = @{thm disj_cong}; +val eq_ac = @{thms eq_ac}; +val eq_cong2 = @{thm eq_cong2} +val Eq_FalseI = @{thm Eq_FalseI}; +val Eq_TrueI = @{thm Eq_TrueI}; +val Ex1_def = @{thm Ex1_def}; +val ex_disj_distrib = @{thm ex_disj_distrib}; +val ex_simps = @{thms ex_simps}; +val if_cancel = @{thm if_cancel}; +val if_eq_cancel = @{thm if_eq_cancel}; +val if_False = @{thm if_False}; +val iff_conv_conj_imp = @{thm iff_conv_conj_imp}; +val iff = @{thm iff}; +val if_splits = @{thms if_splits}; +val if_True = @{thm if_True}; +val if_weak_cong = @{thm if_weak_cong}; +val imp_all = @{thm imp_all}; +val imp_cong = @{thm imp_cong}; +val imp_conjL = @{thm imp_conjL}; +val imp_conjR = @{thm imp_conjR}; +val imp_conv_disj = @{thm imp_conv_disj}; +val simp_implies_def = @{thm simp_implies_def}; +val simp_thms = @{thms simp_thms}; +val split_if = @{thm split_if}; +val the1_equality = @{thm the1_equality}; +val theI = @{thm theI}; +val theI' = @{thm theI'}; +val True_implies_equals = @{thm True_implies_equals}; val nnf_conv = Simplifier.rewrite (HOL_basic_ss addsimps simp_thms @ @{thms "nnf_simps"}) *} diff -r e6b96b4cde7e -r 0dec18004e75 src/HOL/Hoare_Parallel/Mul_Gar_Coll.thy --- a/src/HOL/Hoare_Parallel/Mul_Gar_Coll.thy Mon Sep 06 19:11:01 2010 +0200 +++ b/src/HOL/Hoare_Parallel/Mul_Gar_Coll.thy Mon Sep 06 19:13:10 2010 +0200 @@ -1199,15 +1199,15 @@ apply(case_tac [!] "M x!(T (Muts x ! j))=Black") apply(simp_all add:Graph10) --{* 47 subgoals left *} -apply(tactic {* TRYALL(EVERY'[REPEAT o (rtac disjI2),etac (thm "subset_psubset_trans"),etac (thm "Graph11"),force_tac @{clasimpset}]) *}) +apply(tactic {* TRYALL(EVERY'[REPEAT o (rtac disjI2),etac @{thm subset_psubset_trans}, etac @{thm Graph11},force_tac @{clasimpset}]) *}) --{* 41 subgoals left *} apply(tactic {* TRYALL(EVERY'[rtac disjI2, rtac disjI1, etac @{thm le_trans}, force_tac (@{claset},@{simpset} addsimps [@{thm Queue_def}, @{thm less_Suc_eq_le}, @{thm le_length_filter_update}])]) *}) --{* 35 subgoals left *} -apply(tactic {* TRYALL(EVERY'[rtac disjI2,rtac disjI1,etac (thm "psubset_subset_trans"),rtac (thm "Graph9"),force_tac @{clasimpset}]) *}) +apply(tactic {* TRYALL(EVERY'[rtac disjI2,rtac disjI1,etac @{thm psubset_subset_trans},rtac @{thm Graph9},force_tac @{clasimpset}]) *}) --{* 31 subgoals left *} -apply(tactic {* TRYALL(EVERY'[rtac disjI2,rtac disjI1,etac (thm "subset_psubset_trans"),etac (thm "Graph11"),force_tac @{clasimpset}]) *}) +apply(tactic {* TRYALL(EVERY'[rtac disjI2,rtac disjI1,etac @{thm subset_psubset_trans},etac @{thm Graph11},force_tac @{clasimpset}]) *}) --{* 29 subgoals left *} -apply(tactic {* TRYALL(EVERY'[REPEAT o (rtac disjI2),etac (thm "subset_psubset_trans"),etac (thm "subset_psubset_trans"),etac (thm "Graph11"),force_tac @{clasimpset}]) *}) +apply(tactic {* TRYALL(EVERY'[REPEAT o (rtac disjI2),etac @{thm subset_psubset_trans},etac @{thm subset_psubset_trans},etac @{thm Graph11},force_tac @{clasimpset}]) *}) --{* 25 subgoals left *} apply(tactic {* TRYALL(EVERY'[rtac disjI2, rtac disjI2, rtac disjI1, etac @{thm le_trans}, force_tac (@{claset},@{simpset} addsimps [@{thm Queue_def}, @{thm less_Suc_eq_le}, @{thm le_length_filter_update}])]) *}) --{* 10 subgoals left *} diff -r e6b96b4cde7e -r 0dec18004e75 src/HOL/Hoare_Parallel/OG_Tactics.thy --- a/src/HOL/Hoare_Parallel/OG_Tactics.thy Mon Sep 06 19:11:01 2010 +0200 +++ b/src/HOL/Hoare_Parallel/OG_Tactics.thy Mon Sep 06 19:13:10 2010 +0200 @@ -273,11 +273,11 @@ lemmas ParallelConseq_list = INTER_def Collect_conj_eq length_map length_upt length_append list_length ML {* -val before_interfree_simp_tac = (simp_tac (HOL_basic_ss addsimps [thm "com.simps", thm "post.simps"])) +val before_interfree_simp_tac = simp_tac (HOL_basic_ss addsimps [@{thm com.simps}, @{thm post.simps}]) -val interfree_simp_tac = (asm_simp_tac (HOL_ss addsimps [@{thm split}, thm "ball_Un", thm "ball_empty"]@(thms "my_simp_list"))) +val interfree_simp_tac = asm_simp_tac (HOL_ss addsimps [@{thm split}, @{thm ball_Un}, @{thm ball_empty}] @ @{thms my_simp_list}) -val ParallelConseq = (simp_tac (HOL_basic_ss addsimps (thms "ParallelConseq_list")@(thms "my_simp_list"))) +val ParallelConseq = simp_tac (HOL_basic_ss addsimps @{thms ParallelConseq_list} @ @{thms my_simp_list}) *} text {* The following tactic applies @{text tac} to each conjunct in a diff -r e6b96b4cde7e -r 0dec18004e75 src/HOL/IMPP/Hoare.thy --- a/src/HOL/IMPP/Hoare.thy Mon Sep 06 19:11:01 2010 +0200 +++ b/src/HOL/IMPP/Hoare.thy Mon Sep 06 19:13:10 2010 +0200 @@ -218,7 +218,7 @@ apply (rule hoare_derivs.conseq, intro strip, tactic "smp_tac 2 1", clarify, tactic "smp_tac 1 1",rule exI, rule exI, erule (1) conjI) prefer 7 apply (rule_tac hoare_derivs.Body, drule_tac spec, erule_tac mp, fast) -apply (tactic {* ALLGOALS (resolve_tac ((funpow 5 tl) (thms "hoare_derivs.intros")) THEN_ALL_NEW (fast_tac @{claset})) *}) +apply (tactic {* ALLGOALS (resolve_tac ((funpow 5 tl) @{thms hoare_derivs.intros}) THEN_ALL_NEW (fast_tac @{claset})) *}) done lemma weak_Body: "G|-{P}. the (body pn) .{Q} ==> G|-{P}. BODY pn .{Q}" @@ -278,7 +278,7 @@ lemma hoare_sound: "G||-ts ==> G||=ts" apply (erule hoare_derivs.induct) -apply (tactic {* TRYALL (eresolve_tac [thm "Loop_sound_lemma", thm "Body_sound_lemma"] THEN_ALL_NEW atac) *}) +apply (tactic {* TRYALL (eresolve_tac [@{thm Loop_sound_lemma}, @{thm Body_sound_lemma}] THEN_ALL_NEW atac) *}) apply (unfold hoare_valids_def) apply blast apply blast @@ -349,7 +349,7 @@ rule_tac [3] P1 = "%Z' s. s= (Z[Loc loc::=fun Z])" in hoare_derivs.Local [THEN conseq1], erule_tac [3] conseq12) apply (erule_tac [5] hoare_derivs.Comp, erule_tac [5] conseq12) -apply (tactic {* (rtac (thm "hoare_derivs.If") THEN_ALL_NEW etac (thm "conseq12")) 6 *}) +apply (tactic {* (rtac @{thm hoare_derivs.If} THEN_ALL_NEW etac @{thm conseq12}) 6 *}) apply (rule_tac [8] hoare_derivs.Loop [THEN conseq2], erule_tac [8] conseq12) apply auto done diff -r e6b96b4cde7e -r 0dec18004e75 src/HOL/IMPP/Natural.thy --- a/src/HOL/IMPP/Natural.thy Mon Sep 06 19:11:01 2010 +0200 +++ b/src/HOL/IMPP/Natural.thy Mon Sep 06 19:13:10 2010 +0200 @@ -114,7 +114,7 @@ lemma evaln_evalc: " -n-> t ==> -c-> t" apply (erule evaln.induct) -apply (tactic {* ALLGOALS (resolve_tac (thms "evalc.intros") THEN_ALL_NEW atac) *}) +apply (tactic {* ALLGOALS (resolve_tac @{thms evalc.intros} THEN_ALL_NEW atac) *}) done lemma Suc_le_D_lemma: "[| Suc n <= m'; (!!m. n <= m ==> P (Suc m)) |] ==> P m'" @@ -124,8 +124,8 @@ lemma evaln_nonstrict [rule_format]: " -n-> t ==> !m. n<=m --> -m-> t" apply (erule evaln.induct) -apply (tactic {* ALLGOALS (EVERY'[strip_tac,TRY o etac (thm "Suc_le_D_lemma"), REPEAT o smp_tac 1]) *}) -apply (tactic {* ALLGOALS (resolve_tac (thms "evaln.intros") THEN_ALL_NEW atac) *}) +apply (tactic {* ALLGOALS (EVERY'[strip_tac,TRY o etac @{thm Suc_le_D_lemma}, REPEAT o smp_tac 1]) *}) +apply (tactic {* ALLGOALS (resolve_tac @{thms evaln.intros} THEN_ALL_NEW atac) *}) done lemma evaln_Suc: " -n-> s' ==> -Suc n-> s'" @@ -142,8 +142,8 @@ lemma evalc_evaln: " -c-> t ==> ? n. -n-> t" apply (erule evalc.induct) apply (tactic {* ALLGOALS (REPEAT o etac exE) *}) -apply (tactic {* TRYALL (EVERY'[datac (thm "evaln_max2") 1, REPEAT o eresolve_tac [exE, conjE]]) *}) -apply (tactic {* ALLGOALS (rtac exI THEN' resolve_tac (thms "evaln.intros") THEN_ALL_NEW atac) *}) +apply (tactic {* TRYALL (EVERY' [datac @{thm evaln_max2} 1, REPEAT o eresolve_tac [exE, conjE]]) *}) +apply (tactic {* ALLGOALS (rtac exI THEN' resolve_tac @{thms evaln.intros} THEN_ALL_NEW atac) *}) done lemma eval_eq: " -c-> t = (? n. -n-> t)" diff -r e6b96b4cde7e -r 0dec18004e75 src/HOL/IOA/Solve.thy --- a/src/HOL/IOA/Solve.thy Mon Sep 06 19:11:01 2010 +0200 +++ b/src/HOL/IOA/Solve.thy Mon Sep 06 19:13:10 2010 +0200 @@ -146,7 +146,7 @@ apply (simp (no_asm) add: conj_disj_distribR cong add: conj_cong split add: split_if) apply (tactic {* REPEAT((resolve_tac [conjI,impI] 1 ORELSE etac conjE 1) THEN - asm_full_simp_tac(@{simpset} addsimps[thm "comp1_reachable", thm "comp2_reachable"]) 1) *}) + asm_full_simp_tac(@{simpset} addsimps [@{thm comp1_reachable}, @{thm comp2_reachable}]) 1) *}) done diff -r e6b96b4cde7e -r 0dec18004e75 src/HOL/Import/hol4rews.ML --- a/src/HOL/Import/hol4rews.ML Mon Sep 06 19:11:01 2010 +0200 +++ b/src/HOL/Import/hol4rews.ML Mon Sep 06 19:13:10 2010 +0200 @@ -156,13 +156,10 @@ val hol4_debug = Unsynchronized.ref false fun message s = if !hol4_debug then writeln s else () -local - val eq_reflection = thm "eq_reflection" -in fun add_hol4_rewrite (Context.Theory thy, th) = let val _ = message "Adding HOL4 rewrite" - val th1 = th RS eq_reflection + val th1 = th RS @{thm eq_reflection} val current_rews = HOL4Rewrites.get thy val new_rews = insert Thm.eq_thm th1 current_rews val updated_thy = HOL4Rewrites.put new_rews thy @@ -170,7 +167,6 @@ (Context.Theory updated_thy,th1) end | add_hol4_rewrite (context, th) = (context, th RS eq_reflection); -end fun ignore_hol4 bthy bthm thy = let diff -r e6b96b4cde7e -r 0dec18004e75 src/HOL/Import/proof_kernel.ML --- a/src/HOL/Import/proof_kernel.ML Mon Sep 06 19:11:01 2010 +0200 +++ b/src/HOL/Import/proof_kernel.ML Mon Sep 06 19:13:10 2010 +0200 @@ -977,28 +977,28 @@ | NONE => raise ERR "uniq_compose" "No result" end -val reflexivity_thm = thm "refl" -val substitution_thm = thm "subst" -val mp_thm = thm "mp" -val imp_antisym_thm = thm "light_imp_as" -val disch_thm = thm "impI" -val ccontr_thm = thm "ccontr" +val reflexivity_thm = @{thm refl} +val substitution_thm = @{thm subst} +val mp_thm = @{thm mp} +val imp_antisym_thm = @{thm light_imp_as} +val disch_thm = @{thm impI} +val ccontr_thm = @{thm ccontr} -val meta_eq_to_obj_eq_thm = thm "meta_eq_to_obj_eq" +val meta_eq_to_obj_eq_thm = @{thm meta_eq_to_obj_eq} -val gen_thm = thm "HOLallI" -val choose_thm = thm "exE" -val exists_thm = thm "exI" -val conj_thm = thm "conjI" -val conjunct1_thm = thm "conjunct1" -val conjunct2_thm = thm "conjunct2" -val spec_thm = thm "spec" -val disj_cases_thm = thm "disjE" -val disj1_thm = thm "disjI1" -val disj2_thm = thm "disjI2" +val gen_thm = @{thm HOLallI} +val choose_thm = @{thm exE} +val exists_thm = @{thm exI} +val conj_thm = @{thm conjI} +val conjunct1_thm = @{thm conjunct1} +val conjunct2_thm = @{thm conjunct2} +val spec_thm = @{thm spec} +val disj_cases_thm = @{thm disjE} +val disj1_thm = @{thm disjI1} +val disj2_thm = @{thm disjI2} local - val th = thm "not_def" + val th = @{thm not_def} val thy = theory_of_thm th val pp = Thm.reflexive (cterm_of thy (Const(@{const_name Trueprop},HOLogic.boolT-->propT))) in @@ -1006,13 +1006,13 @@ end val not_intro_thm = Thm.symmetric not_elim_thm -val abs_thm = thm "ext" -val trans_thm = thm "trans" -val symmetry_thm = thm "sym" -val transitivity_thm = thm "trans" -val eqmp_thm = thm "iffD1" -val eqimp_thm = thm "HOL4Setup.eq_imp" -val comb_thm = thm "cong" +val abs_thm = @{thm ext} +val trans_thm = @{thm trans} +val symmetry_thm = @{thm sym} +val transitivity_thm = @{thm trans} +val eqmp_thm = @{thm iffD1} +val eqimp_thm = @{thm HOL4Setup.eq_imp} +val comb_thm = @{thm cong} (* Beta-eta normalizes a theorem (only the conclusion, not the * hypotheses!) *) @@ -1971,9 +1971,6 @@ (thy22',hth) end -local - val helper = thm "termspec_help" -in fun new_specification thyname thmname names hth thy = case HOL4DefThy.get thy of Replaying _ => (thy,hth) @@ -2054,8 +2051,6 @@ intern_store_thm false thyname thmname hth thy'' end -end - fun new_axiom name tm thy = raise ERR "new_axiom" ("Oh, no you don't! (" ^ name ^ ")") fun to_isa_thm (hth as HOLThm(_,th)) = @@ -2068,10 +2063,10 @@ fun to_isa_term tm = tm local - val light_nonempty = thm "light_ex_imp_nonempty" - val ex_imp_nonempty = thm "ex_imp_nonempty" - val typedef_hol2hol4 = thm "typedef_hol2hol4" - val typedef_hol2hollight = thm "typedef_hol2hollight" + val light_nonempty = @{thm light_ex_imp_nonempty} + val ex_imp_nonempty = @{thm ex_imp_nonempty} + val typedef_hol2hol4 = @{thm typedef_hol2hol4} + val typedef_hol2hollight = @{thm typedef_hol2hollight} in fun new_type_definition thyname thmname tycname hth thy = case HOL4DefThy.get thy of diff -r e6b96b4cde7e -r 0dec18004e75 src/HOL/Import/shuffler.ML --- a/src/HOL/Import/shuffler.ML Mon Sep 06 19:11:01 2010 +0200 +++ b/src/HOL/Import/shuffler.ML Mon Sep 06 19:13:10 2010 +0200 @@ -346,7 +346,7 @@ fun beta_fun thy assume t = SOME (Thm.beta_conversion true (cterm_of thy t)) -val meta_sym_rew = thm "refl" +val meta_sym_rew = @{thm refl} fun equals_fun thy assume t = case t of diff -r e6b96b4cde7e -r 0dec18004e75 src/HOL/MicroJava/J/JTypeSafe.thy --- a/src/HOL/MicroJava/J/JTypeSafe.thy Mon Sep 06 19:11:01 2010 +0200 +++ b/src/HOL/MicroJava/J/JTypeSafe.thy Mon Sep 06 19:13:10 2010 +0200 @@ -201,7 +201,7 @@ -- "several simplifications, XcptE, XcptEs, XcptS, Skip, Nil??" apply( simp_all) apply( tactic "ALLGOALS strip_tac") -apply( tactic {* ALLGOALS (eresolve_tac [thm "ty_expr.cases", thm "ty_exprs.cases", thm "wt_stmt.cases"] +apply( tactic {* ALLGOALS (eresolve_tac [@{thm ty_expr.cases}, @{thm ty_exprs.cases}, @{thm wt_stmt.cases}] THEN_ALL_NEW (full_simp_tac (global_simpset_of @{theory Conform}))) *}) apply(tactic "ALLGOALS (EVERY' [REPEAT o (etac conjE), REPEAT o hyp_subst_tac])") @@ -241,7 +241,7 @@ apply( fast elim: conforms_localD [THEN lconfD]) -- "for FAss" -apply( tactic {* EVERY'[eresolve_tac [thm "ty_expr.cases", thm "ty_exprs.cases", thm "wt_stmt.cases"] +apply( tactic {* EVERY'[eresolve_tac [@{thm ty_expr.cases}, @{thm ty_exprs.cases}, @{thm wt_stmt.cases}] THEN_ALL_NEW (full_simp_tac @{simpset}), REPEAT o (etac conjE), hyp_subst_tac] 3*}) -- "for if" @@ -277,7 +277,7 @@ -- "7 LAss" apply (fold fun_upd_def) -apply( tactic {* (eresolve_tac [thm "ty_expr.cases", thm "ty_exprs.cases", thm "wt_stmt.cases"] +apply( tactic {* (eresolve_tac [@{thm ty_expr.cases}, @{thm ty_exprs.cases}, @{thm wt_stmt.cases}] THEN_ALL_NEW (full_simp_tac @{simpset})) 1 *}) apply (intro strip) apply (case_tac E) diff -r e6b96b4cde7e -r 0dec18004e75 src/HOL/NSA/NSA.thy --- a/src/HOL/NSA/NSA.thy Mon Sep 06 19:11:01 2010 +0200 +++ b/src/HOL/NSA/NSA.thy Mon Sep 06 19:13:10 2010 +0200 @@ -663,9 +663,9 @@ ***) (*reorientation simprules using ==, for the following simproc*) -val meta_zero_approx_reorient = thm "zero_approx_reorient" RS eq_reflection; -val meta_one_approx_reorient = thm "one_approx_reorient" RS eq_reflection; -val meta_number_of_approx_reorient = thm "number_of_approx_reorient" RS eq_reflection +val meta_zero_approx_reorient = @{thm zero_approx_reorient} RS eq_reflection; +val meta_one_approx_reorient = @{thm one_approx_reorient} RS eq_reflection; +val meta_number_of_approx_reorient = @{thm number_of_approx_reorient} RS eq_reflection (*reorientation simplification procedure: reorients (polymorphic) 0 = x, 1 = x, nnn = x provided x isn't 0, 1 or a numeral.*) diff -r e6b96b4cde7e -r 0dec18004e75 src/HOL/Nominal/nominal_datatype.ML --- a/src/HOL/Nominal/nominal_datatype.ML Mon Sep 06 19:11:01 2010 +0200 +++ b/src/HOL/Nominal/nominal_datatype.ML Mon Sep 06 19:13:10 2010 +0200 @@ -24,18 +24,18 @@ structure NominalDatatype : NOMINAL_DATATYPE = struct -val finite_emptyI = thm "finite.emptyI"; -val finite_Diff = thm "finite_Diff"; -val finite_Un = thm "finite_Un"; -val Un_iff = thm "Un_iff"; -val In0_eq = thm "In0_eq"; -val In1_eq = thm "In1_eq"; -val In0_not_In1 = thm "In0_not_In1"; -val In1_not_In0 = thm "In1_not_In0"; -val Un_assoc = thm "Un_assoc"; -val Collect_disj_eq = thm "Collect_disj_eq"; +val finite_emptyI = @{thm finite.emptyI}; +val finite_Diff = @{thm finite_Diff}; +val finite_Un = @{thm finite_Un}; +val Un_iff = @{thm Un_iff}; +val In0_eq = @{thm In0_eq}; +val In1_eq = @{thm In1_eq}; +val In0_not_In1 = @{thm In0_not_In1}; +val In1_not_In0 = @{thm In1_not_In0}; +val Un_assoc = @{thm Un_assoc}; +val Collect_disj_eq = @{thm Collect_disj_eq}; val Collect_False_empty = @{thm empty_def [THEN sym, THEN eq_reflection]}; -val empty_iff = thm "empty_iff"; +val empty_iff = @{thm empty_iff}; open Datatype_Aux; open NominalAtoms; @@ -119,7 +119,7 @@ (** simplification procedure for sorting permutations **) -val dj_cp = thm "dj_cp"; +val dj_cp = @{thm dj_cp}; fun dest_permT (Type ("fun", [Type ("List.list", [Type (@{type_name Product_Type.prod}, [T, _])]), Type ("fun", [_, U])])) = (T, U); @@ -148,23 +148,21 @@ val perm_simproc = Simplifier.simproc_global @{theory} "perm_simp" ["pi1 \ (pi2 \ x)"] perm_simproc'; -val meta_spec = thm "meta_spec"; - fun projections rule = Project_Rule.projections (ProofContext.init_global (Thm.theory_of_thm rule)) rule |> map (Drule.export_without_context #> Rule_Cases.save rule); -val supp_prod = thm "supp_prod"; -val fresh_prod = thm "fresh_prod"; -val supports_fresh = thm "supports_fresh"; -val supports_def = thm "Nominal.supports_def"; -val fresh_def = thm "fresh_def"; -val supp_def = thm "supp_def"; -val rev_simps = thms "rev.simps"; -val app_simps = thms "append.simps"; -val at_fin_set_supp = thm "at_fin_set_supp"; -val at_fin_set_fresh = thm "at_fin_set_fresh"; -val abs_fun_eq1 = thm "abs_fun_eq1"; +val supp_prod = @{thm supp_prod}; +val fresh_prod = @{thm fresh_prod}; +val supports_fresh = @{thm supports_fresh}; +val supports_def = @{thm Nominal.supports_def}; +val fresh_def = @{thm fresh_def}; +val supp_def = @{thm supp_def}; +val rev_simps = @{thms rev.simps}; +val app_simps = @{thms append.simps}; +val at_fin_set_supp = @{thm at_fin_set_supp}; +val at_fin_set_fresh = @{thm at_fin_set_fresh}; +val abs_fun_eq1 = @{thm abs_fun_eq1}; val collect_simp = rewrite_rule [mk_meta_eq mem_Collect_eq]; @@ -1406,7 +1404,7 @@ [rtac induct_aux' 1, REPEAT (resolve_tac fs_atoms 1), REPEAT ((resolve_tac prems THEN_ALL_NEW - (etac meta_spec ORELSE' full_simp_tac (HOL_basic_ss addsimps [fresh_def]))) 1)]) + (etac @{thm meta_spec} ORELSE' full_simp_tac (HOL_basic_ss addsimps [fresh_def]))) 1)]) val (_, thy10) = thy9 |> Sign.add_path big_name |> diff -r e6b96b4cde7e -r 0dec18004e75 src/HOL/Nominal/nominal_inductive.ML --- a/src/HOL/Nominal/nominal_inductive.ML Mon Sep 06 19:11:01 2010 +0200 +++ b/src/HOL/Nominal/nominal_inductive.ML Mon Sep 06 19:13:10 2010 +0200 @@ -30,10 +30,10 @@ fun preds_of ps t = inter (op = o apfst dest_Free) (Term.add_frees t []) ps; -val fresh_prod = thm "fresh_prod"; +val fresh_prod = @{thm fresh_prod}; -val perm_bool = mk_meta_eq (thm "perm_bool"); -val perm_boolI = thm "perm_boolI"; +val perm_bool = mk_meta_eq @{thm perm_bool}; +val perm_boolI = @{thm perm_boolI}; val (_, [perm_boolI_pi, _]) = Drule.strip_comb (snd (Thm.dest_comb (Drule.strip_imp_concl (cprop_of perm_boolI)))); diff -r e6b96b4cde7e -r 0dec18004e75 src/HOL/Nominal/nominal_inductive2.ML --- a/src/HOL/Nominal/nominal_inductive2.ML Mon Sep 06 19:11:01 2010 +0200 +++ b/src/HOL/Nominal/nominal_inductive2.ML Mon Sep 06 19:13:10 2010 +0200 @@ -36,8 +36,8 @@ fun preds_of ps t = inter (op = o apfst dest_Free) (Term.add_frees t []) ps; -val perm_bool = mk_meta_eq (thm "perm_bool"); -val perm_boolI = thm "perm_boolI"; +val perm_bool = mk_meta_eq @{thm perm_bool}; +val perm_boolI = @{thm perm_boolI}; val (_, [perm_boolI_pi, _]) = Drule.strip_comb (snd (Thm.dest_comb (Drule.strip_imp_concl (cprop_of perm_boolI)))); diff -r e6b96b4cde7e -r 0dec18004e75 src/HOL/Old_Number_Theory/Chinese.thy --- a/src/HOL/Old_Number_Theory/Chinese.thy Mon Sep 06 19:11:01 2010 +0200 +++ b/src/HOL/Old_Number_Theory/Chinese.thy Mon Sep 06 19:13:10 2010 +0200 @@ -169,11 +169,11 @@ "0 < n ==> i \ n ==> m_cond n mf ==> km_cond n kf mf ==> \!x. 0 \ x \ x < mf i \ [kf i * mhf mf n i * x = bf i] (mod mf i)" apply (rule zcong_lineq_unique) - apply (tactic {* stac (thm "zgcd_zmult_cancel") 2 *}) + apply (tactic {* stac @{thm zgcd_zmult_cancel} 2 *}) apply (unfold m_cond_def km_cond_def mhf_def) apply (simp_all (no_asm_simp)) apply safe - apply (tactic {* stac (thm "zgcd_zmult_cancel") 3 *}) + apply (tactic {* stac @{thm zgcd_zmult_cancel} 3 *}) apply (rule_tac [!] funprod_zgcd) apply safe apply simp_all @@ -231,12 +231,12 @@ apply (rule_tac x = "x_sol n kf bf mf mod funprod mf 0 n" in exI) apply (unfold lincong_sol_def) apply safe - apply (tactic {* stac (thm "zcong_zmod") 3 *}) - apply (tactic {* stac (thm "mod_mult_eq") 3 *}) - apply (tactic {* stac (thm "mod_mod_cancel") 3 *}) - apply (tactic {* stac (thm "x_sol_lin") 4 *}) - apply (tactic {* stac (thm "mod_mult_eq" RS sym) 6 *}) - apply (tactic {* stac (thm "zcong_zmod" RS sym) 6 *}) + apply (tactic {* stac @{thm zcong_zmod} 3 *}) + apply (tactic {* stac @{thm mod_mult_eq} 3 *}) + apply (tactic {* stac @{thm mod_mod_cancel} 3 *}) + apply (tactic {* stac @{thm x_sol_lin} 4 *}) + apply (tactic {* stac (@{thm mod_mult_eq} RS sym) 6 *}) + apply (tactic {* stac (@{thm zcong_zmod} RS sym) 6 *}) apply (subgoal_tac [6] "0 \ xilin_sol i n kf bf mf \ xilin_sol i n kf bf mf < mf i \ [kf i * mhf mf n i * xilin_sol i n kf bf mf = bf i] (mod mf i)") diff -r e6b96b4cde7e -r 0dec18004e75 src/HOL/Old_Number_Theory/IntPrimes.thy --- a/src/HOL/Old_Number_Theory/IntPrimes.thy Mon Sep 06 19:11:01 2010 +0200 +++ b/src/HOL/Old_Number_Theory/IntPrimes.thy Mon Sep 06 19:13:10 2010 +0200 @@ -399,7 +399,7 @@ zgcd a n = 1 ==> \!x. 0 \ x \ x < n \ [a * x = b] (mod n)" apply auto apply (rule_tac [2] zcong_zless_imp_eq) - apply (tactic {* stac (thm "zcong_cancel2" RS sym) 6 *}) + apply (tactic {* stac (@{thm zcong_cancel2} RS sym) 6 *}) apply (rule_tac [8] zcong_trans) apply (simp_all (no_asm_simp)) prefer 2 diff -r e6b96b4cde7e -r 0dec18004e75 src/HOL/Old_Number_Theory/WilsonBij.thy --- a/src/HOL/Old_Number_Theory/WilsonBij.thy Mon Sep 06 19:11:01 2010 +0200 +++ b/src/HOL/Old_Number_Theory/WilsonBij.thy Mon Sep 06 19:13:10 2010 +0200 @@ -145,9 +145,9 @@ apply (unfold inj_on_def) apply auto apply (rule zcong_zless_imp_eq) - apply (tactic {* stac (thm "zcong_cancel" RS sym) 5 *}) + apply (tactic {* stac (@{thm zcong_cancel} RS sym) 5 *}) apply (rule_tac [7] zcong_trans) - apply (tactic {* stac (thm "zcong_sym") 8 *}) + apply (tactic {* stac @{thm zcong_sym} 8 *}) apply (erule_tac [7] inv_is_inv) apply (tactic "asm_simp_tac @{simpset} 9") apply (erule_tac [9] inv_is_inv) @@ -198,15 +198,15 @@ apply (unfold reciR_def uniqP_def) apply auto apply (rule zcong_zless_imp_eq) - apply (tactic {* stac (thm "zcong_cancel2" RS sym) 5 *}) + apply (tactic {* stac (@{thm zcong_cancel2} RS sym) 5 *}) apply (rule_tac [7] zcong_trans) - apply (tactic {* stac (thm "zcong_sym") 8 *}) + apply (tactic {* stac @{thm zcong_sym} 8 *}) apply (rule_tac [6] zless_zprime_imp_zrelprime) apply auto apply (rule zcong_zless_imp_eq) - apply (tactic {* stac (thm "zcong_cancel" RS sym) 5 *}) + apply (tactic {* stac (@{thm zcong_cancel} RS sym) 5 *}) apply (rule_tac [7] zcong_trans) - apply (tactic {* stac (thm "zcong_sym") 8 *}) + apply (tactic {* stac @{thm zcong_sym} 8 *}) apply (rule_tac [6] zless_zprime_imp_zrelprime) apply auto done diff -r e6b96b4cde7e -r 0dec18004e75 src/HOL/Old_Number_Theory/WilsonRuss.thy --- a/src/HOL/Old_Number_Theory/WilsonRuss.thy Mon Sep 06 19:11:01 2010 +0200 +++ b/src/HOL/Old_Number_Theory/WilsonRuss.thy Mon Sep 06 19:13:10 2010 +0200 @@ -257,7 +257,7 @@ apply (subst wset.simps) apply (auto, unfold Let_def, auto) apply (subst setprod_insert) - apply (tactic {* stac (thm "setprod_insert") 3 *}) + apply (tactic {* stac @{thm setprod_insert} 3 *}) apply (subgoal_tac [5] "zcong (a * inv p a * (\x\wset (a - 1) p. x)) (1 * 1) p") prefer 5 diff -r e6b96b4cde7e -r 0dec18004e75 src/HOL/Option.thy --- a/src/HOL/Option.thy Mon Sep 06 19:11:01 2010 +0200 +++ b/src/HOL/Option.thy Mon Sep 06 19:13:10 2010 +0200 @@ -47,7 +47,7 @@ by simp declaration {* fn _ => - Classical.map_cs (fn cs => cs addSD2 ("ospec", thm "ospec")) + Classical.map_cs (fn cs => cs addSD2 ("ospec", @{thm ospec})) *} lemma elem_set [iff]: "(x : set xo) = (xo = Some x)" diff -r e6b96b4cde7e -r 0dec18004e75 src/HOL/Proofs/Lambda/Commutation.thy --- a/src/HOL/Proofs/Lambda/Commutation.thy Mon Sep 06 19:11:01 2010 +0200 +++ b/src/HOL/Proofs/Lambda/Commutation.thy Mon Sep 06 19:13:10 2010 +0200 @@ -130,9 +130,9 @@ apply (tactic {* safe_tac HOL_cs *}) apply (tactic {* blast_tac (HOL_cs addIs - [thm "sup_ge2" RS thm "rtranclp_mono" RS thm "predicate2D" RS thm "rtranclp_trans", - thm "rtranclp_converseI", thm "conversepI", - thm "sup_ge1" RS thm "rtranclp_mono" RS thm "predicate2D"]) 1 *}) + [@{thm sup_ge2} RS @{thm rtranclp_mono} RS @{thm predicate2D} RS @{thm rtranclp_trans}, + @{thm rtranclp_converseI}, @{thm conversepI}, + @{thm sup_ge1} RS @{thm rtranclp_mono} RS @{thm predicate2D}]) 1 *}) apply (erule rtranclp_induct) apply blast apply (blast del: rtranclp.rtrancl_refl intro: rtranclp_trans) diff -r e6b96b4cde7e -r 0dec18004e75 src/HOL/Statespace/distinct_tree_prover.ML --- a/src/HOL/Statespace/distinct_tree_prover.ML Mon Sep 06 19:11:01 2010 +0200 +++ b/src/HOL/Statespace/distinct_tree_prover.ML Mon Sep 06 19:13:10 2010 +0200 @@ -23,18 +23,19 @@ structure DistinctTreeProver : DISTINCT_TREE_PROVER = struct -val all_distinct_left = thm "DistinctTreeProver.all_distinct_left"; -val all_distinct_right = thm "DistinctTreeProver.all_distinct_right"; + +val all_distinct_left = @{thm DistinctTreeProver.all_distinct_left}; +val all_distinct_right = @{thm DistinctTreeProver.all_distinct_right}; -val distinct_left = thm "DistinctTreeProver.distinct_left"; -val distinct_right = thm "DistinctTreeProver.distinct_right"; -val distinct_left_right = thm "DistinctTreeProver.distinct_left_right"; -val in_set_root = thm "DistinctTreeProver.in_set_root"; -val in_set_left = thm "DistinctTreeProver.in_set_left"; -val in_set_right = thm "DistinctTreeProver.in_set_right"; +val distinct_left = @{thm DistinctTreeProver.distinct_left}; +val distinct_right = @{thm DistinctTreeProver.distinct_right}; +val distinct_left_right = @{thm DistinctTreeProver.distinct_left_right}; +val in_set_root = @{thm DistinctTreeProver.in_set_root}; +val in_set_left = @{thm DistinctTreeProver.in_set_left}; +val in_set_right = @{thm DistinctTreeProver.in_set_right}; -val swap_neq = thm "DistinctTreeProver.swap_neq"; -val neq_to_eq_False = thm "DistinctTreeProver.neq_to_eq_False" +val swap_neq = @{thm DistinctTreeProver.swap_neq}; +val neq_to_eq_False = @{thm DistinctTreeProver.neq_to_eq_False}; datatype Direction = Left | Right @@ -273,9 +274,9 @@ end -val delete_root = thm "DistinctTreeProver.delete_root"; -val delete_left = thm "DistinctTreeProver.delete_left"; -val delete_right = thm "DistinctTreeProver.delete_right"; +val delete_root = @{thm DistinctTreeProver.delete_root}; +val delete_left = @{thm DistinctTreeProver.delete_left}; +val delete_right = @{thm DistinctTreeProver.delete_right}; fun deleteProver dist_thm [] = delete_root OF [dist_thm] | deleteProver dist_thm (p::ps) = @@ -286,10 +287,10 @@ val del = deleteProver dist_thm' ps; in discharge [dist_thm, del] del_rule end; -val subtract_Tip = thm "DistinctTreeProver.subtract_Tip"; -val subtract_Node = thm "DistinctTreeProver.subtract_Node"; -val delete_Some_all_distinct = thm "DistinctTreeProver.delete_Some_all_distinct"; -val subtract_Some_all_distinct_res = thm "DistinctTreeProver.subtract_Some_all_distinct_res"; +val subtract_Tip = @{thm DistinctTreeProver.subtract_Tip}; +val subtract_Node = @{thm DistinctTreeProver.subtract_Node}; +val delete_Some_all_distinct = @{thm DistinctTreeProver.delete_Some_all_distinct}; +val subtract_Some_all_distinct_res = @{thm DistinctTreeProver.subtract_Some_all_distinct_res}; local val (alpha,v) = @@ -320,7 +321,7 @@ in discharge [del_tree, sub_l, sub_r] subtract_Node end end -val subtract_Some_all_distinct = thm "DistinctTreeProver.subtract_Some_all_distinct"; +val subtract_Some_all_distinct = @{thm DistinctTreeProver.subtract_Some_all_distinct}; fun distinct_implProver dist_thm ct = let val ctree = ct |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2; diff -r e6b96b4cde7e -r 0dec18004e75 src/HOL/Statespace/state_fun.ML --- a/src/HOL/Statespace/state_fun.ML Mon Sep 06 19:11:01 2010 +0200 +++ b/src/HOL/Statespace/state_fun.ML Mon Sep 06 19:13:10 2010 +0200 @@ -38,10 +38,10 @@ local -val conj1_False = thm "conj1_False"; -val conj2_False = thm "conj2_False"; -val conj_True = thm "conj_True"; -val conj_cong = thm "conj_cong"; +val conj1_False = @{thm conj1_False}; +val conj2_False = @{thm conj2_False}; +val conj_True = @{thm conj_True}; +val conj_cong = @{thm conj_cong}; fun isFalse (Const (@{const_name False},_)) = true | isFalse _ = false; @@ -255,7 +255,7 @@ local -val swap_ex_eq = thm "StateFun.swap_ex_eq"; +val swap_ex_eq = @{thm StateFun.swap_ex_eq}; fun is_selector thy T sel = let val (flds,more) = Record.get_recT_fields thy T diff -r e6b96b4cde7e -r 0dec18004e75 src/HOL/TLA/Memory/Memory.thy --- a/src/HOL/TLA/Memory/Memory.thy Mon Sep 06 19:11:01 2010 +0200 +++ b/src/HOL/TLA/Memory/Memory.thy Mon Sep 06 19:13:10 2010 +0200 @@ -181,10 +181,10 @@ |- Calling ch p & (rs!p ~= #NotAResult) --> Enabled (_(rtrner ch ! p, rs!p))" apply (tactic - {* action_simp_tac @{simpset} [thm "MemReturn_change" RSN (2, thm "enabled_mono") ] [] 1 *}) + {* action_simp_tac @{simpset} [@{thm MemReturn_change} RSN (2, @{thm enabled_mono}) ] [] 1 *}) apply (tactic - {* action_simp_tac (@{simpset} addsimps [thm "MemReturn_def", thm "Return_def", - thm "rtrner_def"]) [exI] [thm "base_enabled", thm "Pair_inject"] 1 *}) + {* action_simp_tac (@{simpset} addsimps [@{thm MemReturn_def}, @{thm Return_def}, + @{thm rtrner_def}]) [exI] [@{thm base_enabled}, @{thm Pair_inject}] 1 *}) done lemma ReadInner_enabled: "!!p. basevars (rtrner ch ! p, rs!p) ==> @@ -227,13 +227,13 @@ --> Enabled (_(rtrner ch ! p, rs!p))" apply (auto simp: enabled_disj [try_rewrite] intro!: RWRNext_enabled [temp_use]) apply (case_tac "arg (ch w p)") - apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "Read_def", - temp_rewrite (thm "enabled_ex")]) [thm "ReadInner_enabled", exI] [] 1 *}) + apply (tactic {* action_simp_tac (@{simpset} addsimps [@{thm Read_def}, + temp_rewrite @{thm enabled_ex}]) [@{thm ReadInner_enabled}, exI] [] 1 *}) apply (force dest: base_pair [temp_use]) apply (erule contrapos_np) - apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "Write_def", - temp_rewrite (thm "enabled_ex")]) - [thm "WriteInner_enabled", exI] [] 1 *}) + apply (tactic {* action_simp_tac (@{simpset} addsimps [@{thm Write_def}, + temp_rewrite @{thm enabled_ex}]) + [@{thm WriteInner_enabled}, exI] [] 1 *}) done end diff -r e6b96b4cde7e -r 0dec18004e75 src/HOL/TLA/Memory/MemoryImplementation.thy --- a/src/HOL/TLA/Memory/MemoryImplementation.thy Mon Sep 06 19:11:01 2010 +0200 +++ b/src/HOL/TLA/Memory/MemoryImplementation.thy Mon Sep 06 19:13:10 2010 +0200 @@ -255,10 +255,10 @@ apply (rule historyI) apply assumption+ apply (rule MI_base) - apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "HInit_def"]) [] [] 1 *}) + apply (tactic {* action_simp_tac (@{simpset} addsimps [@{thm HInit_def}]) [] [] 1 *}) apply (erule fun_cong) - apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "HNext_def"]) - [thm "busy_squareI"] [] 1 *}) + apply (tactic {* action_simp_tac (@{simpset} addsimps [@{thm HNext_def}]) + [@{thm busy_squareI}] [] 1 *}) apply (erule fun_cong) done @@ -346,22 +346,22 @@ caller_def rtrner_def MVNROKBA_def S_def S1_def S2_def Calling_def) lemma S1ClerkUnch: "|- [MClkNext memCh crCh cst p]_(c p) & $(S1 rmhist p) --> unchanged (c p)" - by (tactic {* auto_tac (MI_fast_css addSDs2 [temp_use (thm "MClkidle")] - addsimps2 [thm "S_def", thm "S1_def"]) *}) + by (tactic {* auto_tac (MI_fast_css addSDs2 [temp_use @{thm MClkidle}] + addsimps2 [@{thm S_def}, @{thm S1_def}]) *}) lemma S1RPCUnch: "|- [RPCNext crCh rmCh rst p]_(r p) & $(S1 rmhist p) --> unchanged (r p)" - by (tactic {* auto_tac (MI_fast_css addSDs2 [temp_use (thm "RPCidle")] - addsimps2 [thm "S_def", thm "S1_def"]) *}) + by (tactic {* auto_tac (MI_fast_css addSDs2 [temp_use @{thm RPCidle}] + addsimps2 [@{thm S_def}, @{thm S1_def}]) *}) lemma S1MemUnch: "|- [RNext rmCh mm ires p]_(m p) & $(S1 rmhist p) --> unchanged (m p)" - by (tactic {* auto_tac (MI_fast_css addSDs2 [temp_use (thm "Memoryidle")] - addsimps2 [thm "S_def", thm "S1_def"]) *}) + by (tactic {* auto_tac (MI_fast_css addSDs2 [temp_use @{thm Memoryidle}] + addsimps2 [@{thm S_def}, @{thm S1_def}]) *}) lemma S1Hist: "|- [HNext rmhist p]_(c p,r p,m p,rmhist!p) & $(S1 rmhist p) --> unchanged (rmhist!p)" - by (tactic {* action_simp_tac (@{simpset} addsimps [thm "HNext_def", thm "S_def", - thm "S1_def", thm "MemReturn_def", thm "RPCFail_def", thm "MClkReply_def", - thm "Return_def"]) [] [temp_use (thm "squareE")] 1 *}) + by (tactic {* action_simp_tac (@{simpset} addsimps [@{thm HNext_def}, @{thm S_def}, + @{thm S1_def}, @{thm MemReturn_def}, @{thm RPCFail_def}, @{thm MClkReply_def}, + @{thm Return_def}]) [] [temp_use @{thm squareE}] 1 *}) (* ------------------------------ State S2 ---------------------------------------- *) @@ -375,9 +375,9 @@ lemma S2Forward: "|- $(S2 rmhist p) & MClkFwd memCh crCh cst p & unchanged (e p, r p, m p, rmhist!p) --> (S3 rmhist p)$" - by (tactic {* action_simp_tac (@{simpset} addsimps [thm "MClkFwd_def", - thm "Call_def", thm "e_def", thm "r_def", thm "m_def", thm "caller_def", - thm "rtrner_def", thm "S_def", thm "S2_def", thm "S3_def", thm "Calling_def"]) [] [] 1 *}) + by (tactic {* action_simp_tac (@{simpset} addsimps [@{thm MClkFwd_def}, + @{thm Call_def}, @{thm e_def}, @{thm r_def}, @{thm m_def}, @{thm caller_def}, + @{thm rtrner_def}, @{thm S_def}, @{thm S2_def}, @{thm S3_def}, @{thm Calling_def}]) [] [] 1 *}) lemma S2RPCUnch: "|- [RPCNext crCh rmCh rst p]_(r p) & $(S2 rmhist p) --> unchanged (r p)" by (auto simp: S_def S2_def dest!: RPCidle [temp_use]) @@ -387,8 +387,8 @@ lemma S2Hist: "|- [HNext rmhist p]_(c p,r p,m p,rmhist!p) & $(S2 rmhist p) --> unchanged (rmhist!p)" - by (tactic {* auto_tac (MI_fast_css addsimps2 [thm "HNext_def", thm "MemReturn_def", - thm "RPCFail_def", thm "MClkReply_def", thm "Return_def", thm "S_def", thm "S2_def"]) *}) + by (tactic {* auto_tac (MI_fast_css addsimps2 [@{thm HNext_def}, @{thm MemReturn_def}, + @{thm RPCFail_def}, @{thm MClkReply_def}, @{thm Return_def}, @{thm S_def}, @{thm S2_def}]) *}) (* ------------------------------ State S3 ---------------------------------------- *) @@ -411,19 +411,19 @@ lemma S3Forward: "|- RPCFwd crCh rmCh rst p & HNext rmhist p & $(S3 rmhist p) & unchanged (e p, c p, m p) --> (S4 rmhist p)$ & unchanged (rmhist!p)" - by (tactic {* action_simp_tac (@{simpset} addsimps [thm "RPCFwd_def", - thm "HNext_def", thm "MemReturn_def", thm "RPCFail_def", - thm "MClkReply_def", thm "Return_def", thm "Call_def", thm "e_def", - thm "c_def", thm "m_def", thm "caller_def", thm "rtrner_def", thm "S_def", - thm "S3_def", thm "S4_def", thm "Calling_def"]) [] [] 1 *}) + by (tactic {* action_simp_tac (@{simpset} addsimps [@{thm RPCFwd_def}, + @{thm HNext_def}, @{thm MemReturn_def}, @{thm RPCFail_def}, + @{thm MClkReply_def}, @{thm Return_def}, @{thm Call_def}, @{thm e_def}, + @{thm c_def}, @{thm m_def}, @{thm caller_def}, @{thm rtrner_def}, @{thm S_def}, + @{thm S3_def}, @{thm S4_def}, @{thm Calling_def}]) [] [] 1 *}) lemma S3Fail: "|- RPCFail crCh rmCh rst p & $(S3 rmhist p) & HNext rmhist p & unchanged (e p, c p, m p) --> (S6 rmhist p)$" - by (tactic {* action_simp_tac (@{simpset} addsimps [thm "HNext_def", - thm "RPCFail_def", thm "Return_def", thm "e_def", thm "c_def", - thm "m_def", thm "caller_def", thm "rtrner_def", thm "MVOKBARF_def", - thm "S_def", thm "S3_def", thm "S6_def", thm "Calling_def"]) [] [] 1 *}) + by (tactic {* action_simp_tac (@{simpset} addsimps [@{thm HNext_def}, + @{thm RPCFail_def}, @{thm Return_def}, @{thm e_def}, @{thm c_def}, + @{thm m_def}, @{thm caller_def}, @{thm rtrner_def}, @{thm MVOKBARF_def}, + @{thm S_def}, @{thm S3_def}, @{thm S6_def}, @{thm Calling_def}]) [] [] 1 *}) lemma S3MemUnch: "|- [RNext rmCh mm ires p]_(m p) & $(S3 rmhist p) --> unchanged (m p)" by (auto simp: S_def S3_def dest!: Memoryidle [temp_use]) @@ -441,18 +441,18 @@ by (auto simp: S_def S4_def dest!: MClkbusy [temp_use]) lemma S4RPCUnch: "|- [RPCNext crCh rmCh rst p]_(r p) & $(S4 rmhist p) --> unchanged (r p)" - by (tactic {* auto_tac (MI_fast_css addsimps2 [thm "S_def", thm "S4_def"] - addSDs2 [temp_use (thm "RPCbusy")]) *}) + by (tactic {* auto_tac (MI_fast_css addsimps2 [@{thm S_def}, @{thm S4_def}] + addSDs2 [temp_use @{thm RPCbusy}]) *}) lemma S4ReadInner: "|- ReadInner rmCh mm ires p l & $(S4 rmhist p) & unchanged (e p, c p, r p) & HNext rmhist p & $(MemInv mm l) --> (S4 rmhist p)$ & unchanged (rmhist!p)" - by (tactic {* action_simp_tac (@{simpset} addsimps [thm "ReadInner_def", - thm "GoodRead_def", thm "BadRead_def", thm "HNext_def", thm "MemReturn_def", - thm "RPCFail_def", thm "MClkReply_def", thm "Return_def", thm "e_def", - thm "c_def", thm "r_def", thm "rtrner_def", thm "caller_def", - thm "MVNROKBA_def", thm "S_def", thm "S4_def", thm "RdRequest_def", - thm "Calling_def", thm "MemInv_def"]) [] [] 1 *}) + by (tactic {* action_simp_tac (@{simpset} addsimps [@{thm ReadInner_def}, + @{thm GoodRead_def}, @{thm BadRead_def}, @{thm HNext_def}, @{thm MemReturn_def}, + @{thm RPCFail_def}, @{thm MClkReply_def}, @{thm Return_def}, @{thm e_def}, + @{thm c_def}, @{thm r_def}, @{thm rtrner_def}, @{thm caller_def}, + @{thm MVNROKBA_def}, @{thm S_def}, @{thm S4_def}, @{thm RdRequest_def}, + @{thm Calling_def}, @{thm MemInv_def}]) [] [] 1 *}) lemma S4Read: "|- Read rmCh mm ires p & $(S4 rmhist p) & unchanged (e p, c p, r p) & HNext rmhist p & (!l. $MemInv mm l) @@ -461,11 +461,11 @@ lemma S4WriteInner: "|- WriteInner rmCh mm ires p l v & $(S4 rmhist p) & unchanged (e p, c p, r p) & HNext rmhist p --> (S4 rmhist p)$ & unchanged (rmhist!p)" - by (tactic {* action_simp_tac (@{simpset} addsimps [thm "WriteInner_def", - thm "GoodWrite_def", thm "BadWrite_def", thm "HNext_def", thm "MemReturn_def", - thm "RPCFail_def", thm "MClkReply_def", thm "Return_def", thm "e_def", - thm "c_def", thm "r_def", thm "rtrner_def", thm "caller_def", thm "MVNROKBA_def", - thm "S_def", thm "S4_def", thm "WrRequest_def", thm "Calling_def"]) [] [] 1 *}) + by (tactic {* action_simp_tac (@{simpset} addsimps [@{thm WriteInner_def}, + @{thm GoodWrite_def}, @{thm BadWrite_def}, @{thm HNext_def}, @{thm MemReturn_def}, + @{thm RPCFail_def}, @{thm MClkReply_def}, @{thm Return_def}, @{thm e_def}, + @{thm c_def}, @{thm r_def}, @{thm rtrner_def}, @{thm caller_def}, @{thm MVNROKBA_def}, + @{thm S_def}, @{thm S4_def}, @{thm WrRequest_def}, @{thm Calling_def}]) [] [] 1 *}) lemma S4Write: "|- Write rmCh mm ires p l & $(S4 rmhist p) & unchanged (e p, c p, r p) & (HNext rmhist p) @@ -500,26 +500,26 @@ lemma S5Reply: "|- RPCReply crCh rmCh rst p & $(S5 rmhist p) & unchanged (e p, c p, m p,rmhist!p) --> (S6 rmhist p)$" - by (tactic {* action_simp_tac (@{simpset} addsimps [thm "RPCReply_def", - thm "Return_def", thm "e_def", thm "c_def", thm "m_def", thm "MVOKBA_def", - thm "MVOKBARF_def", thm "caller_def", thm "rtrner_def", thm "S_def", - thm "S5_def", thm "S6_def", thm "Calling_def"]) [] [] 1 *}) + by (tactic {* action_simp_tac (@{simpset} addsimps [@{thm RPCReply_def}, + @{thm Return_def}, @{thm e_def}, @{thm c_def}, @{thm m_def}, @{thm MVOKBA_def}, + @{thm MVOKBARF_def}, @{thm caller_def}, @{thm rtrner_def}, @{thm S_def}, + @{thm S5_def}, @{thm S6_def}, @{thm Calling_def}]) [] [] 1 *}) lemma S5Fail: "|- RPCFail crCh rmCh rst p & $(S5 rmhist p) & unchanged (e p, c p, m p,rmhist!p) --> (S6 rmhist p)$" - by (tactic {* action_simp_tac (@{simpset} addsimps [thm "RPCFail_def", - thm "Return_def", thm "e_def", thm "c_def", thm "m_def", - thm "MVOKBARF_def", thm "caller_def", thm "rtrner_def", - thm "S_def", thm "S5_def", thm "S6_def", thm "Calling_def"]) [] [] 1 *}) + by (tactic {* action_simp_tac (@{simpset} addsimps [@{thm RPCFail_def}, + @{thm Return_def}, @{thm e_def}, @{thm c_def}, @{thm m_def}, + @{thm MVOKBARF_def}, @{thm caller_def}, @{thm rtrner_def}, + @{thm S_def}, @{thm S5_def}, @{thm S6_def}, @{thm Calling_def}]) [] [] 1 *}) lemma S5MemUnch: "|- [RNext rmCh mm ires p]_(m p) & $(S5 rmhist p) --> unchanged (m p)" by (auto simp: S_def S5_def dest!: Memoryidle [temp_use]) lemma S5Hist: "|- [HNext rmhist p]_(c p, r p, m p, rmhist!p) & $(S5 rmhist p) --> (rmhist!p)$ = $(rmhist!p)" - by (tactic {* auto_tac (MI_fast_css addsimps2 [thm "HNext_def", - thm "MemReturn_def", thm "RPCFail_def", thm "MClkReply_def", thm "Return_def", - thm "S_def", thm "S5_def"]) *}) + by (tactic {* auto_tac (MI_fast_css addsimps2 [@{thm HNext_def}, + @{thm MemReturn_def}, @{thm RPCFail_def}, @{thm MClkReply_def}, @{thm Return_def}, + @{thm S_def}, @{thm S5_def}]) *}) (* ------------------------------ State S6 ---------------------------------------- *) @@ -533,18 +533,18 @@ lemma S6Retry: "|- MClkRetry memCh crCh cst p & HNext rmhist p & $S6 rmhist p & unchanged (e p,r p,m p) --> (S3 rmhist p)$ & unchanged (rmhist!p)" - by (tactic {* action_simp_tac (@{simpset} addsimps [thm "HNext_def", - thm "MClkReply_def", thm "MClkRetry_def", thm "Call_def", thm "Return_def", - thm "e_def", thm "r_def", thm "m_def", thm "caller_def", thm "rtrner_def", - thm "S_def", thm "S6_def", thm "S3_def", thm "Calling_def"]) [] [] 1 *}) + by (tactic {* action_simp_tac (@{simpset} addsimps [@{thm HNext_def}, + @{thm MClkReply_def}, @{thm MClkRetry_def}, @{thm Call_def}, @{thm Return_def}, + @{thm e_def}, @{thm r_def}, @{thm m_def}, @{thm caller_def}, @{thm rtrner_def}, + @{thm S_def}, @{thm S6_def}, @{thm S3_def}, @{thm Calling_def}]) [] [] 1 *}) lemma S6Reply: "|- MClkReply memCh crCh cst p & HNext rmhist p & $S6 rmhist p & unchanged (e p,r p,m p) --> (S1 rmhist p)$" - by (tactic {* action_simp_tac (@{simpset} addsimps [thm "HNext_def", - thm "MemReturn_def", thm "RPCFail_def", thm "Return_def", thm "MClkReply_def", - thm "e_def", thm "r_def", thm "m_def", thm "caller_def", thm "rtrner_def", - thm "S_def", thm "S6_def", thm "S1_def", thm "Calling_def"]) [] [] 1 *}) + by (tactic {* action_simp_tac (@{simpset} addsimps [@{thm HNext_def}, + @{thm MemReturn_def}, @{thm RPCFail_def}, @{thm Return_def}, @{thm MClkReply_def}, + @{thm e_def}, @{thm r_def}, @{thm m_def}, @{thm caller_def}, @{thm rtrner_def}, + @{thm S_def}, @{thm S6_def}, @{thm S1_def}, @{thm Calling_def}]) [] [] 1 *}) lemma S6RPCUnch: "|- [RPCNext crCh rmCh rst p]_(r p) & $S6 rmhist p --> unchanged (r p)" by (auto simp: S_def S6_def dest!: RPCidle [temp_use]) @@ -563,9 +563,9 @@ (* The implementation's initial condition implies the state predicate S1 *) lemma Step1_1: "|- ImpInit p & HInit rmhist p --> S1 rmhist p" - by (tactic {* auto_tac (MI_fast_css addsimps2 [thm "MVNROKBA_def", - thm "MClkInit_def", thm "RPCInit_def", thm "PInit_def", thm "HInit_def", - thm "ImpInit_def", thm "S_def", thm "S1_def"]) *}) + by (tactic {* auto_tac (MI_fast_css addsimps2 [@{thm MVNROKBA_def}, + @{thm MClkInit_def}, @{thm RPCInit_def}, @{thm PInit_def}, @{thm HInit_def}, + @{thm ImpInit_def}, @{thm S_def}, @{thm S1_def}]) *}) (* ========== Step 1.2 ================================================== *) (* Figure 16 is a predicate-action diagram for the implementation. *) @@ -573,29 +573,29 @@ lemma Step1_2_1: "|- [HNext rmhist p]_(c p,r p,m p, rmhist!p) & ImpNext p & ~unchanged (e p, c p, r p, m p, rmhist!p) & $S1 rmhist p --> (S2 rmhist p)$ & ENext p & unchanged (c p, r p, m p)" - apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "ImpNext_def"]) [] - (map temp_elim [thm "S1ClerkUnch", thm "S1RPCUnch", thm "S1MemUnch", thm "S1Hist"]) 1 *}) - apply (tactic {* auto_tac (MI_fast_css addSIs2 [temp_use (thm "S1Env")]) *}) + apply (tactic {* action_simp_tac (@{simpset} addsimps [@{thm ImpNext_def}]) [] + (map temp_elim [@{thm S1ClerkUnch}, @{thm S1RPCUnch}, @{thm S1MemUnch}, @{thm S1Hist}]) 1 *}) + apply (tactic {* auto_tac (MI_fast_css addSIs2 [temp_use @{thm S1Env}]) *}) done lemma Step1_2_2: "|- [HNext rmhist p]_(c p,r p,m p, rmhist!p) & ImpNext p & ~unchanged (e p, c p, r p, m p, rmhist!p) & $S2 rmhist p --> (S3 rmhist p)$ & MClkFwd memCh crCh cst p & unchanged (e p, r p, m p, rmhist!p)" - apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "ImpNext_def"]) [] - (map temp_elim [thm "S2EnvUnch", thm "S2RPCUnch", thm "S2MemUnch", thm "S2Hist"]) 1 *}) - apply (tactic {* auto_tac (MI_fast_css addSIs2 [temp_use (thm "S2Clerk"), - temp_use (thm "S2Forward")]) *}) + apply (tactic {* action_simp_tac (@{simpset} addsimps [@{thm ImpNext_def}]) [] + (map temp_elim [@{thm S2EnvUnch}, @{thm S2RPCUnch}, @{thm S2MemUnch}, @{thm S2Hist}]) 1 *}) + apply (tactic {* auto_tac (MI_fast_css addSIs2 [temp_use @{thm S2Clerk}, + temp_use @{thm S2Forward}]) *}) done lemma Step1_2_3: "|- [HNext rmhist p]_(c p,r p,m p, rmhist!p) & ImpNext p & ~unchanged (e p, c p, r p, m p, rmhist!p) & $S3 rmhist p --> ((S4 rmhist p)$ & RPCFwd crCh rmCh rst p & unchanged (e p, c p, m p, rmhist!p)) | ((S6 rmhist p)$ & RPCFail crCh rmCh rst p & unchanged (e p, c p, m p))" - apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "ImpNext_def"]) [] - (map temp_elim [thm "S3EnvUnch", thm "S3ClerkUnch", thm "S3MemUnch"]) 1 *}) + apply (tactic {* action_simp_tac (@{simpset} addsimps [@{thm ImpNext_def}]) [] + (map temp_elim [@{thm S3EnvUnch}, @{thm S3ClerkUnch}, @{thm S3MemUnch}]) 1 *}) apply (tactic {* action_simp_tac @{simpset} [] - (thm "squareE" :: map temp_elim [thm "S3RPC", thm "S3Forward", thm "S3Fail"]) 1 *}) + (@{thm squareE} :: map temp_elim [@{thm S3RPC}, @{thm S3Forward}, @{thm S3Fail}]) 1 *}) apply (auto dest!: S3Hist [temp_use]) done @@ -605,10 +605,10 @@ --> ((S4 rmhist p)$ & Read rmCh mm ires p & unchanged (e p, c p, r p, rmhist!p)) | ((S4 rmhist p)$ & (? l. Write rmCh mm ires p l) & unchanged (e p, c p, r p, rmhist!p)) | ((S5 rmhist p)$ & MemReturn rmCh ires p & unchanged (e p, c p, r p))" - apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "ImpNext_def"]) [] - (map temp_elim [thm "S4EnvUnch", thm "S4ClerkUnch", thm "S4RPCUnch"]) 1 *}) - apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "RNext_def"]) [] - (thm "squareE" :: map temp_elim [thm "S4Read", thm "S4Write", thm "S4Return"]) 1 *}) + apply (tactic {* action_simp_tac (@{simpset} addsimps [@{thm ImpNext_def}]) [] + (map temp_elim [@{thm S4EnvUnch}, @{thm S4ClerkUnch}, @{thm S4RPCUnch}]) 1 *}) + apply (tactic {* action_simp_tac (@{simpset} addsimps [@{thm RNext_def}]) [] + (@{thm squareE} :: map temp_elim [@{thm S4Read}, @{thm S4Write}, @{thm S4Return}]) 1 *}) apply (auto dest!: S4Hist [temp_use]) done @@ -616,21 +616,21 @@ & ~unchanged (e p, c p, r p, m p, rmhist!p) & $S5 rmhist p --> ((S6 rmhist p)$ & RPCReply crCh rmCh rst p & unchanged (e p, c p, m p)) | ((S6 rmhist p)$ & RPCFail crCh rmCh rst p & unchanged (e p, c p, m p))" - apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "ImpNext_def"]) [] - (map temp_elim [thm "S5EnvUnch", thm "S5ClerkUnch", thm "S5MemUnch", thm "S5Hist"]) 1 *}) - apply (tactic {* action_simp_tac @{simpset} [] [thm "squareE", temp_elim (thm "S5RPC")] 1 *}) + apply (tactic {* action_simp_tac (@{simpset} addsimps [@{thm ImpNext_def}]) [] + (map temp_elim [@{thm S5EnvUnch}, @{thm S5ClerkUnch}, @{thm S5MemUnch}, @{thm S5Hist}]) 1 *}) + apply (tactic {* action_simp_tac @{simpset} [] [@{thm squareE}, temp_elim @{thm S5RPC}] 1 *}) apply (tactic {* auto_tac (MI_fast_css addSDs2 - [temp_use (thm "S5Reply"), temp_use (thm "S5Fail")]) *}) + [temp_use @{thm S5Reply}, temp_use @{thm S5Fail}]) *}) done lemma Step1_2_6: "|- [HNext rmhist p]_(c p,r p,m p, rmhist!p) & ImpNext p & ~unchanged (e p, c p, r p, m p, rmhist!p) & $S6 rmhist p --> ((S1 rmhist p)$ & MClkReply memCh crCh cst p & unchanged (e p, r p, m p)) | ((S3 rmhist p)$ & MClkRetry memCh crCh cst p & unchanged (e p,r p,m p,rmhist!p))" - apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "ImpNext_def"]) [] - (map temp_elim [thm "S6EnvUnch", thm "S6RPCUnch", thm "S6MemUnch"]) 1 *}) + apply (tactic {* action_simp_tac (@{simpset} addsimps [@{thm ImpNext_def}]) [] + (map temp_elim [@{thm S6EnvUnch}, @{thm S6RPCUnch}, @{thm S6MemUnch}]) 1 *}) apply (tactic {* action_simp_tac @{simpset} [] - (thm "squareE" :: map temp_elim [thm "S6Clerk", thm "S6Retry", thm "S6Reply"]) 1 *}) + (@{thm squareE} :: map temp_elim [@{thm S6Clerk}, @{thm S6Retry}, @{thm S6Reply}]) 1 *}) apply (auto dest: S6Hist [temp_use]) done @@ -641,8 +641,8 @@ section "Initialization (Step 1.3)" lemma Step1_3: "|- S1 rmhist p --> PInit (resbar rmhist) p" - by (tactic {* action_simp_tac (@{simpset} addsimps [thm "resbar_def", - thm "PInit_def", thm "S_def", thm "S1_def"]) [] [] 1 *}) + by (tactic {* action_simp_tac (@{simpset} addsimps [@{thm resbar_def}, + @{thm PInit_def}, @{thm S_def}, @{thm S1_def}]) [] [] 1 *}) (* ---------------------------------------------------------------------- Step 1.4: Implementation's next-state relation simulates specification's @@ -653,23 +653,23 @@ lemma Step1_4_1: "|- ENext p & $S1 rmhist p & (S2 rmhist p)$ & unchanged (c p, r p, m p) --> unchanged (rtrner memCh!p, resbar rmhist!p)" - by (tactic {* auto_tac (MI_fast_css addsimps2 [thm "c_def", thm "r_def", - thm "m_def", thm "resbar_def"]) *}) + by (tactic {* auto_tac (MI_fast_css addsimps2 [@{thm c_def}, @{thm r_def}, + @{thm m_def}, @{thm resbar_def}]) *}) lemma Step1_4_2: "|- MClkFwd memCh crCh cst p & $S2 rmhist p & (S3 rmhist p)$ & unchanged (e p, r p, m p, rmhist!p) --> unchanged (rtrner memCh!p, resbar rmhist!p)" by (tactic {* action_simp_tac - (@{simpset} addsimps [thm "MClkFwd_def", thm "e_def", thm "r_def", thm "m_def", - thm "resbar_def", thm "S_def", thm "S2_def", thm "S3_def"]) [] [] 1 *}) + (@{simpset} addsimps [@{thm MClkFwd_def}, @{thm e_def}, @{thm r_def}, @{thm m_def}, + @{thm resbar_def}, @{thm S_def}, @{thm S2_def}, @{thm S3_def}]) [] [] 1 *}) lemma Step1_4_3a: "|- RPCFwd crCh rmCh rst p & $S3 rmhist p & (S4 rmhist p)$ & unchanged (e p, c p, m p, rmhist!p) --> unchanged (rtrner memCh!p, resbar rmhist!p)" apply clarsimp apply (drule S3_excl [temp_use] S4_excl [temp_use])+ - apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "e_def", - thm "c_def", thm "m_def", thm "resbar_def", thm "S_def", thm "S3_def"]) [] [] 1 *}) + apply (tactic {* action_simp_tac (@{simpset} addsimps [@{thm e_def}, + @{thm c_def}, @{thm m_def}, @{thm resbar_def}, @{thm S_def}, @{thm S3_def}]) [] [] 1 *}) done lemma Step1_4_3b: "|- RPCFail crCh rmCh rst p & $S3 rmhist p & (S6 rmhist p)$ @@ -687,13 +687,13 @@ --> ReadInner memCh mm (resbar rmhist) p l" apply clarsimp apply (drule S4_excl [temp_use])+ - apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "ReadInner_def", - thm "GoodRead_def", thm "BadRead_def", thm "e_def", thm "c_def", thm "m_def"]) [] [] 1 *}) + apply (tactic {* action_simp_tac (@{simpset} addsimps [@{thm ReadInner_def}, + @{thm GoodRead_def}, @{thm BadRead_def}, @{thm e_def}, @{thm c_def}, @{thm m_def}]) [] [] 1 *}) apply (auto simp: resbar_def) apply (tactic {* ALLGOALS (action_simp_tac - (@{simpset} addsimps [thm "RPCRelayArg_def", thm "MClkRelayArg_def", - thm "S_def", thm "S4_def", thm "RdRequest_def", thm "MemInv_def"]) - [] [thm "impE", thm "MemValNotAResultE"]) *}) + (@{simpset} addsimps [@{thm RPCRelayArg_def}, @{thm MClkRelayArg_def}, + @{thm S_def}, @{thm S4_def}, @{thm RdRequest_def}, @{thm MemInv_def}]) + [] [@{thm impE}, @{thm MemValNotAResultE}]) *}) done lemma Step1_4_4a: "|- Read rmCh mm ires p & $S4 rmhist p & (S4 rmhist p)$ @@ -707,12 +707,12 @@ apply clarsimp apply (drule S4_excl [temp_use])+ apply (tactic {* action_simp_tac (@{simpset} addsimps - [thm "WriteInner_def", thm "GoodWrite_def", thm "BadWrite_def", thm "e_def", - thm "c_def", thm "m_def"]) [] [] 1 *}) + [@{thm WriteInner_def}, @{thm GoodWrite_def}, @{thm BadWrite_def}, @{thm e_def}, + @{thm c_def}, @{thm m_def}]) [] [] 1 *}) apply (auto simp: resbar_def) apply (tactic {* ALLGOALS (action_simp_tac (@{simpset} addsimps - [thm "RPCRelayArg_def", thm "MClkRelayArg_def", thm "S_def", - thm "S4_def", thm "WrRequest_def"]) [] []) *}) + [@{thm RPCRelayArg_def}, @{thm MClkRelayArg_def}, @{thm S_def}, + @{thm S4_def}, @{thm WrRequest_def}]) [] []) *}) done lemma Step1_4_4b: "|- Write rmCh mm ires p l & $S4 rmhist p & (S4 rmhist p)$ @@ -723,10 +723,10 @@ lemma Step1_4_4c: "|- MemReturn rmCh ires p & $S4 rmhist p & (S5 rmhist p)$ & unchanged (e p, c p, r p) --> unchanged (rtrner memCh!p, resbar rmhist!p)" - apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "e_def", - thm "c_def", thm "r_def", thm "resbar_def"]) [] [] 1 *}) + apply (tactic {* action_simp_tac (@{simpset} addsimps [@{thm e_def}, + @{thm c_def}, @{thm r_def}, @{thm resbar_def}]) [] [] 1 *}) apply (drule S4_excl [temp_use] S5_excl [temp_use])+ - apply (tactic {* auto_tac (MI_fast_css addsimps2 [thm "MemReturn_def", thm "Return_def"]) *}) + apply (tactic {* auto_tac (MI_fast_css addsimps2 [@{thm MemReturn_def}, @{thm Return_def}]) *}) done lemma Step1_4_5a: "|- RPCReply crCh rmCh rst p & $S5 rmhist p & (S6 rmhist p)$ @@ -752,12 +752,12 @@ --> MemReturn memCh (resbar rmhist) p" apply clarsimp apply (drule S6_excl [temp_use])+ - apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "e_def", - thm "r_def", thm "m_def", thm "MClkReply_def", thm "MemReturn_def", - thm "Return_def", thm "resbar_def"]) [] [] 1 *}) + apply (tactic {* action_simp_tac (@{simpset} addsimps [@{thm e_def}, + @{thm r_def}, @{thm m_def}, @{thm MClkReply_def}, @{thm MemReturn_def}, + @{thm Return_def}, @{thm resbar_def}]) [] [] 1 *}) apply simp_all (* simplify if-then-else *) apply (tactic {* ALLGOALS (action_simp_tac (@{simpset} addsimps - [thm "MClkReplyVal_def", thm "S6_def", thm "S_def"]) [] [thm "MVOKBARFnotNR"]) *}) + [@{thm MClkReplyVal_def}, @{thm S6_def}, @{thm S_def}]) [] [@{thm MVOKBARFnotNR}]) *}) done lemma Step1_4_6b: "|- MClkRetry memCh crCh cst p & $S6 rmhist p & (S3 rmhist p)$ @@ -765,8 +765,8 @@ --> MemFail memCh (resbar rmhist) p" apply clarsimp apply (drule S3_excl [temp_use])+ - apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "e_def", thm "r_def", - thm "m_def", thm "MClkRetry_def", thm "MemFail_def", thm "resbar_def"]) [] [] 1 *}) + apply (tactic {* action_simp_tac (@{simpset} addsimps [@{thm e_def}, @{thm r_def}, + @{thm m_def}, @{thm MClkRetry_def}, @{thm MemFail_def}, @{thm resbar_def}]) [] [] 1 *}) apply (auto simp: S6_def S_def) done @@ -816,7 +816,7 @@ lemma unchanged_safe: "|- (~unchanged (e p, c p, r p, m p, rmhist!p) --> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)) --> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)" - apply (tactic {* split_idle_tac @{context} [thm "square_def"] 1 *}) + apply (tactic {* split_idle_tac @{context} [@{thm square_def}] 1 *}) apply force done (* turn into (unsafe, looping!) introduction rule *) @@ -898,15 +898,15 @@ lemma S1_RNextdisabled: "|- S1 rmhist p --> ~Enabled (_(rtrner memCh!p, resbar rmhist!p))" - apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "angle_def", - thm "S_def", thm "S1_def"]) [notI] [thm "enabledE", temp_elim (thm "Memoryidle")] 1 *}) + apply (tactic {* action_simp_tac (@{simpset} addsimps [@{thm angle_def}, + @{thm S_def}, @{thm S1_def}]) [notI] [@{thm enabledE}, temp_elim @{thm Memoryidle}] 1 *}) apply force done lemma S1_Returndisabled: "|- S1 rmhist p --> ~Enabled (_(rtrner memCh!p, resbar rmhist!p))" - by (tactic {* action_simp_tac (@{simpset} addsimps [thm "angle_def", thm "MemReturn_def", - thm "Return_def", thm "S_def", thm "S1_def"]) [notI] [thm "enabledE"] 1 *}) + by (tactic {* action_simp_tac (@{simpset} addsimps [@{thm angle_def}, @{thm MemReturn_def}, + @{thm Return_def}, @{thm S_def}, @{thm S1_def}]) [notI] [@{thm enabledE}] 1 *}) lemma RNext_fair: "|- []<>S1 rmhist p --> WF(RNext memCh mm (resbar rmhist) p)_(rtrner memCh!p, resbar rmhist!p)" @@ -986,7 +986,7 @@ & ImpNext p & [HNext rmhist p]_(c p,r p,m p,rmhist!p) & (ALL l. $MemInv mm l) --> (S4 rmhist p & ires!p = #NotAResult)$ | ((S4 rmhist p & ires!p ~= #NotAResult) | S5 rmhist p)$" - apply (tactic {* split_idle_tac @{context} [thm "m_def"] 1 *}) + apply (tactic {* split_idle_tac @{context} [@{thm m_def}] 1 *}) apply (auto dest!: Step1_2_4 [temp_use]) done @@ -1017,7 +1017,7 @@ lemma S4b_successors: "|- $(S4 rmhist p & ires!p ~= #NotAResult) & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) & (ALL l. $MemInv mm l) --> (S4 rmhist p & ires!p ~= #NotAResult)$ | (S5 rmhist p)$" - apply (tactic {* split_idle_tac @{context} [thm "m_def"] 1 *}) + apply (tactic {* split_idle_tac @{context} [@{thm m_def}] 1 *}) apply (auto dest!: WriteResult [temp_use] Step1_2_4 [temp_use] ReadResult [temp_use]) done @@ -1084,16 +1084,16 @@ lemma MClkReplyS6: "|- $ImpInv rmhist p & _(c p) --> $S6 rmhist p" - by (tactic {* action_simp_tac (@{simpset} addsimps [thm "angle_def", - thm "MClkReply_def", thm "Return_def", thm "ImpInv_def", thm "S_def", - thm "S1_def", thm "S2_def", thm "S3_def", thm "S4_def", thm "S5_def"]) [] [] 1 *}) + by (tactic {* action_simp_tac (@{simpset} addsimps [@{thm angle_def}, + @{thm MClkReply_def}, @{thm Return_def}, @{thm ImpInv_def}, @{thm S_def}, + @{thm S1_def}, @{thm S2_def}, @{thm S3_def}, @{thm S4_def}, @{thm S5_def}]) [] [] 1 *}) lemma S6MClkReply_enabled: "|- S6 rmhist p --> Enabled (_(c p))" apply (auto simp: c_def intro!: MClkReply_enabled [temp_use]) apply (cut_tac MI_base) apply (blast dest: base_pair) apply (tactic {* ALLGOALS (action_simp_tac (@{simpset} - addsimps [thm "S_def", thm "S6_def"]) [] []) *}) + addsimps [@{thm S_def}, @{thm S6_def}]) [] []) *}) done lemma S6_live: "|- [](ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) & $(ImpInv rmhist p)) @@ -1104,7 +1104,7 @@ apply (erule InfiniteEnsures) apply assumption apply (tactic {* action_simp_tac @{simpset} [] - (map temp_elim [thm "MClkReplyS6", thm "S6MClkReply_successors"]) 1 *}) + (map temp_elim [@{thm MClkReplyS6}, @{thm S6MClkReply_successors}]) 1 *}) apply (auto simp: SF_def) apply (erule contrapos_np) apply (auto intro!: S6MClkReply_enabled [temp_use] elim!: STL4E [temp_use] DmdImplE [temp_use]) @@ -1191,7 +1191,7 @@ ==> sigma |= []<>S1 rmhist p" apply (rule classical) apply (tactic {* asm_lr_simp_tac (@{simpset} addsimps - [temp_use (thm "NotBox"), temp_rewrite (thm "NotDmd")]) 1 *}) + [temp_use @{thm NotBox}, temp_rewrite @{thm NotDmd}]) 1 *}) apply (auto elim!: leadsto_infinite [temp_use] mp dest!: DBImplBD [temp_use]) done diff -r e6b96b4cde7e -r 0dec18004e75 src/HOL/TLA/Memory/RPC.thy --- a/src/HOL/TLA/Memory/RPC.thy Mon Sep 06 19:11:01 2010 +0200 +++ b/src/HOL/TLA/Memory/RPC.thy Mon Sep 06 19:13:10 2010 +0200 @@ -103,15 +103,15 @@ (* Enabledness of some actions *) lemma RPCFail_enabled: "!!p. basevars (rtrner send!p, caller rcv!p, rst!p) ==> |- ~Calling rcv p & Calling send p --> Enabled (RPCFail send rcv rst p)" - by (tactic {* action_simp_tac (@{simpset} addsimps [thm "RPCFail_def", - thm "Return_def", thm "caller_def", thm "rtrner_def"]) [exI] - [thm "base_enabled", thm "Pair_inject"] 1 *}) + by (tactic {* action_simp_tac (@{simpset} addsimps [@{thm RPCFail_def}, + @{thm Return_def}, @{thm caller_def}, @{thm rtrner_def}]) [exI] + [@{thm base_enabled}, @{thm Pair_inject}] 1 *}) lemma RPCReply_enabled: "!!p. basevars (rtrner send!p, caller rcv!p, rst!p) ==> |- ~Calling rcv p & Calling send p & rst!p = #rpcB --> Enabled (RPCReply send rcv rst p)" - by (tactic {* action_simp_tac (@{simpset} addsimps [thm "RPCReply_def", - thm "Return_def", thm "caller_def", thm "rtrner_def"]) [exI] - [thm "base_enabled", thm "Pair_inject"] 1 *}) + by (tactic {* action_simp_tac (@{simpset} addsimps [@{thm RPCReply_def}, + @{thm Return_def}, @{thm caller_def}, @{thm rtrner_def}]) [exI] + [@{thm base_enabled}, @{thm Pair_inject}] 1 *}) end diff -r e6b96b4cde7e -r 0dec18004e75 src/HOL/Tools/Qelim/cooper.ML --- a/src/HOL/Tools/Qelim/cooper.ML Mon Sep 06 19:11:01 2010 +0200 +++ b/src/HOL/Tools/Qelim/cooper.ML Mon Sep 06 19:13:10 2010 +0200 @@ -423,7 +423,7 @@ val emptyIS = @{cterm "{}::int set"}; val insert_tm = @{cterm "insert :: int => _"}; fun mkISet cts = fold_rev (Thm.capply insert_tm #> Thm.capply) cts emptyIS; -val eqelem_imp_imp = (thm"eqelem_imp_iff") RS iffD1; +val eqelem_imp_imp = @{thm eqelem_imp_iff} RS iffD1; val [A_tm,B_tm] = map (fn th => cprop_of th |> funpow 2 Thm.dest_arg |> Thm.dest_abs NONE |> snd |> Thm.dest_arg1 |> Thm.dest_arg |> Thm.dest_abs NONE |> snd |> Thm.dest_fun |> Thm.dest_arg) [asetP,bsetP]; diff -r e6b96b4cde7e -r 0dec18004e75 src/HOL/Tools/TFL/casesplit.ML --- a/src/HOL/Tools/TFL/casesplit.ML Mon Sep 06 19:11:01 2010 +0200 +++ b/src/HOL/Tools/TFL/casesplit.ML Mon Sep 06 19:13:10 2010 +0200 @@ -32,9 +32,9 @@ val dest_Trueprop = HOLogic.dest_Trueprop; val mk_Trueprop = HOLogic.mk_Trueprop; -val atomize = thms "induct_atomize"; -val rulify = thms "induct_rulify"; -val rulify_fallback = thms "induct_rulify_fallback"; +val atomize = @{thms induct_atomize}; +val rulify = @{thms induct_rulify}; +val rulify_fallback = @{thms induct_rulify_fallback}; end; diff -r e6b96b4cde7e -r 0dec18004e75 src/HOL/Tools/TFL/thms.ML --- a/src/HOL/Tools/TFL/thms.ML Mon Sep 06 19:11:01 2010 +0200 +++ b/src/HOL/Tools/TFL/thms.ML Mon Sep 06 19:13:10 2010 +0200 @@ -1,20 +1,19 @@ (* Title: HOL/Tools/TFL/thms.ML - ID: $Id$ Author: Konrad Slind, Cambridge University Computer Laboratory Copyright 1997 University of Cambridge *) structure Thms = struct - val WFREC_COROLLARY = thm "tfl_wfrec"; - val WF_INDUCTION_THM = thm "tfl_wf_induct"; - val CUT_DEF = thm "cut_def"; - val eqT = thm "tfl_eq_True"; - val rev_eq_mp = thm "tfl_rev_eq_mp"; - val simp_thm = thm "tfl_simp_thm"; - val P_imp_P_iff_True = thm "tfl_P_imp_P_iff_True"; - val imp_trans = thm "tfl_imp_trans"; - val disj_assoc = thm "tfl_disj_assoc"; - val tfl_disjE = thm "tfl_disjE"; - val choose_thm = thm "tfl_exE"; + val WFREC_COROLLARY = @{thm tfl_wfrec}; + val WF_INDUCTION_THM = @{thm tfl_wf_induct}; + val CUT_DEF = @{thm cut_def}; + val eqT = @{thm tfl_eq_True}; + val rev_eq_mp = @{thm tfl_rev_eq_mp}; + val simp_thm = @{thm tfl_simp_thm}; + val P_imp_P_iff_True = @{thm tfl_P_imp_P_iff_True}; + val imp_trans = @{thm tfl_imp_trans}; + val disj_assoc = @{thm tfl_disj_assoc}; + val tfl_disjE = @{thm tfl_disjE}; + val choose_thm = @{thm tfl_exE}; end; diff -r e6b96b4cde7e -r 0dec18004e75 src/HOL/Tools/meson.ML --- a/src/HOL/Tools/meson.ML Mon Sep 06 19:11:01 2010 +0200 +++ b/src/HOL/Tools/meson.ML Mon Sep 06 19:13:10 2010 +0200 @@ -68,24 +68,24 @@ val ex_forward = @{thm ex_forward}; val choice = @{thm choice}; -val not_conjD = thm "meson_not_conjD"; -val not_disjD = thm "meson_not_disjD"; -val not_notD = thm "meson_not_notD"; -val not_allD = thm "meson_not_allD"; -val not_exD = thm "meson_not_exD"; -val imp_to_disjD = thm "meson_imp_to_disjD"; -val not_impD = thm "meson_not_impD"; -val iff_to_disjD = thm "meson_iff_to_disjD"; -val not_iffD = thm "meson_not_iffD"; -val conj_exD1 = thm "meson_conj_exD1"; -val conj_exD2 = thm "meson_conj_exD2"; -val disj_exD = thm "meson_disj_exD"; -val disj_exD1 = thm "meson_disj_exD1"; -val disj_exD2 = thm "meson_disj_exD2"; -val disj_assoc = thm "meson_disj_assoc"; -val disj_comm = thm "meson_disj_comm"; -val disj_FalseD1 = thm "meson_disj_FalseD1"; -val disj_FalseD2 = thm "meson_disj_FalseD2"; +val not_conjD = @{thm meson_not_conjD}; +val not_disjD = @{thm meson_not_disjD}; +val not_notD = @{thm meson_not_notD}; +val not_allD = @{thm meson_not_allD}; +val not_exD = @{thm meson_not_exD}; +val imp_to_disjD = @{thm meson_imp_to_disjD}; +val not_impD = @{thm meson_not_impD}; +val iff_to_disjD = @{thm meson_iff_to_disjD}; +val not_iffD = @{thm meson_not_iffD}; +val conj_exD1 = @{thm meson_conj_exD1}; +val conj_exD2 = @{thm meson_conj_exD2}; +val disj_exD = @{thm meson_disj_exD}; +val disj_exD1 = @{thm meson_disj_exD1}; +val disj_exD2 = @{thm meson_disj_exD2}; +val disj_assoc = @{thm meson_disj_assoc}; +val disj_comm = @{thm meson_disj_comm}; +val disj_FalseD1 = @{thm meson_disj_FalseD1}; +val disj_FalseD2 = @{thm meson_disj_FalseD2}; (**** Operators for forward proof ****) @@ -203,7 +203,7 @@ (*They are typically functional reflexivity axioms and are the converses of injectivity equivalences*) -val not_refl_disj_D = thm"meson_not_refl_disj_D"; +val not_refl_disj_D = @{thm meson_not_refl_disj_D}; (*Is either term a Var that does not properly occur in the other term?*) fun eliminable (t as Var _, u) = t aconv u orelse not (Logic.occs(t,u)) diff -r e6b96b4cde7e -r 0dec18004e75 src/HOL/UNITY/Comp/Alloc.thy --- a/src/HOL/UNITY/Comp/Alloc.thy Mon Sep 06 19:11:01 2010 +0200 +++ b/src/HOL/UNITY/Comp/Alloc.thy Mon Sep 06 19:13:10 2010 +0200 @@ -426,7 +426,7 @@ apply (rule fst_o_funPair) done -ML {* bind_thms ("fst_o_client_map'", make_o_equivs (thm "fst_o_client_map")) *} +ML {* bind_thms ("fst_o_client_map'", make_o_equivs @{thm fst_o_client_map}) *} declare fst_o_client_map' [simp] lemma snd_o_client_map: "snd o client_map = clientState_d.dummy" @@ -434,7 +434,7 @@ apply (rule snd_o_funPair) done -ML {* bind_thms ("snd_o_client_map'", make_o_equivs (thm "snd_o_client_map")) *} +ML {* bind_thms ("snd_o_client_map'", make_o_equivs @{thm snd_o_client_map}) *} declare snd_o_client_map' [simp] @@ -444,28 +444,28 @@ apply record_auto done -ML {* bind_thms ("client_o_sysOfAlloc'", make_o_equivs (thm "client_o_sysOfAlloc")) *} +ML {* bind_thms ("client_o_sysOfAlloc'", make_o_equivs @{thm client_o_sysOfAlloc}) *} declare client_o_sysOfAlloc' [simp] lemma allocGiv_o_sysOfAlloc_eq: "allocGiv o sysOfAlloc = allocGiv" apply record_auto done -ML {* bind_thms ("allocGiv_o_sysOfAlloc_eq'", make_o_equivs (thm "allocGiv_o_sysOfAlloc_eq")) *} +ML {* bind_thms ("allocGiv_o_sysOfAlloc_eq'", make_o_equivs @{thm allocGiv_o_sysOfAlloc_eq}) *} declare allocGiv_o_sysOfAlloc_eq' [simp] lemma allocAsk_o_sysOfAlloc_eq: "allocAsk o sysOfAlloc = allocAsk" apply record_auto done -ML {* bind_thms ("allocAsk_o_sysOfAlloc_eq'", make_o_equivs (thm "allocAsk_o_sysOfAlloc_eq")) *} +ML {* bind_thms ("allocAsk_o_sysOfAlloc_eq'", make_o_equivs @{thm allocAsk_o_sysOfAlloc_eq}) *} declare allocAsk_o_sysOfAlloc_eq' [simp] lemma allocRel_o_sysOfAlloc_eq: "allocRel o sysOfAlloc = allocRel" apply record_auto done -ML {* bind_thms ("allocRel_o_sysOfAlloc_eq'", make_o_equivs (thm "allocRel_o_sysOfAlloc_eq")) *} +ML {* bind_thms ("allocRel_o_sysOfAlloc_eq'", make_o_equivs @{thm allocRel_o_sysOfAlloc_eq}) *} declare allocRel_o_sysOfAlloc_eq' [simp] @@ -475,49 +475,49 @@ apply record_auto done -ML {* bind_thms ("client_o_sysOfClient'", make_o_equivs (thm "client_o_sysOfClient")) *} +ML {* bind_thms ("client_o_sysOfClient'", make_o_equivs @{thm client_o_sysOfClient}) *} declare client_o_sysOfClient' [simp] lemma allocGiv_o_sysOfClient_eq: "allocGiv o sysOfClient = allocGiv o snd " apply record_auto done -ML {* bind_thms ("allocGiv_o_sysOfClient_eq'", make_o_equivs (thm "allocGiv_o_sysOfClient_eq")) *} +ML {* bind_thms ("allocGiv_o_sysOfClient_eq'", make_o_equivs @{thm allocGiv_o_sysOfClient_eq}) *} declare allocGiv_o_sysOfClient_eq' [simp] lemma allocAsk_o_sysOfClient_eq: "allocAsk o sysOfClient = allocAsk o snd " apply record_auto done -ML {* bind_thms ("allocAsk_o_sysOfClient_eq'", make_o_equivs (thm "allocAsk_o_sysOfClient_eq")) *} +ML {* bind_thms ("allocAsk_o_sysOfClient_eq'", make_o_equivs @{thm allocAsk_o_sysOfClient_eq}) *} declare allocAsk_o_sysOfClient_eq' [simp] lemma allocRel_o_sysOfClient_eq: "allocRel o sysOfClient = allocRel o snd " apply record_auto done -ML {* bind_thms ("allocRel_o_sysOfClient_eq'", make_o_equivs (thm "allocRel_o_sysOfClient_eq")) *} +ML {* bind_thms ("allocRel_o_sysOfClient_eq'", make_o_equivs @{thm allocRel_o_sysOfClient_eq}) *} declare allocRel_o_sysOfClient_eq' [simp] lemma allocGiv_o_inv_sysOfAlloc_eq: "allocGiv o inv sysOfAlloc = allocGiv" apply (simp add: o_def) done -ML {* bind_thms ("allocGiv_o_inv_sysOfAlloc_eq'", make_o_equivs (thm "allocGiv_o_inv_sysOfAlloc_eq")) *} +ML {* bind_thms ("allocGiv_o_inv_sysOfAlloc_eq'", make_o_equivs @{thm allocGiv_o_inv_sysOfAlloc_eq}) *} declare allocGiv_o_inv_sysOfAlloc_eq' [simp] lemma allocAsk_o_inv_sysOfAlloc_eq: "allocAsk o inv sysOfAlloc = allocAsk" apply (simp add: o_def) done -ML {* bind_thms ("allocAsk_o_inv_sysOfAlloc_eq'", make_o_equivs (thm "allocAsk_o_inv_sysOfAlloc_eq")) *} +ML {* bind_thms ("allocAsk_o_inv_sysOfAlloc_eq'", make_o_equivs @{thm allocAsk_o_inv_sysOfAlloc_eq}) *} declare allocAsk_o_inv_sysOfAlloc_eq' [simp] lemma allocRel_o_inv_sysOfAlloc_eq: "allocRel o inv sysOfAlloc = allocRel" apply (simp add: o_def) done -ML {* bind_thms ("allocRel_o_inv_sysOfAlloc_eq'", make_o_equivs (thm "allocRel_o_inv_sysOfAlloc_eq")) *} +ML {* bind_thms ("allocRel_o_inv_sysOfAlloc_eq'", make_o_equivs @{thm allocRel_o_inv_sysOfAlloc_eq}) *} declare allocRel_o_inv_sysOfAlloc_eq' [simp] lemma rel_inv_client_map_drop_map: "(rel o inv client_map o drop_map i o inv sysOfClient) = @@ -525,7 +525,7 @@ apply (simp add: o_def drop_map_def) done -ML {* bind_thms ("rel_inv_client_map_drop_map'", make_o_equivs (thm "rel_inv_client_map_drop_map")) *} +ML {* bind_thms ("rel_inv_client_map_drop_map'", make_o_equivs @{thm rel_inv_client_map_drop_map}) *} declare rel_inv_client_map_drop_map [simp] lemma ask_inv_client_map_drop_map: "(ask o inv client_map o drop_map i o inv sysOfClient) = @@ -533,7 +533,7 @@ apply (simp add: o_def drop_map_def) done -ML {* bind_thms ("ask_inv_client_map_drop_map'", make_o_equivs (thm "ask_inv_client_map_drop_map")) *} +ML {* bind_thms ("ask_inv_client_map_drop_map'", make_o_equivs @{thm ask_inv_client_map_drop_map}) *} declare ask_inv_client_map_drop_map [simp] @@ -812,7 +812,7 @@ ML {* -bind_thms ("System_Increasing'", list_of_Int (thm "System_Increasing")) +bind_thms ("System_Increasing'", list_of_Int @{thm System_Increasing}) *} declare System_Increasing' [intro!] @@ -903,9 +903,9 @@ text{*safety (1), step 4 (final result!) *} theorem System_safety: "System : system_safety" apply (unfold system_safety_def) - apply (tactic {* rtac (Always_Int_rule [thm "System_sum_bounded", - thm "Always_tokens_giv_le_allocGiv", thm "Always_tokens_allocRel_le_rel"] RS - thm "Always_weaken") 1 *}) + apply (tactic {* rtac (Always_Int_rule [@{thm System_sum_bounded}, + @{thm Always_tokens_giv_le_allocGiv}, @{thm Always_tokens_allocRel_le_rel}] RS + @{thm Always_weaken}) 1 *}) apply auto apply (rule setsum_fun_mono [THEN order_trans]) apply (drule_tac [2] order_trans) @@ -946,8 +946,8 @@ lemma System_Bounded_allocAsk: "System : Always {s. ALL i NbT}" apply (auto simp add: Collect_all_imp_eq) - apply (tactic {* rtac (Always_Int_rule [thm "Always_allocAsk_le_ask", - thm "System_Bounded_ask"] RS thm "Always_weaken") 1 *}) + apply (tactic {* rtac (Always_Int_rule [@{thm Always_allocAsk_le_ask}, + @{thm System_Bounded_ask}] RS @{thm Always_weaken}) 1 *}) apply (auto dest: set_mono) done diff -r e6b96b4cde7e -r 0dec18004e75 src/HOLCF/FOCUS/Fstream.thy --- a/src/HOLCF/FOCUS/Fstream.thy Mon Sep 06 19:11:01 2010 +0200 +++ b/src/HOLCF/FOCUS/Fstream.thy Mon Sep 06 19:13:10 2010 +0200 @@ -156,12 +156,12 @@ lemma slen_fscons_eq_rev: "(#x < Fin (Suc (Suc n))) = (!a y. x ~= a~> y | #y < Fin (Suc n))" apply (simp add: fscons_def2 slen_scons_eq_rev) -apply (tactic {* step_tac (HOL_cs addSEs [thm "DefE"]) 1 *}) -apply (tactic {* step_tac (HOL_cs addSEs [thm "DefE"]) 1 *}) -apply (tactic {* step_tac (HOL_cs addSEs [thm "DefE"]) 1 *}) -apply (tactic {* step_tac (HOL_cs addSEs [thm "DefE"]) 1 *}) -apply (tactic {* step_tac (HOL_cs addSEs [thm "DefE"]) 1 *}) -apply (tactic {* step_tac (HOL_cs addSEs [thm "DefE"]) 1 *}) +apply (tactic {* step_tac (HOL_cs addSEs @{thms DefE}) 1 *}) +apply (tactic {* step_tac (HOL_cs addSEs @{thms DefE}) 1 *}) +apply (tactic {* step_tac (HOL_cs addSEs @{thms DefE}) 1 *}) +apply (tactic {* step_tac (HOL_cs addSEs @{thms DefE}) 1 *}) +apply (tactic {* step_tac (HOL_cs addSEs @{thms DefE}) 1 *}) +apply (tactic {* step_tac (HOL_cs addSEs @{thms DefE}) 1 *}) apply (erule contrapos_np) apply (fast dest: not_Undef_is_Def [THEN iffD1] elim: DefE) done diff -r e6b96b4cde7e -r 0dec18004e75 src/HOLCF/IOA/ABP/Correctness.thy --- a/src/HOLCF/IOA/ABP/Correctness.thy Mon Sep 06 19:11:01 2010 +0200 +++ b/src/HOLCF/IOA/ABP/Correctness.thy Mon Sep 06 19:13:10 2010 +0200 @@ -164,16 +164,16 @@ lemma sender_abstraction: "is_weak_ref_map reduce srch_ioa srch_fin_ioa" apply (tactic {* - simp_tac (HOL_ss addsimps [thm "srch_fin_ioa_def", thm "rsch_fin_ioa_def", - thm "srch_ioa_def", thm "rsch_ioa_def", thm "rename_through_pmap", - thm "channel_abstraction"]) 1 *}) + simp_tac (HOL_ss addsimps [@{thm srch_fin_ioa_def}, @{thm rsch_fin_ioa_def}, + @{thm srch_ioa_def}, @{thm rsch_ioa_def}, @{thm rename_through_pmap}, + @{thm channel_abstraction}]) 1 *}) done lemma receiver_abstraction: "is_weak_ref_map reduce rsch_ioa rsch_fin_ioa" apply (tactic {* - simp_tac (HOL_ss addsimps [thm "srch_fin_ioa_def", thm "rsch_fin_ioa_def", - thm "srch_ioa_def", thm "rsch_ioa_def", thm "rename_through_pmap", - thm "channel_abstraction"]) 1 *}) + simp_tac (HOL_ss addsimps [@{thm srch_fin_ioa_def}, @{thm rsch_fin_ioa_def}, + @{thm srch_ioa_def}, @{thm rsch_ioa_def}, @{thm rename_through_pmap}, + @{thm channel_abstraction}]) 1 *}) done diff -r e6b96b4cde7e -r 0dec18004e75 src/HOLCF/IOA/meta_theory/CompoScheds.thy --- a/src/HOLCF/IOA/meta_theory/CompoScheds.thy Mon Sep 06 19:11:01 2010 +0200 +++ b/src/HOLCF/IOA/meta_theory/CompoScheds.thy Mon Sep 06 19:13:10 2010 +0200 @@ -289,9 +289,9 @@ ML {* local - val defs = [thm "Filter_def", thm "Forall_def", thm "sforall_def", thm "mkex_def", - thm "stutter_def"] - val asigs = [thm "asig_of_par", thm "actions_asig_comp"] + val defs = [@{thm Filter_def}, @{thm Forall_def}, @{thm sforall_def}, @{thm mkex_def}, + @{thm stutter_def}] + val asigs = [@{thm asig_of_par}, @{thm actions_asig_comp}] in fun mkex_induct_tac ctxt sch exA exB = diff -r e6b96b4cde7e -r 0dec18004e75 src/HOLCF/IOA/meta_theory/SimCorrectness.thy --- a/src/HOLCF/IOA/meta_theory/SimCorrectness.thy Mon Sep 06 19:11:01 2010 +0200 +++ b/src/HOLCF/IOA/meta_theory/SimCorrectness.thy Mon Sep 06 19:13:10 2010 +0200 @@ -171,7 +171,7 @@ !s s'. reachable C s & is_exec_frag C (s,ex) & (s,s'): R --> mk_trace C$ex = mk_trace A$((corresp_ex_simC A R$ex) s')" -apply (tactic {* pair_induct_tac @{context} "ex" [thm "is_exec_frag_def"] 1 *}) +apply (tactic {* pair_induct_tac @{context} "ex" [@{thm is_exec_frag_def}] 1 *}) (* cons case *) apply auto apply (rename_tac ex a t s s') diff -r e6b96b4cde7e -r 0dec18004e75 src/HOLCF/ex/Focus_ex.thy --- a/src/HOLCF/ex/Focus_ex.thy Mon Sep 06 19:11:01 2010 +0200 +++ b/src/HOLCF/ex/Focus_ex.thy Mon Sep 06 19:13:10 2010 +0200 @@ -180,7 +180,7 @@ done lemma lemma3: "def_g(g) --> is_g(g)" -apply (tactic {* simp_tac (HOL_ss addsimps [thm "def_g_def", thm "lemma1", thm "lemma2"]) 1 *}) +apply (tactic {* simp_tac (HOL_ss addsimps [@{thm def_g_def}, @{thm lemma1}, @{thm lemma2}]) 1 *}) apply (rule impI) apply (erule exE) apply (rule_tac x = "f" in exI) @@ -205,7 +205,7 @@ lemma lemma4: "is_g(g) --> def_g(g)" apply (tactic {* simp_tac (HOL_ss delsimps (@{thms HOL.ex_simps} @ @{thms HOL.all_simps}) - addsimps [thm "lemma1", thm "lemma2", thm "def_g_def"]) 1 *}) + addsimps [@{thm lemma1}, @{thm lemma2}, @{thm def_g_def}]) 1 *}) apply (rule impI) apply (erule exE) apply (rule_tac x = "f" in exI) diff -r e6b96b4cde7e -r 0dec18004e75 src/HOLCF/ex/Loop.thy --- a/src/HOLCF/ex/Loop.thy Mon Sep 06 19:11:01 2010 +0200 +++ b/src/HOLCF/ex/Loop.thy Mon Sep 06 19:13:10 2010 +0200 @@ -104,12 +104,12 @@ apply (simp (no_asm) add: step_def2) apply (rule_tac p = "b$ (iterate n$ (step$b$g) $x) " in trE) apply (erule notE) -apply (tactic {* asm_simp_tac (HOLCF_ss addsimps [thm "step_def2"]) 1 *}) +apply (tactic {* asm_simp_tac (HOLCF_ss addsimps [@{thm step_def2}]) 1 *}) apply (tactic "asm_simp_tac HOLCF_ss 1") apply (rule mp) apply (erule spec) -apply (tactic {* asm_simp_tac (HOLCF_ss delsimps [thm "iterate_Suc"] - addsimps [thm "loop_lemma2"]) 1 *}) +apply (tactic {* asm_simp_tac (HOLCF_ss delsimps [@{thm iterate_Suc}] + addsimps [@{thm loop_lemma2}]) 1 *}) apply (rule_tac s = "iterate (Suc n) $ (step$b$g) $x" and t = "g$ (iterate n$ (step$b$g) $x) " in ssubst) prefer 2 apply (assumption) diff -r e6b96b4cde7e -r 0dec18004e75 src/Provers/quasi.ML --- a/src/Provers/quasi.ML Mon Sep 06 19:11:01 2010 +0200 +++ b/src/Provers/quasi.ML Mon Sep 06 19:13:10 2010 +0200 @@ -149,7 +149,7 @@ | "~=" => if (x aconv y) then raise Contr (Thm ([(Thm ([(Thm ([], Less.le_refl)) ,(Asm n)], Less.le_neq_trans))], Less.less_reflE)) else [ NotEq (x, y, Asm n), - NotEq (y, x,Thm ( [Asm n], thm "not_sym"))] + NotEq (y, x,Thm ( [Asm n], @{thm not_sym}))] | _ => error ("quasi_tac: unknown relation symbol ``" ^ rel ^ "''returned by decomp_quasi.")) | NONE => []; @@ -300,7 +300,7 @@ let val leEdge = Le (x,y, Thm ([p], Less.less_imp_le)) val neqEdges = [ NotEq (x,y, Thm ([p], Less.less_imp_neq)), - NotEq (y,x, Thm ( [Thm ([p], Less.less_imp_neq)], thm "not_sym"))] + NotEq (y,x, Thm ( [Thm ([p], Less.less_imp_neq)], @{thm not_sym}))] in buildGraphs (ls, addEdge(y,[],(addEdge (x,[(y,leEdge)],leG))), neqEdges@neqE) end @@ -459,9 +459,10 @@ let fun findParallelNeq [] = NONE | findParallelNeq (e::es) = - if (x aconv (lower e) andalso y aconv (upper e)) then SOME e - else if (y aconv (lower e) andalso x aconv (upper e)) then SOME (NotEq (x,y, (Thm ([getprf e], thm "not_sym")))) - else findParallelNeq es ; + if (x aconv (lower e) andalso y aconv (upper e)) then SOME e + else if (y aconv (lower e) andalso x aconv (upper e)) + then SOME (NotEq (x,y, (Thm ([getprf e], @{thm not_sym})))) + else findParallelNeq es; in (* test if there is a edge x ~= y respectivly y ~= x and *) (* if it possible to find a path x <= y in leG, thus we can conclude x < y *) @@ -483,7 +484,7 @@ (case (Library.find_first (fn fact => fact subsumes subgoal) neqE, subgoal) of (SOME (NotEq (x, y, p)), NotEq (x', y', _)) => if (x aconv x' andalso y aconv y') then p - else Thm ([p], thm "not_sym") + else Thm ([p], @{thm not_sym}) | _ => raise Cannot ) diff -r e6b96b4cde7e -r 0dec18004e75 src/Sequents/ILL.thy --- a/src/Sequents/ILL.thy Mon Sep 06 19:11:01 2010 +0200 +++ b/src/Sequents/ILL.thy Mon Sep 06 19:13:10 2010 +0200 @@ -126,24 +126,16 @@ ML {* - val lazy_cs = empty_pack - add_safes [thm "tensl", thm "conjr", thm "disjl", thm "promote0", - thm "context2", thm "context3"] - add_unsafes [thm "identity", thm "zerol", thm "conjll", thm "conjlr", - thm "disjrl", thm "disjrr", thm "impr", thm "tensr", thm "impl", - thm "derelict", thm "weaken", thm "promote1", thm "promote2", - thm "context1", thm "context4a", thm "context4b"]; + add_safes [@{thm tensl}, @{thm conjr}, @{thm disjl}, @{thm promote0}, + @{thm context2}, @{thm context3}] + add_unsafes [@{thm identity}, @{thm zerol}, @{thm conjll}, @{thm conjlr}, + @{thm disjrl}, @{thm disjrr}, @{thm impr}, @{thm tensr}, @{thm impl}, + @{thm derelict}, @{thm weaken}, @{thm promote1}, @{thm promote2}, + @{thm context1}, @{thm context4a}, @{thm context4b}]; -local - val promote0 = thm "promote0" - val promote1 = thm "promote1" - val promote2 = thm "promote2" -in - -fun prom_tac n = REPEAT (resolve_tac [promote0,promote1,promote2] n) - -end +fun prom_tac n = + REPEAT (resolve_tac [@{thm promote0}, @{thm promote1}, @{thm promote2}] n) *} method_setup best_lazy = @@ -272,13 +264,12 @@ done ML {* +val safe_cs = lazy_cs add_safes [@{thm conj_lemma}, @{thm ll_mp}, @{thm contrad1}, + @{thm contrad2}, @{thm mp_rule1}, @{thm mp_rule2}, @{thm o_a_rule}, + @{thm a_not_a_rule}] + add_unsafes [@{thm aux_impl}]; -val safe_cs = lazy_cs add_safes [thm "conj_lemma", thm "ll_mp", thm "contrad1", - thm "contrad2", thm "mp_rule1", thm "mp_rule2", thm "o_a_rule", - thm "a_not_a_rule"] - add_unsafes [thm "aux_impl"]; - -val power_cs = safe_cs add_unsafes [thm "impr_contr_der"]; +val power_cs = safe_cs add_unsafes [@{thm impr_contr_der}]; *} diff -r e6b96b4cde7e -r 0dec18004e75 src/Sequents/LK0.thy --- a/src/Sequents/LK0.thy Mon Sep 06 19:11:01 2010 +0200 +++ b/src/Sequents/LK0.thy Mon Sep 06 19:13:10 2010 +0200 @@ -210,27 +210,19 @@ ML {* val prop_pack = empty_pack add_safes - [thm "basic", thm "refl", thm "TrueR", thm "FalseL", - thm "conjL", thm "conjR", thm "disjL", thm "disjR", thm "impL", thm "impR", - thm "notL", thm "notR", thm "iffL", thm "iffR"]; + [@{thm basic}, @{thm refl}, @{thm TrueR}, @{thm FalseL}, + @{thm conjL}, @{thm conjR}, @{thm disjL}, @{thm disjR}, @{thm impL}, @{thm impR}, + @{thm notL}, @{thm notR}, @{thm iffL}, @{thm iffR}]; -val LK_pack = prop_pack add_safes [thm "allR", thm "exL"] - add_unsafes [thm "allL_thin", thm "exR_thin", thm "the_equality"]; +val LK_pack = prop_pack add_safes [@{thm allR}, @{thm exL}] + add_unsafes [@{thm allL_thin}, @{thm exR_thin}, @{thm the_equality}]; -val LK_dup_pack = prop_pack add_safes [thm "allR", thm "exL"] - add_unsafes [thm "allL", thm "exR", thm "the_equality"]; +val LK_dup_pack = prop_pack add_safes [@{thm allR}, @{thm exL}] + add_unsafes [@{thm allL}, @{thm exR}, @{thm the_equality}]; -local - val thinR = thm "thinR" - val thinL = thm "thinL" - val cut = thm "cut" -in - fun lemma_tac th i = - rtac (thinR RS cut) i THEN REPEAT (rtac thinL i) THEN rtac th i; - -end; + rtac (@{thm thinR} RS @{thm cut}) i THEN REPEAT (rtac @{thm thinL} i) THEN rtac th i; *} method_setup fast_prop = @@ -321,10 +313,10 @@ (** Equality **) lemma sym: "|- a=b --> b=a" - by (tactic {* safe_tac (LK_pack add_safes [thm "subst"]) 1 *}) + by (tactic {* safe_tac (LK_pack add_safes [@{thm subst}]) 1 *}) lemma trans: "|- a=b --> b=c --> a=c" - by (tactic {* safe_tac (LK_pack add_safes [thm "subst"]) 1 *}) + by (tactic {* safe_tac (LK_pack add_safes [@{thm subst}]) 1 *}) (* Symmetry of equality in hypotheses *) lemmas symL = sym [THEN L_of_imp, standard] diff -r e6b96b4cde7e -r 0dec18004e75 src/Sequents/S4.thy --- a/src/Sequents/S4.thy Mon Sep 06 19:11:01 2010 +0200 +++ b/src/Sequents/S4.thy Mon Sep 06 19:13:10 2010 +0200 @@ -34,12 +34,12 @@ ML {* structure S4_Prover = Modal_ProverFun ( - val rewrite_rls = thms "rewrite_rls" - val safe_rls = thms "safe_rls" - val unsafe_rls = thms "unsafe_rls" @ [thm "boxR", thm "diaL"] - val bound_rls = thms "bound_rls" @ [thm "boxL", thm "diaR"] - val aside_rls = [thm "lstar0", thm "lstar1", thm "lstar2", thm "rstar0", - thm "rstar1", thm "rstar2"] + val rewrite_rls = @{thms rewrite_rls} + val safe_rls = @{thms safe_rls} + val unsafe_rls = @{thms unsafe_rls} @ [@{thm boxR}, @{thm diaL}] + val bound_rls = @{thms bound_rls} @ [@{thm boxL}, @{thm diaR}] + val aside_rls = [@{thm lstar0}, @{thm lstar1}, @{thm lstar2}, @{thm rstar0}, + @{thm rstar1}, @{thm rstar2}] ) *} diff -r e6b96b4cde7e -r 0dec18004e75 src/Sequents/S43.thy --- a/src/Sequents/S43.thy Mon Sep 06 19:11:01 2010 +0200 +++ b/src/Sequents/S43.thy Mon Sep 06 19:13:10 2010 +0200 @@ -79,12 +79,12 @@ ML {* structure S43_Prover = Modal_ProverFun ( - val rewrite_rls = thms "rewrite_rls" - val safe_rls = thms "safe_rls" - val unsafe_rls = thms "unsafe_rls" @ [thm "pi1", thm "pi2"] - val bound_rls = thms "bound_rls" @ [thm "boxL", thm "diaR"] - val aside_rls = [thm "lstar0", thm "lstar1", thm "lstar2", thm "rstar0", - thm "rstar1", thm "rstar2", thm "S43pi0", thm "S43pi1", thm "S43pi2"] + val rewrite_rls = @{thms rewrite_rls} + val safe_rls = @{thms safe_rls} + val unsafe_rls = @{thms unsafe_rls} @ [@{thm pi1}, @{thm pi2}] + val bound_rls = @{thms bound_rls} @ [@{thm boxL}, @{thm diaR}] + val aside_rls = [@{thm lstar0}, @{thm lstar1}, @{thm lstar2}, @{thm rstar0}, + @{thm rstar1}, @{thm rstar2}, @{thm S43pi0}, @{thm S43pi1}, @{thm S43pi2}] ) *} diff -r e6b96b4cde7e -r 0dec18004e75 src/Sequents/T.thy --- a/src/Sequents/T.thy Mon Sep 06 19:11:01 2010 +0200 +++ b/src/Sequents/T.thy Mon Sep 06 19:13:10 2010 +0200 @@ -33,12 +33,12 @@ ML {* structure T_Prover = Modal_ProverFun ( - val rewrite_rls = thms "rewrite_rls" - val safe_rls = thms "safe_rls" - val unsafe_rls = thms "unsafe_rls" @ [thm "boxR", thm "diaL"] - val bound_rls = thms "bound_rls" @ [thm "boxL", thm "diaR"] - val aside_rls = [thm "lstar0", thm "lstar1", thm "lstar2", thm "rstar0", - thm "rstar1", thm "rstar2"] + val rewrite_rls = @{thms rewrite_rls} + val safe_rls = @{thms safe_rls} + val unsafe_rls = @{thms unsafe_rls} @ [@{thm boxR}, @{thm diaL}] + val bound_rls = @{thms bound_rls} @ [@{thm boxL}, @{thm diaR}] + val aside_rls = [@{thm lstar0}, @{thm lstar1}, @{thm lstar2}, @{thm rstar0}, + @{thm rstar1}, @{thm rstar2}] ) *} diff -r e6b96b4cde7e -r 0dec18004e75 src/Sequents/Washing.thy --- a/src/Sequents/Washing.thy Mon Sep 06 19:11:01 2010 +0200 +++ b/src/Sequents/Washing.thy Mon Sep 06 19:13:10 2010 +0200 @@ -33,27 +33,27 @@ (* "activate" definitions for use in proof *) -ML {* bind_thms ("changeI", [thm "context1"] RL ([thm "change"] RLN (2,[thm "cut"]))) *} -ML {* bind_thms ("load1I", [thm "context1"] RL ([thm "load1"] RLN (2,[thm "cut"]))) *} -ML {* bind_thms ("washI", [thm "context1"] RL ([thm "wash"] RLN (2,[thm "cut"]))) *} -ML {* bind_thms ("dryI", [thm "context1"] RL ([thm "dry"] RLN (2,[thm "cut"]))) *} +ML {* bind_thms ("changeI", [@{thm context1}] RL ([@{thm change}] RLN (2,[@{thm cut}]))) *} +ML {* bind_thms ("load1I", [@{thm context1}] RL ([@{thm load1}] RLN (2,[@{thm cut}]))) *} +ML {* bind_thms ("washI", [@{thm context1}] RL ([@{thm wash}] RLN (2,[@{thm cut}]))) *} +ML {* bind_thms ("dryI", [@{thm context1}] RL ([@{thm dry}] RLN (2,[@{thm cut}]))) *} (* a load of dirty clothes and two dollars gives you clean clothes *) lemma "dollar , dollar , dirty |- clean" - apply (tactic {* best_tac (lazy_cs add_safes (thms "changeI" @ thms "load1I" @ thms "washI" @ thms "dryI")) 1 *}) + apply (tactic {* best_tac (lazy_cs add_safes (@{thms changeI} @ @{thms load1I} @ @{thms washI} @ @{thms dryI})) 1 *}) done (* order of premises doesn't matter *) lemma "dollar , dirty , dollar |- clean" - apply (tactic {* best_tac (lazy_cs add_safes (thms "changeI" @ thms "load1I" @ thms "washI" @ thms "dryI")) 1 *}) + apply (tactic {* best_tac (lazy_cs add_safes (@{thms changeI} @ @{thms load1I} @ @{thms washI} @ @{thms dryI})) 1 *}) done (* alternative formulation *) lemma "dollar , dollar |- dirty -o clean" - apply (tactic {* best_tac (lazy_cs add_safes (thms "changeI" @ thms "load1I" @ thms "washI" @ thms "dryI")) 1 *}) + apply (tactic {* best_tac (lazy_cs add_safes (@{thms changeI} @ @{thms load1I} @ @{thms washI} @ @{thms dryI})) 1 *}) done end diff -r e6b96b4cde7e -r 0dec18004e75 src/ZF/Bool.thy --- a/src/ZF/Bool.thy Mon Sep 06 19:11:01 2010 +0200 +++ b/src/ZF/Bool.thy Mon Sep 06 19:13:10 2010 +0200 @@ -172,45 +172,44 @@ ML {* -val bool_def = thm "bool_def"; - -val bool_defs = thms "bool_defs"; -val singleton_0 = thm "singleton_0"; -val bool_1I = thm "bool_1I"; -val bool_0I = thm "bool_0I"; -val one_not_0 = thm "one_not_0"; -val one_neq_0 = thm "one_neq_0"; -val boolE = thm "boolE"; -val cond_1 = thm "cond_1"; -val cond_0 = thm "cond_0"; -val cond_type = thm "cond_type"; -val cond_simple_type = thm "cond_simple_type"; -val def_cond_1 = thm "def_cond_1"; -val def_cond_0 = thm "def_cond_0"; -val not_1 = thm "not_1"; -val not_0 = thm "not_0"; -val and_1 = thm "and_1"; -val and_0 = thm "and_0"; -val or_1 = thm "or_1"; -val or_0 = thm "or_0"; -val xor_1 = thm "xor_1"; -val xor_0 = thm "xor_0"; -val not_type = thm "not_type"; -val and_type = thm "and_type"; -val or_type = thm "or_type"; -val xor_type = thm "xor_type"; -val bool_typechecks = thms "bool_typechecks"; -val not_not = thm "not_not"; -val not_and = thm "not_and"; -val not_or = thm "not_or"; -val and_absorb = thm "and_absorb"; -val and_commute = thm "and_commute"; -val and_assoc = thm "and_assoc"; -val and_or_distrib = thm "and_or_distrib"; -val or_absorb = thm "or_absorb"; -val or_commute = thm "or_commute"; -val or_assoc = thm "or_assoc"; -val or_and_distrib = thm "or_and_distrib"; +val bool_def = @{thm bool_def}; +val bool_defs = @{thms bool_defs}; +val singleton_0 = @{thm singleton_0}; +val bool_1I = @{thm bool_1I}; +val bool_0I = @{thm bool_0I}; +val one_not_0 = @{thm one_not_0}; +val one_neq_0 = @{thm one_neq_0}; +val boolE = @{thm boolE}; +val cond_1 = @{thm cond_1}; +val cond_0 = @{thm cond_0}; +val cond_type = @{thm cond_type}; +val cond_simple_type = @{thm cond_simple_type}; +val def_cond_1 = @{thm def_cond_1}; +val def_cond_0 = @{thm def_cond_0}; +val not_1 = @{thm not_1}; +val not_0 = @{thm not_0}; +val and_1 = @{thm and_1}; +val and_0 = @{thm and_0}; +val or_1 = @{thm or_1}; +val or_0 = @{thm or_0}; +val xor_1 = @{thm xor_1}; +val xor_0 = @{thm xor_0}; +val not_type = @{thm not_type}; +val and_type = @{thm and_type}; +val or_type = @{thm or_type}; +val xor_type = @{thm xor_type}; +val bool_typechecks = @{thms bool_typechecks}; +val not_not = @{thm not_not}; +val not_and = @{thm not_and}; +val not_or = @{thm not_or}; +val and_absorb = @{thm and_absorb}; +val and_commute = @{thm and_commute}; +val and_assoc = @{thm and_assoc}; +val and_or_distrib = @{thm and_or_distrib}; +val or_absorb = @{thm or_absorb}; +val or_commute = @{thm or_commute}; +val or_assoc = @{thm or_assoc}; +val or_and_distrib = @{thm or_and_distrib}; *} end diff -r e6b96b4cde7e -r 0dec18004e75 src/ZF/Cardinal.thy --- a/src/ZF/Cardinal.thy Mon Sep 06 19:11:01 2010 +0200 +++ b/src/ZF/Cardinal.thy Mon Sep 06 19:13:10 2010 +0200 @@ -1044,134 +1044,134 @@ ML {* -val Least_def = thm "Least_def"; -val eqpoll_def = thm "eqpoll_def"; -val lepoll_def = thm "lepoll_def"; -val lesspoll_def = thm "lesspoll_def"; -val cardinal_def = thm "cardinal_def"; -val Finite_def = thm "Finite_def"; -val Card_def = thm "Card_def"; -val eq_imp_not_mem = thm "eq_imp_not_mem"; -val decomp_bnd_mono = thm "decomp_bnd_mono"; -val Banach_last_equation = thm "Banach_last_equation"; -val decomposition = thm "decomposition"; -val schroeder_bernstein = thm "schroeder_bernstein"; -val bij_imp_eqpoll = thm "bij_imp_eqpoll"; -val eqpoll_refl = thm "eqpoll_refl"; -val eqpoll_sym = thm "eqpoll_sym"; -val eqpoll_trans = thm "eqpoll_trans"; -val subset_imp_lepoll = thm "subset_imp_lepoll"; -val lepoll_refl = thm "lepoll_refl"; -val le_imp_lepoll = thm "le_imp_lepoll"; -val eqpoll_imp_lepoll = thm "eqpoll_imp_lepoll"; -val lepoll_trans = thm "lepoll_trans"; -val eqpollI = thm "eqpollI"; -val eqpollE = thm "eqpollE"; -val eqpoll_iff = thm "eqpoll_iff"; -val lepoll_0_is_0 = thm "lepoll_0_is_0"; -val empty_lepollI = thm "empty_lepollI"; -val lepoll_0_iff = thm "lepoll_0_iff"; -val Un_lepoll_Un = thm "Un_lepoll_Un"; -val eqpoll_0_is_0 = thm "eqpoll_0_is_0"; -val eqpoll_0_iff = thm "eqpoll_0_iff"; -val eqpoll_disjoint_Un = thm "eqpoll_disjoint_Un"; -val lesspoll_not_refl = thm "lesspoll_not_refl"; -val lesspoll_irrefl = thm "lesspoll_irrefl"; -val lesspoll_imp_lepoll = thm "lesspoll_imp_lepoll"; -val lepoll_well_ord = thm "lepoll_well_ord"; -val lepoll_iff_leqpoll = thm "lepoll_iff_leqpoll"; -val inj_not_surj_succ = thm "inj_not_surj_succ"; -val lesspoll_trans = thm "lesspoll_trans"; -val lesspoll_trans1 = thm "lesspoll_trans1"; -val lesspoll_trans2 = thm "lesspoll_trans2"; -val Least_equality = thm "Least_equality"; -val LeastI = thm "LeastI"; -val Least_le = thm "Least_le"; -val less_LeastE = thm "less_LeastE"; -val LeastI2 = thm "LeastI2"; -val Least_0 = thm "Least_0"; -val Ord_Least = thm "Ord_Least"; -val Least_cong = thm "Least_cong"; -val cardinal_cong = thm "cardinal_cong"; -val well_ord_cardinal_eqpoll = thm "well_ord_cardinal_eqpoll"; -val Ord_cardinal_eqpoll = thm "Ord_cardinal_eqpoll"; -val well_ord_cardinal_eqE = thm "well_ord_cardinal_eqE"; -val well_ord_cardinal_eqpoll_iff = thm "well_ord_cardinal_eqpoll_iff"; -val Ord_cardinal_le = thm "Ord_cardinal_le"; -val Card_cardinal_eq = thm "Card_cardinal_eq"; -val CardI = thm "CardI"; -val Card_is_Ord = thm "Card_is_Ord"; -val Card_cardinal_le = thm "Card_cardinal_le"; -val Ord_cardinal = thm "Ord_cardinal"; -val Card_iff_initial = thm "Card_iff_initial"; -val lt_Card_imp_lesspoll = thm "lt_Card_imp_lesspoll"; -val Card_0 = thm "Card_0"; -val Card_Un = thm "Card_Un"; -val Card_cardinal = thm "Card_cardinal"; -val cardinal_mono = thm "cardinal_mono"; -val cardinal_lt_imp_lt = thm "cardinal_lt_imp_lt"; -val Card_lt_imp_lt = thm "Card_lt_imp_lt"; -val Card_lt_iff = thm "Card_lt_iff"; -val Card_le_iff = thm "Card_le_iff"; -val well_ord_lepoll_imp_Card_le = thm "well_ord_lepoll_imp_Card_le"; -val lepoll_cardinal_le = thm "lepoll_cardinal_le"; -val lepoll_Ord_imp_eqpoll = thm "lepoll_Ord_imp_eqpoll"; -val lesspoll_imp_eqpoll = thm "lesspoll_imp_eqpoll"; -val cardinal_subset_Ord = thm "cardinal_subset_Ord"; -val cons_lepoll_consD = thm "cons_lepoll_consD"; -val cons_eqpoll_consD = thm "cons_eqpoll_consD"; -val succ_lepoll_succD = thm "succ_lepoll_succD"; -val nat_lepoll_imp_le = thm "nat_lepoll_imp_le"; -val nat_eqpoll_iff = thm "nat_eqpoll_iff"; -val nat_into_Card = thm "nat_into_Card"; -val cardinal_0 = thm "cardinal_0"; -val cardinal_1 = thm "cardinal_1"; -val succ_lepoll_natE = thm "succ_lepoll_natE"; -val n_lesspoll_nat = thm "n_lesspoll_nat"; -val nat_lepoll_imp_ex_eqpoll_n = thm "nat_lepoll_imp_ex_eqpoll_n"; -val lepoll_imp_lesspoll_succ = thm "lepoll_imp_lesspoll_succ"; -val lesspoll_succ_imp_lepoll = thm "lesspoll_succ_imp_lepoll"; -val lesspoll_succ_iff = thm "lesspoll_succ_iff"; -val lepoll_succ_disj = thm "lepoll_succ_disj"; -val lesspoll_cardinal_lt = thm "lesspoll_cardinal_lt"; -val lt_not_lepoll = thm "lt_not_lepoll"; -val Ord_nat_eqpoll_iff = thm "Ord_nat_eqpoll_iff"; -val Card_nat = thm "Card_nat"; -val nat_le_cardinal = thm "nat_le_cardinal"; -val cons_lepoll_cong = thm "cons_lepoll_cong"; -val cons_eqpoll_cong = thm "cons_eqpoll_cong"; -val cons_lepoll_cons_iff = thm "cons_lepoll_cons_iff"; -val cons_eqpoll_cons_iff = thm "cons_eqpoll_cons_iff"; -val singleton_eqpoll_1 = thm "singleton_eqpoll_1"; -val cardinal_singleton = thm "cardinal_singleton"; -val not_0_is_lepoll_1 = thm "not_0_is_lepoll_1"; -val succ_eqpoll_cong = thm "succ_eqpoll_cong"; -val sum_eqpoll_cong = thm "sum_eqpoll_cong"; -val prod_eqpoll_cong = thm "prod_eqpoll_cong"; -val inj_disjoint_eqpoll = thm "inj_disjoint_eqpoll"; -val Diff_sing_lepoll = thm "Diff_sing_lepoll"; -val lepoll_Diff_sing = thm "lepoll_Diff_sing"; -val Diff_sing_eqpoll = thm "Diff_sing_eqpoll"; -val lepoll_1_is_sing = thm "lepoll_1_is_sing"; -val Un_lepoll_sum = thm "Un_lepoll_sum"; -val well_ord_Un = thm "well_ord_Un"; -val disj_Un_eqpoll_sum = thm "disj_Un_eqpoll_sum"; -val Finite_0 = thm "Finite_0"; -val lepoll_nat_imp_Finite = thm "lepoll_nat_imp_Finite"; -val lesspoll_nat_is_Finite = thm "lesspoll_nat_is_Finite"; -val lepoll_Finite = thm "lepoll_Finite"; -val subset_Finite = thm "subset_Finite"; -val Finite_Diff = thm "Finite_Diff"; -val Finite_cons = thm "Finite_cons"; -val Finite_succ = thm "Finite_succ"; -val nat_le_infinite_Ord = thm "nat_le_infinite_Ord"; -val Finite_imp_well_ord = thm "Finite_imp_well_ord"; -val nat_wf_on_converse_Memrel = thm "nat_wf_on_converse_Memrel"; -val nat_well_ord_converse_Memrel = thm "nat_well_ord_converse_Memrel"; -val well_ord_converse = thm "well_ord_converse"; -val ordertype_eq_n = thm "ordertype_eq_n"; -val Finite_well_ord_converse = thm "Finite_well_ord_converse"; -val nat_into_Finite = thm "nat_into_Finite"; +val Least_def = @{thm Least_def}; +val eqpoll_def = @{thm eqpoll_def}; +val lepoll_def = @{thm lepoll_def}; +val lesspoll_def = @{thm lesspoll_def}; +val cardinal_def = @{thm cardinal_def}; +val Finite_def = @{thm Finite_def}; +val Card_def = @{thm Card_def}; +val eq_imp_not_mem = @{thm eq_imp_not_mem}; +val decomp_bnd_mono = @{thm decomp_bnd_mono}; +val Banach_last_equation = @{thm Banach_last_equation}; +val decomposition = @{thm decomposition}; +val schroeder_bernstein = @{thm schroeder_bernstein}; +val bij_imp_eqpoll = @{thm bij_imp_eqpoll}; +val eqpoll_refl = @{thm eqpoll_refl}; +val eqpoll_sym = @{thm eqpoll_sym}; +val eqpoll_trans = @{thm eqpoll_trans}; +val subset_imp_lepoll = @{thm subset_imp_lepoll}; +val lepoll_refl = @{thm lepoll_refl}; +val le_imp_lepoll = @{thm le_imp_lepoll}; +val eqpoll_imp_lepoll = @{thm eqpoll_imp_lepoll}; +val lepoll_trans = @{thm lepoll_trans}; +val eqpollI = @{thm eqpollI}; +val eqpollE = @{thm eqpollE}; +val eqpoll_iff = @{thm eqpoll_iff}; +val lepoll_0_is_0 = @{thm lepoll_0_is_0}; +val empty_lepollI = @{thm empty_lepollI}; +val lepoll_0_iff = @{thm lepoll_0_iff}; +val Un_lepoll_Un = @{thm Un_lepoll_Un}; +val eqpoll_0_is_0 = @{thm eqpoll_0_is_0}; +val eqpoll_0_iff = @{thm eqpoll_0_iff}; +val eqpoll_disjoint_Un = @{thm eqpoll_disjoint_Un}; +val lesspoll_not_refl = @{thm lesspoll_not_refl}; +val lesspoll_irrefl = @{thm lesspoll_irrefl}; +val lesspoll_imp_lepoll = @{thm lesspoll_imp_lepoll}; +val lepoll_well_ord = @{thm lepoll_well_ord}; +val lepoll_iff_leqpoll = @{thm lepoll_iff_leqpoll}; +val inj_not_surj_succ = @{thm inj_not_surj_succ}; +val lesspoll_trans = @{thm lesspoll_trans}; +val lesspoll_trans1 = @{thm lesspoll_trans1}; +val lesspoll_trans2 = @{thm lesspoll_trans2}; +val Least_equality = @{thm Least_equality}; +val LeastI = @{thm LeastI}; +val Least_le = @{thm Least_le}; +val less_LeastE = @{thm less_LeastE}; +val LeastI2 = @{thm LeastI2}; +val Least_0 = @{thm Least_0}; +val Ord_Least = @{thm Ord_Least}; +val Least_cong = @{thm Least_cong}; +val cardinal_cong = @{thm cardinal_cong}; +val well_ord_cardinal_eqpoll = @{thm well_ord_cardinal_eqpoll}; +val Ord_cardinal_eqpoll = @{thm Ord_cardinal_eqpoll}; +val well_ord_cardinal_eqE = @{thm well_ord_cardinal_eqE}; +val well_ord_cardinal_eqpoll_iff = @{thm well_ord_cardinal_eqpoll_iff}; +val Ord_cardinal_le = @{thm Ord_cardinal_le}; +val Card_cardinal_eq = @{thm Card_cardinal_eq}; +val CardI = @{thm CardI}; +val Card_is_Ord = @{thm Card_is_Ord}; +val Card_cardinal_le = @{thm Card_cardinal_le}; +val Ord_cardinal = @{thm Ord_cardinal}; +val Card_iff_initial = @{thm Card_iff_initial}; +val lt_Card_imp_lesspoll = @{thm lt_Card_imp_lesspoll}; +val Card_0 = @{thm Card_0}; +val Card_Un = @{thm Card_Un}; +val Card_cardinal = @{thm Card_cardinal}; +val cardinal_mono = @{thm cardinal_mono}; +val cardinal_lt_imp_lt = @{thm cardinal_lt_imp_lt}; +val Card_lt_imp_lt = @{thm Card_lt_imp_lt}; +val Card_lt_iff = @{thm Card_lt_iff}; +val Card_le_iff = @{thm Card_le_iff}; +val well_ord_lepoll_imp_Card_le = @{thm well_ord_lepoll_imp_Card_le}; +val lepoll_cardinal_le = @{thm lepoll_cardinal_le}; +val lepoll_Ord_imp_eqpoll = @{thm lepoll_Ord_imp_eqpoll}; +val lesspoll_imp_eqpoll = @{thm lesspoll_imp_eqpoll}; +val cardinal_subset_Ord = @{thm cardinal_subset_Ord}; +val cons_lepoll_consD = @{thm cons_lepoll_consD}; +val cons_eqpoll_consD = @{thm cons_eqpoll_consD}; +val succ_lepoll_succD = @{thm succ_lepoll_succD}; +val nat_lepoll_imp_le = @{thm nat_lepoll_imp_le}; +val nat_eqpoll_iff = @{thm nat_eqpoll_iff}; +val nat_into_Card = @{thm nat_into_Card}; +val cardinal_0 = @{thm cardinal_0}; +val cardinal_1 = @{thm cardinal_1}; +val succ_lepoll_natE = @{thm succ_lepoll_natE}; +val n_lesspoll_nat = @{thm n_lesspoll_nat}; +val nat_lepoll_imp_ex_eqpoll_n = @{thm nat_lepoll_imp_ex_eqpoll_n}; +val lepoll_imp_lesspoll_succ = @{thm lepoll_imp_lesspoll_succ}; +val lesspoll_succ_imp_lepoll = @{thm lesspoll_succ_imp_lepoll}; +val lesspoll_succ_iff = @{thm lesspoll_succ_iff}; +val lepoll_succ_disj = @{thm lepoll_succ_disj}; +val lesspoll_cardinal_lt = @{thm lesspoll_cardinal_lt}; +val lt_not_lepoll = @{thm lt_not_lepoll}; +val Ord_nat_eqpoll_iff = @{thm Ord_nat_eqpoll_iff}; +val Card_nat = @{thm Card_nat}; +val nat_le_cardinal = @{thm nat_le_cardinal}; +val cons_lepoll_cong = @{thm cons_lepoll_cong}; +val cons_eqpoll_cong = @{thm cons_eqpoll_cong}; +val cons_lepoll_cons_iff = @{thm cons_lepoll_cons_iff}; +val cons_eqpoll_cons_iff = @{thm cons_eqpoll_cons_iff}; +val singleton_eqpoll_1 = @{thm singleton_eqpoll_1}; +val cardinal_singleton = @{thm cardinal_singleton}; +val not_0_is_lepoll_1 = @{thm not_0_is_lepoll_1}; +val succ_eqpoll_cong = @{thm succ_eqpoll_cong}; +val sum_eqpoll_cong = @{thm sum_eqpoll_cong}; +val prod_eqpoll_cong = @{thm prod_eqpoll_cong}; +val inj_disjoint_eqpoll = @{thm inj_disjoint_eqpoll}; +val Diff_sing_lepoll = @{thm Diff_sing_lepoll}; +val lepoll_Diff_sing = @{thm lepoll_Diff_sing}; +val Diff_sing_eqpoll = @{thm Diff_sing_eqpoll}; +val lepoll_1_is_sing = @{thm lepoll_1_is_sing}; +val Un_lepoll_sum = @{thm Un_lepoll_sum}; +val well_ord_Un = @{thm well_ord_Un}; +val disj_Un_eqpoll_sum = @{thm disj_Un_eqpoll_sum}; +val Finite_0 = @{thm Finite_0}; +val lepoll_nat_imp_Finite = @{thm lepoll_nat_imp_Finite}; +val lesspoll_nat_is_Finite = @{thm lesspoll_nat_is_Finite}; +val lepoll_Finite = @{thm lepoll_Finite}; +val subset_Finite = @{thm subset_Finite}; +val Finite_Diff = @{thm Finite_Diff}; +val Finite_cons = @{thm Finite_cons}; +val Finite_succ = @{thm Finite_succ}; +val nat_le_infinite_Ord = @{thm nat_le_infinite_Ord}; +val Finite_imp_well_ord = @{thm Finite_imp_well_ord}; +val nat_wf_on_converse_Memrel = @{thm nat_wf_on_converse_Memrel}; +val nat_well_ord_converse_Memrel = @{thm nat_well_ord_converse_Memrel}; +val well_ord_converse = @{thm well_ord_converse}; +val ordertype_eq_n = @{thm ordertype_eq_n}; +val Finite_well_ord_converse = @{thm Finite_well_ord_converse}; +val nat_into_Finite = @{thm nat_into_Finite}; *} end diff -r e6b96b4cde7e -r 0dec18004e75 src/ZF/CardinalArith.thy --- a/src/ZF/CardinalArith.thy Mon Sep 06 19:11:01 2010 +0200 +++ b/src/ZF/CardinalArith.thy Mon Sep 06 19:13:10 2010 +0200 @@ -911,89 +911,89 @@ ML{* -val InfCard_def = thm "InfCard_def" -val cmult_def = thm "cmult_def" -val cadd_def = thm "cadd_def" -val jump_cardinal_def = thm "jump_cardinal_def" -val csucc_def = thm "csucc_def" +val InfCard_def = @{thm InfCard_def}; +val cmult_def = @{thm cmult_def}; +val cadd_def = @{thm cadd_def}; +val jump_cardinal_def = @{thm jump_cardinal_def}; +val csucc_def = @{thm csucc_def}; -val sum_commute_eqpoll = thm "sum_commute_eqpoll"; -val cadd_commute = thm "cadd_commute"; -val sum_assoc_eqpoll = thm "sum_assoc_eqpoll"; -val well_ord_cadd_assoc = thm "well_ord_cadd_assoc"; -val sum_0_eqpoll = thm "sum_0_eqpoll"; -val cadd_0 = thm "cadd_0"; -val sum_lepoll_self = thm "sum_lepoll_self"; -val cadd_le_self = thm "cadd_le_self"; -val sum_lepoll_mono = thm "sum_lepoll_mono"; -val cadd_le_mono = thm "cadd_le_mono"; -val eq_imp_not_mem = thm "eq_imp_not_mem"; -val sum_succ_eqpoll = thm "sum_succ_eqpoll"; -val nat_cadd_eq_add = thm "nat_cadd_eq_add"; -val prod_commute_eqpoll = thm "prod_commute_eqpoll"; -val cmult_commute = thm "cmult_commute"; -val prod_assoc_eqpoll = thm "prod_assoc_eqpoll"; -val well_ord_cmult_assoc = thm "well_ord_cmult_assoc"; -val sum_prod_distrib_eqpoll = thm "sum_prod_distrib_eqpoll"; -val well_ord_cadd_cmult_distrib = thm "well_ord_cadd_cmult_distrib"; -val prod_0_eqpoll = thm "prod_0_eqpoll"; -val cmult_0 = thm "cmult_0"; -val prod_singleton_eqpoll = thm "prod_singleton_eqpoll"; -val cmult_1 = thm "cmult_1"; -val prod_lepoll_self = thm "prod_lepoll_self"; -val cmult_le_self = thm "cmult_le_self"; -val prod_lepoll_mono = thm "prod_lepoll_mono"; -val cmult_le_mono = thm "cmult_le_mono"; -val prod_succ_eqpoll = thm "prod_succ_eqpoll"; -val nat_cmult_eq_mult = thm "nat_cmult_eq_mult"; -val cmult_2 = thm "cmult_2"; -val sum_lepoll_prod = thm "sum_lepoll_prod"; -val lepoll_imp_sum_lepoll_prod = thm "lepoll_imp_sum_lepoll_prod"; -val nat_cons_lepoll = thm "nat_cons_lepoll"; -val nat_cons_eqpoll = thm "nat_cons_eqpoll"; -val nat_succ_eqpoll = thm "nat_succ_eqpoll"; -val InfCard_nat = thm "InfCard_nat"; -val InfCard_is_Card = thm "InfCard_is_Card"; -val InfCard_Un = thm "InfCard_Un"; -val InfCard_is_Limit = thm "InfCard_is_Limit"; -val ordermap_eqpoll_pred = thm "ordermap_eqpoll_pred"; -val ordermap_z_lt = thm "ordermap_z_lt"; -val InfCard_le_cmult_eq = thm "InfCard_le_cmult_eq"; -val InfCard_cmult_eq = thm "InfCard_cmult_eq"; -val InfCard_cdouble_eq = thm "InfCard_cdouble_eq"; -val InfCard_le_cadd_eq = thm "InfCard_le_cadd_eq"; -val InfCard_cadd_eq = thm "InfCard_cadd_eq"; -val Ord_jump_cardinal = thm "Ord_jump_cardinal"; -val jump_cardinal_iff = thm "jump_cardinal_iff"; -val K_lt_jump_cardinal = thm "K_lt_jump_cardinal"; -val Card_jump_cardinal = thm "Card_jump_cardinal"; -val csucc_basic = thm "csucc_basic"; -val Card_csucc = thm "Card_csucc"; -val lt_csucc = thm "lt_csucc"; -val Ord_0_lt_csucc = thm "Ord_0_lt_csucc"; -val csucc_le = thm "csucc_le"; -val lt_csucc_iff = thm "lt_csucc_iff"; -val Card_lt_csucc_iff = thm "Card_lt_csucc_iff"; -val InfCard_csucc = thm "InfCard_csucc"; -val Finite_into_Fin = thm "Finite_into_Fin"; -val Fin_into_Finite = thm "Fin_into_Finite"; -val Finite_Fin_iff = thm "Finite_Fin_iff"; -val Finite_Un = thm "Finite_Un"; -val Finite_Union = thm "Finite_Union"; -val Finite_induct = thm "Finite_induct"; -val Fin_imp_not_cons_lepoll = thm "Fin_imp_not_cons_lepoll"; -val Finite_imp_cardinal_cons = thm "Finite_imp_cardinal_cons"; -val Finite_imp_succ_cardinal_Diff = thm "Finite_imp_succ_cardinal_Diff"; -val Finite_imp_cardinal_Diff = thm "Finite_imp_cardinal_Diff"; -val nat_implies_well_ord = thm "nat_implies_well_ord"; -val nat_sum_eqpoll_sum = thm "nat_sum_eqpoll_sum"; -val Diff_sing_Finite = thm "Diff_sing_Finite"; -val Diff_Finite = thm "Diff_Finite"; -val Ord_subset_natD = thm "Ord_subset_natD"; -val Ord_nat_subset_into_Card = thm "Ord_nat_subset_into_Card"; -val Finite_cardinal_in_nat = thm "Finite_cardinal_in_nat"; -val Finite_Diff_sing_eq_diff_1 = thm "Finite_Diff_sing_eq_diff_1"; -val cardinal_lt_imp_Diff_not_0 = thm "cardinal_lt_imp_Diff_not_0"; +val sum_commute_eqpoll = @{thm sum_commute_eqpoll}; +val cadd_commute = @{thm cadd_commute}; +val sum_assoc_eqpoll = @{thm sum_assoc_eqpoll}; +val well_ord_cadd_assoc = @{thm well_ord_cadd_assoc}; +val sum_0_eqpoll = @{thm sum_0_eqpoll}; +val cadd_0 = @{thm cadd_0}; +val sum_lepoll_self = @{thm sum_lepoll_self}; +val cadd_le_self = @{thm cadd_le_self}; +val sum_lepoll_mono = @{thm sum_lepoll_mono}; +val cadd_le_mono = @{thm cadd_le_mono}; +val eq_imp_not_mem = @{thm eq_imp_not_mem}; +val sum_succ_eqpoll = @{thm sum_succ_eqpoll}; +val nat_cadd_eq_add = @{thm nat_cadd_eq_add}; +val prod_commute_eqpoll = @{thm prod_commute_eqpoll}; +val cmult_commute = @{thm cmult_commute}; +val prod_assoc_eqpoll = @{thm prod_assoc_eqpoll}; +val well_ord_cmult_assoc = @{thm well_ord_cmult_assoc}; +val sum_prod_distrib_eqpoll = @{thm sum_prod_distrib_eqpoll}; +val well_ord_cadd_cmult_distrib = @{thm well_ord_cadd_cmult_distrib}; +val prod_0_eqpoll = @{thm prod_0_eqpoll}; +val cmult_0 = @{thm cmult_0}; +val prod_singleton_eqpoll = @{thm prod_singleton_eqpoll}; +val cmult_1 = @{thm cmult_1}; +val prod_lepoll_self = @{thm prod_lepoll_self}; +val cmult_le_self = @{thm cmult_le_self}; +val prod_lepoll_mono = @{thm prod_lepoll_mono}; +val cmult_le_mono = @{thm cmult_le_mono}; +val prod_succ_eqpoll = @{thm prod_succ_eqpoll}; +val nat_cmult_eq_mult = @{thm nat_cmult_eq_mult}; +val cmult_2 = @{thm cmult_2}; +val sum_lepoll_prod = @{thm sum_lepoll_prod}; +val lepoll_imp_sum_lepoll_prod = @{thm lepoll_imp_sum_lepoll_prod}; +val nat_cons_lepoll = @{thm nat_cons_lepoll}; +val nat_cons_eqpoll = @{thm nat_cons_eqpoll}; +val nat_succ_eqpoll = @{thm nat_succ_eqpoll}; +val InfCard_nat = @{thm InfCard_nat}; +val InfCard_is_Card = @{thm InfCard_is_Card}; +val InfCard_Un = @{thm InfCard_Un}; +val InfCard_is_Limit = @{thm InfCard_is_Limit}; +val ordermap_eqpoll_pred = @{thm ordermap_eqpoll_pred}; +val ordermap_z_lt = @{thm ordermap_z_lt}; +val InfCard_le_cmult_eq = @{thm InfCard_le_cmult_eq}; +val InfCard_cmult_eq = @{thm InfCard_cmult_eq}; +val InfCard_cdouble_eq = @{thm InfCard_cdouble_eq}; +val InfCard_le_cadd_eq = @{thm InfCard_le_cadd_eq}; +val InfCard_cadd_eq = @{thm InfCard_cadd_eq}; +val Ord_jump_cardinal = @{thm Ord_jump_cardinal}; +val jump_cardinal_iff = @{thm jump_cardinal_iff}; +val K_lt_jump_cardinal = @{thm K_lt_jump_cardinal}; +val Card_jump_cardinal = @{thm Card_jump_cardinal}; +val csucc_basic = @{thm csucc_basic}; +val Card_csucc = @{thm Card_csucc}; +val lt_csucc = @{thm lt_csucc}; +val Ord_0_lt_csucc = @{thm Ord_0_lt_csucc}; +val csucc_le = @{thm csucc_le}; +val lt_csucc_iff = @{thm lt_csucc_iff}; +val Card_lt_csucc_iff = @{thm Card_lt_csucc_iff}; +val InfCard_csucc = @{thm InfCard_csucc}; +val Finite_into_Fin = @{thm Finite_into_Fin}; +val Fin_into_Finite = @{thm Fin_into_Finite}; +val Finite_Fin_iff = @{thm Finite_Fin_iff}; +val Finite_Un = @{thm Finite_Un}; +val Finite_Union = @{thm Finite_Union}; +val Finite_induct = @{thm Finite_induct}; +val Fin_imp_not_cons_lepoll = @{thm Fin_imp_not_cons_lepoll}; +val Finite_imp_cardinal_cons = @{thm Finite_imp_cardinal_cons}; +val Finite_imp_succ_cardinal_Diff = @{thm Finite_imp_succ_cardinal_Diff}; +val Finite_imp_cardinal_Diff = @{thm Finite_imp_cardinal_Diff}; +val nat_implies_well_ord = @{thm nat_implies_well_ord}; +val nat_sum_eqpoll_sum = @{thm nat_sum_eqpoll_sum}; +val Diff_sing_Finite = @{thm Diff_sing_Finite}; +val Diff_Finite = @{thm Diff_Finite}; +val Ord_subset_natD = @{thm Ord_subset_natD}; +val Ord_nat_subset_into_Card = @{thm Ord_nat_subset_into_Card}; +val Finite_cardinal_in_nat = @{thm Finite_cardinal_in_nat}; +val Finite_Diff_sing_eq_diff_1 = @{thm Finite_Diff_sing_eq_diff_1}; +val cardinal_lt_imp_Diff_not_0 = @{thm cardinal_lt_imp_Diff_not_0}; *} end diff -r e6b96b4cde7e -r 0dec18004e75 src/ZF/Cardinal_AC.thy --- a/src/ZF/Cardinal_AC.thy Mon Sep 06 19:11:01 2010 +0200 +++ b/src/ZF/Cardinal_AC.thy Mon Sep 06 19:13:10 2010 +0200 @@ -193,8 +193,8 @@ ML {* -val cardinal_0_iff_0 = thm "cardinal_0_iff_0"; -val cardinal_lt_iff_lesspoll = thm "cardinal_lt_iff_lesspoll"; +val cardinal_0_iff_0 = @{thm cardinal_0_iff_0}; +val cardinal_lt_iff_lesspoll = @{thm cardinal_lt_iff_lesspoll}; *} end diff -r e6b96b4cde7e -r 0dec18004e75 src/ZF/Epsilon.thy --- a/src/ZF/Epsilon.thy Mon Sep 06 19:11:01 2010 +0200 +++ b/src/ZF/Epsilon.thy Mon Sep 06 19:13:10 2010 +0200 @@ -398,56 +398,56 @@ ML {* -val arg_subset_eclose = thm "arg_subset_eclose"; -val arg_into_eclose = thm "arg_into_eclose"; -val Transset_eclose = thm "Transset_eclose"; -val eclose_subset = thm "eclose_subset"; -val ecloseD = thm "ecloseD"; -val arg_in_eclose_sing = thm "arg_in_eclose_sing"; -val arg_into_eclose_sing = thm "arg_into_eclose_sing"; -val eclose_induct = thm "eclose_induct"; -val eps_induct = thm "eps_induct"; -val eclose_least = thm "eclose_least"; -val eclose_induct_down = thm "eclose_induct_down"; -val Transset_eclose_eq_arg = thm "Transset_eclose_eq_arg"; -val mem_eclose_trans = thm "mem_eclose_trans"; -val mem_eclose_sing_trans = thm "mem_eclose_sing_trans"; -val under_Memrel = thm "under_Memrel"; -val under_Memrel_eclose = thm "under_Memrel_eclose"; -val wfrec_ssubst = thm "wfrec_ssubst"; -val wfrec_eclose_eq = thm "wfrec_eclose_eq"; -val wfrec_eclose_eq2 = thm "wfrec_eclose_eq2"; -val transrec = thm "transrec"; -val def_transrec = thm "def_transrec"; -val transrec_type = thm "transrec_type"; -val eclose_sing_Ord = thm "eclose_sing_Ord"; -val Ord_transrec_type = thm "Ord_transrec_type"; -val rank = thm "rank"; -val Ord_rank = thm "Ord_rank"; -val rank_of_Ord = thm "rank_of_Ord"; -val rank_lt = thm "rank_lt"; -val eclose_rank_lt = thm "eclose_rank_lt"; -val rank_mono = thm "rank_mono"; -val rank_Pow = thm "rank_Pow"; -val rank_0 = thm "rank_0"; -val rank_succ = thm "rank_succ"; -val rank_Union = thm "rank_Union"; -val rank_eclose = thm "rank_eclose"; -val rank_pair1 = thm "rank_pair1"; -val rank_pair2 = thm "rank_pair2"; -val the_equality_if = thm "the_equality_if"; -val rank_apply = thm "rank_apply"; -val mem_eclose_subset = thm "mem_eclose_subset"; -val eclose_mono = thm "eclose_mono"; -val eclose_idem = thm "eclose_idem"; -val transrec2_0 = thm "transrec2_0"; -val transrec2_succ = thm "transrec2_succ"; -val transrec2_Limit = thm "transrec2_Limit"; -val recursor_0 = thm "recursor_0"; -val recursor_succ = thm "recursor_succ"; -val rec_0 = thm "rec_0"; -val rec_succ = thm "rec_succ"; -val rec_type = thm "rec_type"; +val arg_subset_eclose = @{thm arg_subset_eclose}; +val arg_into_eclose = @{thm arg_into_eclose}; +val Transset_eclose = @{thm Transset_eclose}; +val eclose_subset = @{thm eclose_subset}; +val ecloseD = @{thm ecloseD}; +val arg_in_eclose_sing = @{thm arg_in_eclose_sing}; +val arg_into_eclose_sing = @{thm arg_into_eclose_sing}; +val eclose_induct = @{thm eclose_induct}; +val eps_induct = @{thm eps_induct}; +val eclose_least = @{thm eclose_least}; +val eclose_induct_down = @{thm eclose_induct_down}; +val Transset_eclose_eq_arg = @{thm Transset_eclose_eq_arg}; +val mem_eclose_trans = @{thm mem_eclose_trans}; +val mem_eclose_sing_trans = @{thm mem_eclose_sing_trans}; +val under_Memrel = @{thm under_Memrel}; +val under_Memrel_eclose = @{thm under_Memrel_eclose}; +val wfrec_ssubst = @{thm wfrec_ssubst}; +val wfrec_eclose_eq = @{thm wfrec_eclose_eq}; +val wfrec_eclose_eq2 = @{thm wfrec_eclose_eq2}; +val transrec = @{thm transrec}; +val def_transrec = @{thm def_transrec}; +val transrec_type = @{thm transrec_type}; +val eclose_sing_Ord = @{thm eclose_sing_Ord}; +val Ord_transrec_type = @{thm Ord_transrec_type}; +val rank = @{thm rank}; +val Ord_rank = @{thm Ord_rank}; +val rank_of_Ord = @{thm rank_of_Ord}; +val rank_lt = @{thm rank_lt}; +val eclose_rank_lt = @{thm eclose_rank_lt}; +val rank_mono = @{thm rank_mono}; +val rank_Pow = @{thm rank_Pow}; +val rank_0 = @{thm rank_0}; +val rank_succ = @{thm rank_succ}; +val rank_Union = @{thm rank_Union}; +val rank_eclose = @{thm rank_eclose}; +val rank_pair1 = @{thm rank_pair1}; +val rank_pair2 = @{thm rank_pair2}; +val the_equality_if = @{thm the_equality_if}; +val rank_apply = @{thm rank_apply}; +val mem_eclose_subset = @{thm mem_eclose_subset}; +val eclose_mono = @{thm eclose_mono}; +val eclose_idem = @{thm eclose_idem}; +val transrec2_0 = @{thm transrec2_0}; +val transrec2_succ = @{thm transrec2_succ}; +val transrec2_Limit = @{thm transrec2_Limit}; +val recursor_0 = @{thm recursor_0}; +val recursor_succ = @{thm recursor_succ}; +val rec_0 = @{thm rec_0}; +val rec_succ = @{thm rec_succ}; +val rec_type = @{thm rec_type}; *} end