more antiquotations;
authorwenzelm
Mon Sep 06 19:13:10 2010 +0200 (2010-09-06)
changeset 391590dec18004e75
parent 39158 e6b96b4cde7e
child 39160 75e096565cd3
more antiquotations;
src/CCL/CCL.thy
src/CCL/Type.thy
src/CCL/ex/Stream.thy
src/CTT/Arith.thy
src/CTT/ex/Elimination.thy
src/CTT/ex/Typechecking.thy
src/CTT/rew.ML
src/FOL/IFOL.thy
src/FOL/hypsubstdata.ML
src/HOL/Algebra/abstract/Ring2.thy
src/HOL/Algebra/poly/LongDiv.thy
src/HOL/Bali/AxCompl.thy
src/HOL/Bali/AxSem.thy
src/HOL/Bali/Eval.thy
src/HOL/Bali/Evaln.thy
src/HOL/Decision_Procs/mir_tac.ML
src/HOL/HOL.thy
src/HOL/Hoare_Parallel/Mul_Gar_Coll.thy
src/HOL/Hoare_Parallel/OG_Tactics.thy
src/HOL/IMPP/Hoare.thy
src/HOL/IMPP/Natural.thy
src/HOL/IOA/Solve.thy
src/HOL/Import/hol4rews.ML
src/HOL/Import/proof_kernel.ML
src/HOL/Import/shuffler.ML
src/HOL/MicroJava/J/JTypeSafe.thy
src/HOL/NSA/NSA.thy
src/HOL/Nominal/nominal_datatype.ML
src/HOL/Nominal/nominal_inductive.ML
src/HOL/Nominal/nominal_inductive2.ML
src/HOL/Old_Number_Theory/Chinese.thy
src/HOL/Old_Number_Theory/IntPrimes.thy
src/HOL/Old_Number_Theory/WilsonBij.thy
src/HOL/Old_Number_Theory/WilsonRuss.thy
src/HOL/Option.thy
src/HOL/Proofs/Lambda/Commutation.thy
src/HOL/Statespace/distinct_tree_prover.ML
src/HOL/Statespace/state_fun.ML
src/HOL/TLA/Memory/Memory.thy
src/HOL/TLA/Memory/MemoryImplementation.thy
src/HOL/TLA/Memory/RPC.thy
src/HOL/Tools/Qelim/cooper.ML
src/HOL/Tools/TFL/casesplit.ML
src/HOL/Tools/TFL/thms.ML
src/HOL/Tools/meson.ML
src/HOL/UNITY/Comp/Alloc.thy
src/HOLCF/FOCUS/Fstream.thy
src/HOLCF/IOA/ABP/Correctness.thy
src/HOLCF/IOA/meta_theory/CompoScheds.thy
src/HOLCF/IOA/meta_theory/SimCorrectness.thy
src/HOLCF/ex/Focus_ex.thy
src/HOLCF/ex/Loop.thy
src/Provers/quasi.ML
src/Sequents/ILL.thy
src/Sequents/LK0.thy
src/Sequents/S4.thy
src/Sequents/S43.thy
src/Sequents/T.thy
src/Sequents/Washing.thy
src/ZF/Bool.thy
src/ZF/Cardinal.thy
src/ZF/CardinalArith.thy
src/ZF/Cardinal_AC.thy
src/ZF/Epsilon.thy
     1.1 --- a/src/CCL/CCL.thy	Mon Sep 06 19:11:01 2010 +0200
     1.2 +++ b/src/CCL/CCL.thy	Mon Sep 06 19:13:10 2010 +0200
     1.3 @@ -238,9 +238,9 @@
     1.4  
     1.5    fun mk_thm_str thy a b = "~ " ^ (saturate thy a "a") ^ " = " ^ (saturate thy b "b")
     1.6  
     1.7 -  val lemma = thm "lem";
     1.8 -  val eq_lemma = thm "eq_lemma";
     1.9 -  val distinctness = thm "distinctness";
    1.10 +  val lemma = @{thm lem};
    1.11 +  val eq_lemma = @{thm eq_lemma};
    1.12 +  val distinctness = @{thm distinctness};
    1.13    fun mk_lemma (ra,rb) = [lemma] RL [ra RS (rb RS eq_lemma)] RL
    1.14                             [distinctness RS notE, @{thm sym} RS (distinctness RS notE)]
    1.15  in
     2.1 --- a/src/CCL/Type.thy	Mon Sep 06 19:11:01 2010 +0200
     2.2 +++ b/src/CCL/Type.thy	Mon Sep 06 19:13:10 2010 +0200
     2.3 @@ -99,7 +99,7 @@
     2.4    unfolding simp_type_defs by blast+
     2.5  
     2.6  ML {*
     2.7 -bind_thms ("case_rls", XH_to_Es (thms "XHs"));
     2.8 +bind_thms ("case_rls", XH_to_Es @{thms XHs});
     2.9  *}
    2.10  
    2.11  
    2.12 @@ -260,7 +260,7 @@
    2.13  
    2.14  lemmas iXHs = NatXH ListXH
    2.15  
    2.16 -ML {* bind_thms ("icase_rls", XH_to_Es (thms "iXHs")) *}
    2.17 +ML {* bind_thms ("icase_rls", XH_to_Es @{thms iXHs}) *}
    2.18  
    2.19  
    2.20  subsection {* Type Rules *}
     3.1 --- a/src/CCL/ex/Stream.thy	Mon Sep 06 19:11:01 2010 +0200
     3.2 +++ b/src/CCL/ex/Stream.thy	Mon Sep 06 19:13:10 2010 +0200
     3.3 @@ -88,7 +88,7 @@
     3.4    apply (tactic "EQgen_tac @{context} [] 1")
     3.5     prefer 2
     3.6     apply blast
     3.7 -  apply (tactic {* DEPTH_SOLVE (etac (XH_to_E (thm "ListsXH")) 1
     3.8 +  apply (tactic {* DEPTH_SOLVE (etac (XH_to_E @{thm ListsXH}) 1
     3.9      THEN EQgen_tac @{context} [] 1) *})
    3.10    done
    3.11  
    3.12 @@ -135,7 +135,7 @@
    3.13    apply (tactic {* eq_coinduct3_tac @{context}
    3.14      "{p. EX x y. p=<x,y> & (EX n:Nat. x=iter1 (f,f^n`a) & y=map (f) ^n`iter2 (f,a))}" 1*})
    3.15    apply (fast intro!: napplyBzero [symmetric] napplyBzero [symmetric, THEN arg_cong])
    3.16 -  apply (tactic {* EQgen_tac @{context} [thm "iter1B", thm "iter2Blemma"] 1 *})
    3.17 +  apply (tactic {* EQgen_tac @{context} [@{thm iter1B}, @{thm iter2Blemma}] 1 *})
    3.18    apply (subst napply_f, assumption)
    3.19    apply (rule_tac f1 = f in napplyBsucc [THEN subst])
    3.20    apply blast
     4.1 --- a/src/CTT/Arith.thy	Mon Sep 06 19:11:01 2010 +0200
     4.2 +++ b/src/CTT/Arith.thy	Mon Sep 06 19:13:10 2010 +0200
     4.3 @@ -82,12 +82,12 @@
     4.4  
     4.5  lemma mult_typing: "[| a:N;  b:N |] ==> a #* b : N"
     4.6  apply (unfold arith_defs)
     4.7 -apply (tactic {* typechk_tac [thm "add_typing"] *})
     4.8 +apply (tactic {* typechk_tac [@{thm add_typing}] *})
     4.9  done
    4.10  
    4.11  lemma mult_typingL: "[| a=c:N;  b=d:N |] ==> a #* b = c #* d : N"
    4.12  apply (unfold arith_defs)
    4.13 -apply (tactic {* equal_tac [thm "add_typingL"] *})
    4.14 +apply (tactic {* equal_tac [@{thm add_typingL}] *})
    4.15  done
    4.16  
    4.17  (*computation for mult: 0 and successor cases*)
    4.18 @@ -159,19 +159,19 @@
    4.19  
    4.20  structure Arith_simp_data: TSIMP_DATA =
    4.21    struct
    4.22 -  val refl              = thm "refl_elem"
    4.23 -  val sym               = thm "sym_elem"
    4.24 -  val trans             = thm "trans_elem"
    4.25 -  val refl_red          = thm "refl_red"
    4.26 -  val trans_red         = thm "trans_red"
    4.27 -  val red_if_equal      = thm "red_if_equal"
    4.28 -  val default_rls       = thms "arithC_rls" @ thms "comp_rls"
    4.29 -  val routine_tac       = routine_tac (thms "arith_typing_rls" @ thms "routine_rls")
    4.30 +  val refl              = @{thm refl_elem}
    4.31 +  val sym               = @{thm sym_elem}
    4.32 +  val trans             = @{thm trans_elem}
    4.33 +  val refl_red          = @{thm refl_red}
    4.34 +  val trans_red         = @{thm trans_red}
    4.35 +  val red_if_equal      = @{thm red_if_equal}
    4.36 +  val default_rls       = @{thms arithC_rls} @ @{thms comp_rls}
    4.37 +  val routine_tac       = routine_tac (@{thms arith_typing_rls} @ @{thms routine_rls})
    4.38    end
    4.39  
    4.40  structure Arith_simp = TSimpFun (Arith_simp_data)
    4.41  
    4.42 -local val congr_rls = thms "congr_rls" in
    4.43 +local val congr_rls = @{thms congr_rls} in
    4.44  
    4.45  fun arith_rew_tac prems = make_rew_tac
    4.46      (Arith_simp.norm_tac(congr_rls, prems))
    4.47 @@ -271,7 +271,7 @@
    4.48  (*Solves first 0 goal, simplifies others.  Two sugbgoals remain.
    4.49    Both follow by rewriting, (2) using quantified induction hyp*)
    4.50  apply (tactic "intr_tac []") (*strips remaining PRODs*)
    4.51 -apply (tactic {* hyp_arith_rew_tac [thm "add_0_right"] *})
    4.52 +apply (tactic {* hyp_arith_rew_tac [@{thm add_0_right}] *})
    4.53  apply assumption
    4.54  done
    4.55  
    4.56 @@ -303,7 +303,7 @@
    4.57  
    4.58  lemma absdiff_self_eq_0: "a:N ==> a |-| a = 0 : N"
    4.59  apply (unfold absdiff_def)
    4.60 -apply (tactic {* arith_rew_tac [thm "diff_self_eq_0"] *})
    4.61 +apply (tactic {* arith_rew_tac [@{thm diff_self_eq_0}] *})
    4.62  done
    4.63  
    4.64  lemma absdiffC0: "a:N ==> 0 |-| a = a : N"
    4.65 @@ -321,7 +321,7 @@
    4.66  lemma absdiff_commute: "[| a:N;  b:N |] ==> a |-| b = b |-| a : N"
    4.67  apply (unfold absdiff_def)
    4.68  apply (rule add_commute)
    4.69 -apply (tactic {* typechk_tac [thm "diff_typing"] *})
    4.70 +apply (tactic {* typechk_tac [@{thm diff_typing}] *})
    4.71  done
    4.72  
    4.73  (*If a+b=0 then a=0.   Surprisingly tedious*)
    4.74 @@ -332,7 +332,7 @@
    4.75  apply (tactic "intr_tac []") (*strips remaining PRODs*)
    4.76  apply (rule_tac [2] zero_ne_succ [THEN FE])
    4.77  apply (erule_tac [3] EqE [THEN sym_elem])
    4.78 -apply (tactic {* typechk_tac [thm "add_typing"] *})
    4.79 +apply (tactic {* typechk_tac [@{thm add_typing}] *})
    4.80  done
    4.81  
    4.82  (*Version of above with the premise  a+b=0.
    4.83 @@ -354,7 +354,7 @@
    4.84  apply (rule_tac [2] add_eq0)
    4.85  apply (rule add_eq0)
    4.86  apply (rule_tac [6] add_commute [THEN trans_elem])
    4.87 -apply (tactic {* typechk_tac [thm "diff_typing"] *})
    4.88 +apply (tactic {* typechk_tac [@{thm diff_typing}] *})
    4.89  done
    4.90  
    4.91  (*if  a |-| b = 0  then  a = b
    4.92 @@ -366,7 +366,7 @@
    4.93  apply (tactic eqintr_tac)
    4.94  apply (rule add_diff_inverse [THEN sym_elem, THEN trans_elem])
    4.95  apply (rule_tac [3] EqE, tactic "assume_tac 3")
    4.96 -apply (tactic {* hyp_arith_rew_tac [thm "add_0_right"] *})
    4.97 +apply (tactic {* hyp_arith_rew_tac [@{thm add_0_right}] *})
    4.98  done
    4.99  
   4.100  
   4.101 @@ -376,12 +376,12 @@
   4.102  
   4.103  lemma mod_typing: "[| a:N;  b:N |] ==> a mod b : N"
   4.104  apply (unfold mod_def)
   4.105 -apply (tactic {* typechk_tac [thm "absdiff_typing"] *})
   4.106 +apply (tactic {* typechk_tac [@{thm absdiff_typing}] *})
   4.107  done
   4.108  
   4.109  lemma mod_typingL: "[| a=c:N;  b=d:N |] ==> a mod b = c mod d : N"
   4.110  apply (unfold mod_def)
   4.111 -apply (tactic {* equal_tac [thm "absdiff_typingL"] *})
   4.112 +apply (tactic {* equal_tac [@{thm absdiff_typingL}] *})
   4.113  done
   4.114  
   4.115  
   4.116 @@ -389,13 +389,13 @@
   4.117  
   4.118  lemma modC0: "b:N ==> 0 mod b = 0 : N"
   4.119  apply (unfold mod_def)
   4.120 -apply (tactic {* rew_tac [thm "absdiff_typing"] *})
   4.121 +apply (tactic {* rew_tac [@{thm absdiff_typing}] *})
   4.122  done
   4.123  
   4.124  lemma modC_succ:
   4.125  "[| a:N; b:N |] ==> succ(a) mod b = rec(succ(a mod b) |-| b, 0, %x y. succ(a mod b)) : N"
   4.126  apply (unfold mod_def)
   4.127 -apply (tactic {* rew_tac [thm "absdiff_typing"] *})
   4.128 +apply (tactic {* rew_tac [@{thm absdiff_typing}] *})
   4.129  done
   4.130  
   4.131  
   4.132 @@ -403,12 +403,12 @@
   4.133  
   4.134  lemma div_typing: "[| a:N;  b:N |] ==> a div b : N"
   4.135  apply (unfold div_def)
   4.136 -apply (tactic {* typechk_tac [thm "absdiff_typing", thm "mod_typing"] *})
   4.137 +apply (tactic {* typechk_tac [@{thm absdiff_typing}, @{thm mod_typing}] *})
   4.138  done
   4.139  
   4.140  lemma div_typingL: "[| a=c:N;  b=d:N |] ==> a div b = c div d : N"
   4.141  apply (unfold div_def)
   4.142 -apply (tactic {* equal_tac [thm "absdiff_typingL", thm "mod_typingL"] *})
   4.143 +apply (tactic {* equal_tac [@{thm absdiff_typingL}, @{thm mod_typingL}] *})
   4.144  done
   4.145  
   4.146  lemmas div_typing_rls = mod_typing div_typing absdiff_typing
   4.147 @@ -418,14 +418,14 @@
   4.148  
   4.149  lemma divC0: "b:N ==> 0 div b = 0 : N"
   4.150  apply (unfold div_def)
   4.151 -apply (tactic {* rew_tac [thm "mod_typing", thm "absdiff_typing"] *})
   4.152 +apply (tactic {* rew_tac [@{thm mod_typing}, @{thm absdiff_typing}] *})
   4.153  done
   4.154  
   4.155  lemma divC_succ:
   4.156   "[| a:N;  b:N |] ==> succ(a) div b =
   4.157       rec(succ(a) mod b, succ(a div b), %x y. a div b) : N"
   4.158  apply (unfold div_def)
   4.159 -apply (tactic {* rew_tac [thm "mod_typing"] *})
   4.160 +apply (tactic {* rew_tac [@{thm mod_typing}] *})
   4.161  done
   4.162  
   4.163  
   4.164 @@ -433,9 +433,9 @@
   4.165  lemma divC_succ2: "[| a:N;  b:N |] ==>
   4.166       succ(a) div b =rec(succ(a mod b) |-| b, succ(a div b), %x y. a div b) : N"
   4.167  apply (rule divC_succ [THEN trans_elem])
   4.168 -apply (tactic {* rew_tac (thms "div_typing_rls" @ [thm "modC_succ"]) *})
   4.169 +apply (tactic {* rew_tac (@{thms div_typing_rls} @ [@{thm modC_succ}]) *})
   4.170  apply (tactic {* NE_tac @{context} "succ (a mod b) |-|b" 1 *})
   4.171 -apply (tactic {* rew_tac [thm "mod_typing", thm "div_typing", thm "absdiff_typing"] *})
   4.172 +apply (tactic {* rew_tac [@{thm mod_typing}, @{thm div_typing}, @{thm absdiff_typing}] *})
   4.173  done
   4.174  
   4.175  (*for case analysis on whether a number is 0 or a successor*)
   4.176 @@ -451,19 +451,19 @@
   4.177  (*Main Result.  Holds when b is 0 since   a mod 0 = a     and    a div 0 = 0  *)
   4.178  lemma mod_div_equality: "[| a:N;  b:N |] ==> a mod b  #+  (a div b) #* b = a : N"
   4.179  apply (tactic {* NE_tac @{context} "a" 1 *})
   4.180 -apply (tactic {* arith_rew_tac (thms "div_typing_rls" @
   4.181 -  [thm "modC0", thm "modC_succ", thm "divC0", thm "divC_succ2"]) *})
   4.182 +apply (tactic {* arith_rew_tac (@{thms div_typing_rls} @
   4.183 +  [@{thm modC0}, @{thm modC_succ}, @{thm divC0}, @{thm divC_succ2}]) *})
   4.184  apply (rule EqE)
   4.185  (*case analysis on   succ(u mod b)|-|b  *)
   4.186  apply (rule_tac a1 = "succ (u mod b) |-| b" in iszero_decidable [THEN PlusE])
   4.187  apply (erule_tac [3] SumE)
   4.188 -apply (tactic {* hyp_arith_rew_tac (thms "div_typing_rls" @
   4.189 -  [thm "modC0", thm "modC_succ", thm "divC0", thm "divC_succ2"]) *})
   4.190 +apply (tactic {* hyp_arith_rew_tac (@{thms div_typing_rls} @
   4.191 +  [@{thm modC0}, @{thm modC_succ}, @{thm divC0}, @{thm divC_succ2}]) *})
   4.192  (*Replace one occurence of  b  by succ(u mod b).  Clumsy!*)
   4.193  apply (rule add_typingL [THEN trans_elem])
   4.194  apply (erule EqE [THEN absdiff_eq0, THEN sym_elem])
   4.195  apply (rule_tac [3] refl_elem)
   4.196 -apply (tactic {* hyp_arith_rew_tac (thms "div_typing_rls") *})
   4.197 +apply (tactic {* hyp_arith_rew_tac @{thms div_typing_rls} *})
   4.198  done
   4.199  
   4.200  end
     5.1 --- a/src/CTT/ex/Elimination.thy	Mon Sep 06 19:11:01 2010 +0200
     5.2 +++ b/src/CTT/ex/Elimination.thy	Mon Sep 06 19:13:10 2010 +0200
     5.3 @@ -53,7 +53,7 @@
     5.4      and "!!x. x:A ==> B(x) type"
     5.5      and "!!x. x:A ==> C(x) type"
     5.6    shows "?a : (SUM x:A. B(x) + C(x)) --> (SUM x:A. B(x)) + (SUM x:A. C(x))"
     5.7 -apply (tactic {* pc_tac (thms "prems") 1 *})
     5.8 +apply (tactic {* pc_tac @{thms assms} 1 *})
     5.9  done
    5.10  
    5.11  text "Construction of the currying functional"
    5.12 @@ -68,7 +68,7 @@
    5.13      and "!!z. z: (SUM x:A. B(x)) ==> C(z) type"
    5.14    shows "?a : PROD f: (PROD z : (SUM x:A . B(x)) . C(z)).
    5.15                        (PROD x:A . PROD y:B(x) . C(<x,y>))"
    5.16 -apply (tactic {* pc_tac (thms "prems") 1 *})
    5.17 +apply (tactic {* pc_tac @{thms assms} 1 *})
    5.18  done
    5.19  
    5.20  text "Martin-Lof (1984), page 48: axiom of sum-elimination (uncurry)"
    5.21 @@ -83,7 +83,7 @@
    5.22      and "!!z. z: (SUM x:A . B(x)) ==> C(z) type"
    5.23    shows "?a : (PROD x:A . PROD y:B(x) . C(<x,y>))
    5.24          --> (PROD z : (SUM x:A . B(x)) . C(z))"
    5.25 -apply (tactic {* pc_tac (thms "prems") 1 *})
    5.26 +apply (tactic {* pc_tac @{thms assms} 1 *})
    5.27  done
    5.28  
    5.29  text "Function application"
    5.30 @@ -99,7 +99,7 @@
    5.31    shows
    5.32      "?a :     (SUM y:B . PROD x:A . C(x,y))
    5.33            --> (PROD x:A . SUM y:B . C(x,y))"
    5.34 -apply (tactic {* pc_tac (thms "prems") 1 *})
    5.35 +apply (tactic {* pc_tac @{thms assms} 1 *})
    5.36  done
    5.37  
    5.38  text "Martin-Lof (1984) pages 36-7: the combinator S"
    5.39 @@ -109,7 +109,7 @@
    5.40      and "!!x y.[| x:A; y:B(x) |] ==> C(x,y) type"
    5.41    shows "?a :    (PROD x:A. PROD y:B(x). C(x,y))
    5.42               --> (PROD f: (PROD x:A. B(x)). PROD x:A. C(x, f`x))"
    5.43 -apply (tactic {* pc_tac (thms "prems") 1 *})
    5.44 +apply (tactic {* pc_tac @{thms assms} 1 *})
    5.45  done
    5.46  
    5.47  text "Martin-Lof (1984) page 58: the axiom of disjunction elimination"
    5.48 @@ -119,7 +119,7 @@
    5.49      and "!!z. z: A+B ==> C(z) type"
    5.50    shows "?a : (PROD x:A. C(inl(x))) --> (PROD y:B. C(inr(y)))
    5.51            --> (PROD z: A+B. C(z))"
    5.52 -apply (tactic {* pc_tac (thms "prems") 1 *})
    5.53 +apply (tactic {* pc_tac @{thms assms} 1 *})
    5.54  done
    5.55  
    5.56  (*towards AXIOM OF CHOICE*)
    5.57 @@ -137,7 +137,7 @@
    5.58      and "!!x y.[| x:A;  y:B(x) |] ==> C(x,y) type"
    5.59    shows "?a : PROD h: (PROD x:A. SUM y:B(x). C(x,y)).
    5.60                           (SUM f: (PROD x:A. B(x)). PROD x:A. C(x, f`x))"
    5.61 -apply (tactic {* intr_tac (thms "prems") *})
    5.62 +apply (tactic {* intr_tac @{thms assms} *})
    5.63  apply (tactic "add_mp_tac 2")
    5.64  apply (tactic "add_mp_tac 1")
    5.65  apply (erule SumE_fst)
    5.66 @@ -145,7 +145,7 @@
    5.67  apply (rule subst_eqtyparg)
    5.68  apply (rule comp_rls)
    5.69  apply (rule_tac [4] SumE_snd)
    5.70 -apply (tactic {* typechk_tac (thm "SumE_fst" :: thms "prems") *})
    5.71 +apply (tactic {* typechk_tac (@{thm SumE_fst} :: @{thms prems}) *})
    5.72  done
    5.73  
    5.74  text "Axiom of choice.  Proof without fst, snd.  Harder still!"
    5.75 @@ -155,7 +155,7 @@
    5.76      and "!!x y.[| x:A;  y:B(x) |] ==> C(x,y) type"
    5.77    shows "?a : PROD h: (PROD x:A. SUM y:B(x). C(x,y)).
    5.78                           (SUM f: (PROD x:A. B(x)). PROD x:A. C(x, f`x))"
    5.79 -apply (tactic {* intr_tac (thms "prems") *})
    5.80 +apply (tactic {* intr_tac @{thms assms} *})
    5.81  (*Must not use add_mp_tac as subst_prodE hides the construction.*)
    5.82  apply (rule ProdE [THEN SumE], assumption)
    5.83  apply (tactic "TRYALL assume_tac")
    5.84 @@ -163,11 +163,11 @@
    5.85  apply (rule subst_eqtyparg)
    5.86  apply (rule comp_rls)
    5.87  apply (erule_tac [4] ProdE [THEN SumE])
    5.88 -apply (tactic {* typechk_tac (thms "prems") *})
    5.89 +apply (tactic {* typechk_tac @{thms assms} *})
    5.90  apply (rule replace_type)
    5.91  apply (rule subst_eqtyparg)
    5.92  apply (rule comp_rls)
    5.93 -apply (tactic {* typechk_tac (thms "prems") *})
    5.94 +apply (tactic {* typechk_tac @{thms assms} *})
    5.95  apply assumption
    5.96  done
    5.97  
    5.98 @@ -183,11 +183,11 @@
    5.99  apply (tactic {* biresolve_tac safe_brls 2 *})
   5.100  (*Now must convert assumption C(z) into antecedent C(<kd,ke>) *)
   5.101  apply (rule_tac [2] a = "y" in ProdE)
   5.102 -apply (tactic {* typechk_tac (thms "prems") *})
   5.103 +apply (tactic {* typechk_tac @{thms assms} *})
   5.104  apply (rule SumE, assumption)
   5.105  apply (tactic "intr_tac []")
   5.106  apply (tactic "TRYALL assume_tac")
   5.107 -apply (tactic {* typechk_tac (thms "prems") *})
   5.108 +apply (tactic {* typechk_tac @{thms assms} *})
   5.109  done
   5.110  
   5.111  end
     6.1 --- a/src/CTT/ex/Typechecking.thy	Mon Sep 06 19:11:01 2010 +0200
     6.2 +++ b/src/CTT/ex/Typechecking.thy	Mon Sep 06 19:13:10 2010 +0200
     6.3 @@ -66,7 +66,7 @@
     6.4  
     6.5  (*Proofs involving arbitrary types.
     6.6    For concreteness, every type variable left over is forced to be N*)
     6.7 -ML {* val N_tac = TRYALL (rtac (thm "NF")) *}
     6.8 +ML {* val N_tac = TRYALL (rtac @{thm NF}) *}
     6.9  
    6.10  schematic_lemma "lam w. <w,w> : ?A"
    6.11  apply (tactic "typechk_tac []")
     7.1 --- a/src/CTT/rew.ML	Mon Sep 06 19:11:01 2010 +0200
     7.2 +++ b/src/CTT/rew.ML	Mon Sep 06 19:13:10 2010 +0200
     7.3 @@ -8,7 +8,7 @@
     7.4  (*Make list of ProdE RS ProdE ... RS ProdE RS EqE
     7.5    for using assumptions as rewrite rules*)
     7.6  fun peEs 0 = []
     7.7 -  | peEs n = thm "EqE" :: map (curry (op RS) (thm "ProdE")) (peEs (n-1));
     7.8 +  | peEs n = @{thm EqE} :: map (curry (op RS) @{thm ProdE}) (peEs (n-1));
     7.9  
    7.10  (*Tactic used for proving conditions for the cond_rls*)
    7.11  val prove_cond_tac = eresolve_tac (peEs 5);
    7.12 @@ -16,19 +16,19 @@
    7.13  
    7.14  structure TSimp_data: TSIMP_DATA =
    7.15    struct
    7.16 -  val refl              = thm "refl_elem"
    7.17 -  val sym               = thm "sym_elem"
    7.18 -  val trans             = thm "trans_elem"
    7.19 -  val refl_red          = thm "refl_red"
    7.20 -  val trans_red         = thm "trans_red"
    7.21 -  val red_if_equal      = thm "red_if_equal"
    7.22 -  val default_rls       = thms "comp_rls"
    7.23 -  val routine_tac       = routine_tac (thms "routine_rls")
    7.24 +  val refl              = @{thm refl_elem}
    7.25 +  val sym               = @{thm sym_elem}
    7.26 +  val trans             = @{thm trans_elem}
    7.27 +  val refl_red          = @{thm refl_red}
    7.28 +  val trans_red         = @{thm trans_red}
    7.29 +  val red_if_equal      = @{thm red_if_equal}
    7.30 +  val default_rls       = @{thms comp_rls}
    7.31 +  val routine_tac       = routine_tac (@{thms routine_rls})
    7.32    end;
    7.33  
    7.34  structure TSimp = TSimpFun (TSimp_data);
    7.35  
    7.36 -val standard_congr_rls = thms "intrL2_rls" @ thms "elimL_rls";
    7.37 +val standard_congr_rls = @{thms intrL2_rls} @ @{thms elimL_rls};
    7.38  
    7.39  (*Make a rewriting tactic from a normalization tactic*)
    7.40  fun make_rew_tac ntac =
     8.1 --- a/src/FOL/IFOL.thy	Mon Sep 06 19:11:01 2010 +0200
     8.2 +++ b/src/FOL/IFOL.thy	Mon Sep 06 19:13:10 2010 +0200
     8.3 @@ -340,7 +340,7 @@
     8.4    shows "(P&Q) <-> (P'&Q')"
     8.5    apply (insert assms)
     8.6    apply (assumption | rule iffI conjI | erule iffE conjE mp |
     8.7 -    tactic {* iff_tac (thms "assms") 1 *})+
     8.8 +    tactic {* iff_tac @{thms assms} 1 *})+
     8.9    done
    8.10  
    8.11  (*Reversed congruence rule!   Used in ZF/Order*)
    8.12 @@ -350,7 +350,7 @@
    8.13    shows "(Q&P) <-> (Q'&P')"
    8.14    apply (insert assms)
    8.15    apply (assumption | rule iffI conjI | erule iffE conjE mp |
    8.16 -    tactic {* iff_tac (thms "assms") 1 *})+
    8.17 +    tactic {* iff_tac @{thms assms} 1 *})+
    8.18    done
    8.19  
    8.20  lemma disj_cong:
    8.21 @@ -366,7 +366,7 @@
    8.22    shows "(P-->Q) <-> (P'-->Q')"
    8.23    apply (insert assms)
    8.24    apply (assumption | rule iffI impI | erule iffE | erule (1) notE impE |
    8.25 -    tactic {* iff_tac (thms "assms") 1 *})+
    8.26 +    tactic {* iff_tac @{thms assms} 1 *})+
    8.27    done
    8.28  
    8.29  lemma iff_cong: "[| P <-> P'; Q <-> Q' |] ==> (P<->Q) <-> (P'<->Q')"
    8.30 @@ -381,21 +381,21 @@
    8.31    assumes "!!x. P(x) <-> Q(x)"
    8.32    shows "(ALL x. P(x)) <-> (ALL x. Q(x))"
    8.33    apply (assumption | rule iffI allI | erule (1) notE impE | erule allE |
    8.34 -    tactic {* iff_tac (thms "assms") 1 *})+
    8.35 +    tactic {* iff_tac @{thms assms} 1 *})+
    8.36    done
    8.37  
    8.38  lemma ex_cong:
    8.39    assumes "!!x. P(x) <-> Q(x)"
    8.40    shows "(EX x. P(x)) <-> (EX x. Q(x))"
    8.41    apply (erule exE | assumption | rule iffI exI | erule (1) notE impE |
    8.42 -    tactic {* iff_tac (thms "assms") 1 *})+
    8.43 +    tactic {* iff_tac @{thms assms} 1 *})+
    8.44    done
    8.45  
    8.46  lemma ex1_cong:
    8.47    assumes "!!x. P(x) <-> Q(x)"
    8.48    shows "(EX! x. P(x)) <-> (EX! x. Q(x))"
    8.49    apply (erule ex1E spec [THEN mp] | assumption | rule iffI ex1I | erule (1) notE impE |
    8.50 -    tactic {* iff_tac (thms "assms") 1 *})+
    8.51 +    tactic {* iff_tac @{thms assms} 1 *})+
    8.52    done
    8.53  
    8.54  (*** Equality rules ***)
     9.1 --- a/src/FOL/hypsubstdata.ML	Mon Sep 06 19:11:01 2010 +0200
     9.2 +++ b/src/FOL/hypsubstdata.ML	Mon Sep 06 19:13:10 2010 +0200
     9.3 @@ -6,13 +6,13 @@
     9.4    val dest_eq = FOLogic.dest_eq
     9.5    val dest_Trueprop = FOLogic.dest_Trueprop
     9.6    val dest_imp = FOLogic.dest_imp
     9.7 -  val eq_reflection = thm "eq_reflection"
     9.8 -  val rev_eq_reflection = thm "meta_eq_to_obj_eq"
     9.9 -  val imp_intr = thm "impI"
    9.10 -  val rev_mp = thm "rev_mp"
    9.11 -  val subst = thm "subst"
    9.12 -  val sym = thm "sym"
    9.13 -  val thin_refl = thm "thin_refl"
    9.14 +  val eq_reflection = @{thm eq_reflection}
    9.15 +  val rev_eq_reflection = @{thm meta_eq_to_obj_eq}
    9.16 +  val imp_intr = @{thm impI}
    9.17 +  val rev_mp = @{thm rev_mp}
    9.18 +  val subst = @{thm subst}
    9.19 +  val sym = @{thm sym}
    9.20 +  val thin_refl = @{thm thin_refl}
    9.21    val prop_subst = @{lemma "PROP P(t) ==> PROP prop (x = t ==> PROP P(x))"
    9.22                       by (unfold prop_def) (drule eq_reflection, unfold)}
    9.23  end;
    10.1 --- a/src/HOL/Algebra/abstract/Ring2.thy	Mon Sep 06 19:11:01 2010 +0200
    10.2 +++ b/src/HOL/Algebra/abstract/Ring2.thy	Mon Sep 06 19:13:10 2010 +0200
    10.3 @@ -211,11 +211,11 @@
    10.4  fun termless_ring (a, b) = (Term_Ord.term_lpo ring_ord (a, b) = LESS);
    10.5  
    10.6  val ring_ss = HOL_basic_ss settermless termless_ring addsimps
    10.7 -  [thm "a_assoc", thm "l_zero", thm "l_neg", thm "a_comm", thm "m_assoc",
    10.8 -   thm "l_one", thm "l_distr", thm "m_comm", thm "minus_def",
    10.9 -   thm "r_zero", thm "r_neg", thm "r_neg2", thm "r_neg1", thm "minus_add",
   10.10 -   thm "minus_minus", thm "minus0", thm "a_lcomm", thm "m_lcomm", (*thm "r_one",*)
   10.11 -   thm "r_distr", thm "l_null", thm "r_null", thm "l_minus", thm "r_minus"];
   10.12 +  [@{thm a_assoc}, @{thm l_zero}, @{thm l_neg}, @{thm a_comm}, @{thm m_assoc},
   10.13 +   @{thm l_one}, @{thm l_distr}, @{thm m_comm}, @{thm minus_def},
   10.14 +   @{thm r_zero}, @{thm r_neg}, @{thm r_neg2}, @{thm r_neg1}, @{thm minus_add},
   10.15 +   @{thm minus_minus}, @{thm minus0}, @{thm a_lcomm}, @{thm m_lcomm}, (*@{thm r_one},*)
   10.16 +   @{thm r_distr}, @{thm l_null}, @{thm r_null}, @{thm l_minus}, @{thm r_minus}];
   10.17  *}   (* Note: r_one is not necessary in ring_ss *)
   10.18  
   10.19  method_setup ring =
    11.1 --- a/src/HOL/Algebra/poly/LongDiv.thy	Mon Sep 06 19:11:01 2010 +0200
    11.2 +++ b/src/HOL/Algebra/poly/LongDiv.thy	Mon Sep 06 19:13:10 2010 +0200
    11.3 @@ -133,8 +133,8 @@
    11.4    apply (tactic {* simp_tac (@{simpset} addsimps [@{thm l_distr}, @{thm a_assoc}]
    11.5      delsimprocs [ring_simproc]) 1 *})
    11.6    apply (tactic {* asm_simp_tac (@{simpset} delsimprocs [ring_simproc]) 1 *})
    11.7 -  apply (tactic {* simp_tac (@{simpset} addsimps [thm "minus_def", thm "smult_r_distr",
    11.8 -    thm "smult_r_minus", thm "monom_mult_smult", thm "smult_assoc2"]
    11.9 +  apply (tactic {* simp_tac (@{simpset} addsimps [@{thm minus_def}, @{thm smult_r_distr},
   11.10 +    @{thm smult_r_minus}, @{thm monom_mult_smult}, @{thm smult_assoc2}]
   11.11      delsimprocs [ring_simproc]) 1 *})
   11.12    apply (simp add: smult_assoc1 [symmetric])
   11.13    done
   11.14 @@ -169,7 +169,7 @@
   11.15    apply (rule conjI)
   11.16     apply (drule sym)
   11.17     apply (tactic {* asm_simp_tac
   11.18 -     (@{simpset} addsimps [thm "smult_r_distr" RS sym, thm "smult_assoc2"]
   11.19 +     (@{simpset} addsimps [@{thm smult_r_distr} RS sym, @{thm smult_assoc2}]
   11.20       delsimprocs [ring_simproc]) 1 *})
   11.21     apply (simp (no_asm_simp) add: l_inverse_ring unit_power smult_assoc1 [symmetric])
   11.22    (* degree property *)
   11.23 @@ -216,21 +216,21 @@
   11.24      apply (erule disjE)
   11.25    (* r2 = 0 *)
   11.26       apply (tactic {* asm_full_simp_tac (@{simpset}
   11.27 -       addsimps [thm "integral_iff", thm "minus_def", thm "l_zero", thm "uminus_zero"]
   11.28 +       addsimps [@{thm integral_iff}, @{thm minus_def}, @{thm l_zero}, @{thm uminus_zero}]
   11.29         delsimprocs [ring_simproc]) 1 *})
   11.30    (* r2 ~= 0 *)
   11.31      apply (drule_tac f = "deg" and y = "r2 - r1" in arg_cong)
   11.32      apply (tactic {* asm_full_simp_tac (@{simpset} addsimps
   11.33 -      [thm "minus_def", thm "l_zero", thm "uminus_zero"] delsimprocs [ring_simproc]) 1 *})
   11.34 +      [@{thm minus_def}, @{thm l_zero}, @{thm uminus_zero}] delsimprocs [ring_simproc]) 1 *})
   11.35    (* r1 ~=0 *)
   11.36     apply (erule disjE)
   11.37    (* r2 = 0 *)
   11.38      apply (drule_tac f = "deg" and y = "r2 - r1" in arg_cong)
   11.39      apply (tactic {* asm_full_simp_tac (@{simpset} addsimps
   11.40 -      [thm "minus_def", thm "l_zero", thm "uminus_zero"] delsimprocs [ring_simproc]) 1 *})
   11.41 +      [@{thm minus_def}, @{thm l_zero}, @{thm uminus_zero}] delsimprocs [ring_simproc]) 1 *})
   11.42    (* r2 ~= 0 *)
   11.43     apply (drule_tac f = "deg" and y = "r2 - r1" in arg_cong)
   11.44 -   apply (tactic {* asm_full_simp_tac (@{simpset} addsimps [thm "minus_def"]
   11.45 +   apply (tactic {* asm_full_simp_tac (@{simpset} addsimps [@{thm minus_def}]
   11.46       delsimprocs [ring_simproc]) 1 *})
   11.47     apply (drule order_eq_refl [THEN add_leD2])
   11.48     apply (drule leD)
    12.1 --- a/src/HOL/Bali/AxCompl.thy	Mon Sep 06 19:11:01 2010 +0200
    12.2 +++ b/src/HOL/Bali/AxCompl.thy	Mon Sep 06 19:13:10 2010 +0200
    12.3 @@ -1392,7 +1392,7 @@
    12.4  apply -
    12.5  apply (induct_tac "n")
    12.6  apply  (tactic "ALLGOALS (clarsimp_tac @{clasimpset})")
    12.7 -apply  (tactic {* dtac (Thm.permute_prems 0 1 (thm "card_seteq")) 1 *})
    12.8 +apply  (tactic {* dtac (Thm.permute_prems 0 1 @{thm card_seteq}) 1 *})
    12.9  apply    simp
   12.10  apply   (erule finite_imageI)
   12.11  apply  (simp add: MGF_asm ax_derivs_asm)
    13.1 --- a/src/HOL/Bali/AxSem.thy	Mon Sep 06 19:11:01 2010 +0200
    13.2 +++ b/src/HOL/Bali/AxSem.thy	Mon Sep 06 19:13:10 2010 +0200
    13.3 @@ -671,7 +671,7 @@
    13.4  (* 37 subgoals *)
    13.5  prefer 18 (* Methd *)
    13.6  apply (rule ax_derivs.Methd, drule spec, erule mp, fast) 
    13.7 -apply (tactic {* TRYALL (resolve_tac ((funpow 5 tl) (thms "ax_derivs.intros"))) *})
    13.8 +apply (tactic {* TRYALL (resolve_tac ((funpow 5 tl) @{thms ax_derivs.intros})) *})
    13.9  apply auto
   13.10  done
   13.11  
   13.12 @@ -691,8 +691,8 @@
   13.13  apply (erule ax_derivs.induct)
   13.14  (*42 subgoals*)
   13.15  apply       (tactic "ALLGOALS strip_tac")
   13.16 -apply       (tactic {* ALLGOALS(REPEAT o (EVERY'[dtac (thm "subset_singletonD"),
   13.17 -         etac disjE, fast_tac (@{claset} addSIs [thm "ax_derivs.empty"])]))*})
   13.18 +apply       (tactic {* ALLGOALS(REPEAT o (EVERY'[dtac @{thm subset_singletonD},
   13.19 +         etac disjE, fast_tac (@{claset} addSIs @{thms ax_derivs.empty})]))*})
   13.20  apply       (tactic "TRYALL hyp_subst_tac")
   13.21  apply       (simp, rule ax_derivs.empty)
   13.22  apply      (drule subset_insertD)
   13.23 @@ -702,7 +702,7 @@
   13.24  apply   (fast intro: ax_derivs.weaken)
   13.25  apply  (rule ax_derivs.conseq, clarify, tactic "smp_tac 3 1", blast(* unused *))
   13.26  (*37 subgoals*)
   13.27 -apply (tactic {* TRYALL (resolve_tac ((funpow 5 tl) (thms "ax_derivs.intros")) 
   13.28 +apply (tactic {* TRYALL (resolve_tac ((funpow 5 tl) @{thms ax_derivs.intros}) 
   13.29                     THEN_ALL_NEW fast_tac @{claset}) *})
   13.30  (*1 subgoal*)
   13.31  apply (clarsimp simp add: subset_mtriples_iff)
    14.1 --- a/src/HOL/Bali/Eval.thy	Mon Sep 06 19:11:01 2010 +0200
    14.2 +++ b/src/HOL/Bali/Eval.thy	Mon Sep 06 19:13:10 2010 +0200
    14.3 @@ -1168,7 +1168,7 @@
    14.4    "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (w, s') \<Longrightarrow> (\<forall>w' s''. G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (w', s'') \<longrightarrow> w' = w \<and> s'' = s')"
    14.5  apply (erule eval_induct)
    14.6  apply (tactic {* ALLGOALS (EVERY'
    14.7 -      [strip_tac, rotate_tac ~1, eresolve_tac (thms "eval_elim_cases")]) *})
    14.8 +      [strip_tac, rotate_tac ~1, eresolve_tac @{thms eval_elim_cases}]) *})
    14.9  (* 31 subgoals *)
   14.10  prefer 28 (* Try *) 
   14.11  apply (simp (no_asm_use) only: split add: split_if_asm)
    15.1 --- a/src/HOL/Bali/Evaln.thy	Mon Sep 06 19:11:01 2010 +0200
    15.2 +++ b/src/HOL/Bali/Evaln.thy	Mon Sep 06 19:13:10 2010 +0200
    15.3 @@ -449,9 +449,9 @@
    15.4  lemma evaln_nonstrict [rule_format (no_asm), elim]: 
    15.5    "G\<turnstile>s \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (w, s') \<Longrightarrow> \<forall>m. n\<le>m \<longrightarrow> G\<turnstile>s \<midarrow>t\<succ>\<midarrow>m\<rightarrow> (w, s')"
    15.6  apply (erule evaln.induct)
    15.7 -apply (tactic {* ALLGOALS (EVERY'[strip_tac, TRY o etac (thm "Suc_le_D_lemma"),
    15.8 +apply (tactic {* ALLGOALS (EVERY'[strip_tac, TRY o etac @{thm Suc_le_D_lemma},
    15.9    REPEAT o smp_tac 1, 
   15.10 -  resolve_tac (thms "evaln.intros") THEN_ALL_NEW TRY o atac]) *})
   15.11 +  resolve_tac @{thms evaln.intros} THEN_ALL_NEW TRY o atac]) *})
   15.12  (* 3 subgoals *)
   15.13  apply (auto split del: split_if)
   15.14  done
    16.1 --- a/src/HOL/Decision_Procs/mir_tac.ML	Mon Sep 06 19:11:01 2010 +0200
    16.2 +++ b/src/HOL/Decision_Procs/mir_tac.ML	Mon Sep 06 19:13:10 2010 +0200
    16.3 @@ -16,18 +16,18 @@
    16.4  fun trace_msg s = if !trace then tracing s else ();
    16.5  
    16.6  val mir_ss = 
    16.7 -let val ths = map thm ["real_of_int_inject", "real_of_int_less_iff", "real_of_int_le_iff"]
    16.8 +let val ths = [@{thm "real_of_int_inject"}, @{thm "real_of_int_less_iff"}, @{thm "real_of_int_le_iff"}]
    16.9  in @{simpset} delsimps ths addsimps (map (fn th => th RS sym) ths)
   16.10  end;
   16.11  
   16.12  val nT = HOLogic.natT;
   16.13 -  val nat_arith = map thm ["add_nat_number_of", "diff_nat_number_of", 
   16.14 -                       "mult_nat_number_of", "eq_nat_number_of", "less_nat_number_of"];
   16.15 +  val nat_arith = [@{thm "add_nat_number_of"}, @{thm "diff_nat_number_of"},
   16.16 +                       @{thm "mult_nat_number_of"}, @{thm "eq_nat_number_of"}, @{thm "less_nat_number_of"}];
   16.17  
   16.18 -  val comp_arith = (map thm ["Let_def", "if_False", "if_True", "add_0", 
   16.19 -                 "add_Suc", "add_number_of_left", "mult_number_of_left", 
   16.20 -                 "Suc_eq_plus1"])@
   16.21 -                 (map (fn s => thm s RS sym) ["numeral_1_eq_1", "numeral_0_eq_0"])
   16.22 +  val comp_arith = [@{thm "Let_def"}, @{thm "if_False"}, @{thm "if_True"}, @{thm "add_0"},
   16.23 +                 @{thm "add_Suc"}, @{thm "add_number_of_left"}, @{thm "mult_number_of_left"},
   16.24 +                 @{thm "Suc_eq_plus1"}] @
   16.25 +                 (map (fn th => th RS sym) [@{thm "numeral_1_eq_1"}, @{thm "numeral_0_eq_0"}])
   16.26                   @ @{thms arith_simps} @ nat_arith @ @{thms rel_simps} 
   16.27    val ths = [@{thm "mult_numeral_1"}, @{thm "mult_numeral_1_right"}, 
   16.28               @{thm "real_of_nat_number_of"},
    17.1 --- a/src/HOL/HOL.thy	Mon Sep 06 19:11:01 2010 +0200
    17.2 +++ b/src/HOL/HOL.thy	Mon Sep 06 19:13:10 2010 +0200
    17.3 @@ -2089,47 +2089,47 @@
    17.4    fun smp_tac j = EVERY'[dresolve_tac (smp j), atac];
    17.5  end;
    17.6  
    17.7 -val all_conj_distrib = thm "all_conj_distrib";
    17.8 -val all_simps = thms "all_simps";
    17.9 -val atomize_not = thm "atomize_not";
   17.10 -val case_split = thm "case_split";
   17.11 -val cases_simp = thm "cases_simp";
   17.12 -val choice_eq = thm "choice_eq"
   17.13 -val cong = thm "cong"
   17.14 -val conj_comms = thms "conj_comms";
   17.15 -val conj_cong = thm "conj_cong";
   17.16 -val de_Morgan_conj = thm "de_Morgan_conj";
   17.17 -val de_Morgan_disj = thm "de_Morgan_disj";
   17.18 -val disj_assoc = thm "disj_assoc";
   17.19 -val disj_comms = thms "disj_comms";
   17.20 -val disj_cong = thm "disj_cong";
   17.21 -val eq_ac = thms "eq_ac";
   17.22 -val eq_cong2 = thm "eq_cong2"
   17.23 -val Eq_FalseI = thm "Eq_FalseI";
   17.24 -val Eq_TrueI = thm "Eq_TrueI";
   17.25 -val Ex1_def = thm "Ex1_def"
   17.26 -val ex_disj_distrib = thm "ex_disj_distrib";
   17.27 -val ex_simps = thms "ex_simps";
   17.28 -val if_cancel = thm "if_cancel";
   17.29 -val if_eq_cancel = thm "if_eq_cancel";
   17.30 -val if_False = thm "if_False";
   17.31 -val iff_conv_conj_imp = thm "iff_conv_conj_imp";
   17.32 -val iff = thm "iff"
   17.33 -val if_splits = thms "if_splits";
   17.34 -val if_True = thm "if_True";
   17.35 -val if_weak_cong = thm "if_weak_cong"
   17.36 -val imp_all = thm "imp_all";
   17.37 -val imp_cong = thm "imp_cong";
   17.38 -val imp_conjL = thm "imp_conjL";
   17.39 -val imp_conjR = thm "imp_conjR";
   17.40 -val imp_conv_disj = thm "imp_conv_disj";
   17.41 -val simp_implies_def = thm "simp_implies_def";
   17.42 -val simp_thms = thms "simp_thms";
   17.43 -val split_if = thm "split_if";
   17.44 -val the1_equality = thm "the1_equality"
   17.45 -val theI = thm "theI"
   17.46 -val theI' = thm "theI'"
   17.47 -val True_implies_equals = thm "True_implies_equals";
   17.48 +val all_conj_distrib = @{thm all_conj_distrib};
   17.49 +val all_simps = @{thms all_simps};
   17.50 +val atomize_not = @{thm atomize_not};
   17.51 +val case_split = @{thm case_split};
   17.52 +val cases_simp = @{thm cases_simp};
   17.53 +val choice_eq = @{thm choice_eq};
   17.54 +val cong = @{thm cong};
   17.55 +val conj_comms = @{thms conj_comms};
   17.56 +val conj_cong = @{thm conj_cong};
   17.57 +val de_Morgan_conj = @{thm de_Morgan_conj};
   17.58 +val de_Morgan_disj = @{thm de_Morgan_disj};
   17.59 +val disj_assoc = @{thm disj_assoc};
   17.60 +val disj_comms = @{thms disj_comms};
   17.61 +val disj_cong = @{thm disj_cong};
   17.62 +val eq_ac = @{thms eq_ac};
   17.63 +val eq_cong2 = @{thm eq_cong2}
   17.64 +val Eq_FalseI = @{thm Eq_FalseI};
   17.65 +val Eq_TrueI = @{thm Eq_TrueI};
   17.66 +val Ex1_def = @{thm Ex1_def};
   17.67 +val ex_disj_distrib = @{thm ex_disj_distrib};
   17.68 +val ex_simps = @{thms ex_simps};
   17.69 +val if_cancel = @{thm if_cancel};
   17.70 +val if_eq_cancel = @{thm if_eq_cancel};
   17.71 +val if_False = @{thm if_False};
   17.72 +val iff_conv_conj_imp = @{thm iff_conv_conj_imp};
   17.73 +val iff = @{thm iff};
   17.74 +val if_splits = @{thms if_splits};
   17.75 +val if_True = @{thm if_True};
   17.76 +val if_weak_cong = @{thm if_weak_cong};
   17.77 +val imp_all = @{thm imp_all};
   17.78 +val imp_cong = @{thm imp_cong};
   17.79 +val imp_conjL = @{thm imp_conjL};
   17.80 +val imp_conjR = @{thm imp_conjR};
   17.81 +val imp_conv_disj = @{thm imp_conv_disj};
   17.82 +val simp_implies_def = @{thm simp_implies_def};
   17.83 +val simp_thms = @{thms simp_thms};
   17.84 +val split_if = @{thm split_if};
   17.85 +val the1_equality = @{thm the1_equality};
   17.86 +val theI = @{thm theI};
   17.87 +val theI' = @{thm theI'};
   17.88 +val True_implies_equals = @{thm True_implies_equals};
   17.89  val nnf_conv = Simplifier.rewrite (HOL_basic_ss addsimps simp_thms @ @{thms "nnf_simps"})
   17.90  
   17.91  *}
    18.1 --- a/src/HOL/Hoare_Parallel/Mul_Gar_Coll.thy	Mon Sep 06 19:11:01 2010 +0200
    18.2 +++ b/src/HOL/Hoare_Parallel/Mul_Gar_Coll.thy	Mon Sep 06 19:13:10 2010 +0200
    18.3 @@ -1199,15 +1199,15 @@
    18.4  apply(case_tac [!] "M x!(T (Muts x ! j))=Black")
    18.5  apply(simp_all add:Graph10)
    18.6  --{* 47 subgoals left *}
    18.7 -apply(tactic {* TRYALL(EVERY'[REPEAT o (rtac disjI2),etac (thm "subset_psubset_trans"),etac (thm "Graph11"),force_tac @{clasimpset}]) *})
    18.8 +apply(tactic {* TRYALL(EVERY'[REPEAT o (rtac disjI2),etac @{thm subset_psubset_trans}, etac @{thm Graph11},force_tac @{clasimpset}]) *})
    18.9  --{* 41 subgoals left *}
   18.10  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}])]) *})
   18.11  --{* 35 subgoals left *}
   18.12 -apply(tactic {* TRYALL(EVERY'[rtac disjI2,rtac disjI1,etac (thm "psubset_subset_trans"),rtac (thm "Graph9"),force_tac @{clasimpset}]) *})
   18.13 +apply(tactic {* TRYALL(EVERY'[rtac disjI2,rtac disjI1,etac @{thm psubset_subset_trans},rtac @{thm Graph9},force_tac @{clasimpset}]) *})
   18.14  --{* 31 subgoals left *}
   18.15 -apply(tactic {* TRYALL(EVERY'[rtac disjI2,rtac disjI1,etac (thm "subset_psubset_trans"),etac (thm "Graph11"),force_tac @{clasimpset}]) *})
   18.16 +apply(tactic {* TRYALL(EVERY'[rtac disjI2,rtac disjI1,etac @{thm subset_psubset_trans},etac @{thm Graph11},force_tac @{clasimpset}]) *})
   18.17  --{* 29 subgoals left *}
   18.18 -apply(tactic {* TRYALL(EVERY'[REPEAT o (rtac disjI2),etac (thm "subset_psubset_trans"),etac (thm "subset_psubset_trans"),etac (thm "Graph11"),force_tac @{clasimpset}]) *})
   18.19 +apply(tactic {* TRYALL(EVERY'[REPEAT o (rtac disjI2),etac @{thm subset_psubset_trans},etac @{thm subset_psubset_trans},etac @{thm Graph11},force_tac @{clasimpset}]) *})
   18.20  --{* 25 subgoals left *}
   18.21  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}])]) *})
   18.22  --{* 10 subgoals left *}
    19.1 --- a/src/HOL/Hoare_Parallel/OG_Tactics.thy	Mon Sep 06 19:11:01 2010 +0200
    19.2 +++ b/src/HOL/Hoare_Parallel/OG_Tactics.thy	Mon Sep 06 19:13:10 2010 +0200
    19.3 @@ -273,11 +273,11 @@
    19.4  lemmas ParallelConseq_list = INTER_def Collect_conj_eq length_map length_upt length_append list_length
    19.5  
    19.6  ML {*
    19.7 -val before_interfree_simp_tac = (simp_tac (HOL_basic_ss addsimps [thm "com.simps", thm "post.simps"]))
    19.8 +val before_interfree_simp_tac = simp_tac (HOL_basic_ss addsimps [@{thm com.simps}, @{thm post.simps}])
    19.9  
   19.10 -val  interfree_simp_tac = (asm_simp_tac (HOL_ss addsimps [@{thm split}, thm "ball_Un", thm "ball_empty"]@(thms "my_simp_list")))
   19.11 +val  interfree_simp_tac = asm_simp_tac (HOL_ss addsimps [@{thm split}, @{thm ball_Un}, @{thm ball_empty}] @ @{thms my_simp_list})
   19.12  
   19.13 -val ParallelConseq = (simp_tac (HOL_basic_ss addsimps (thms "ParallelConseq_list")@(thms "my_simp_list")))
   19.14 +val ParallelConseq = simp_tac (HOL_basic_ss addsimps @{thms ParallelConseq_list} @ @{thms my_simp_list})
   19.15  *}
   19.16  
   19.17  text {* The following tactic applies @{text tac} to each conjunct in a
    20.1 --- a/src/HOL/IMPP/Hoare.thy	Mon Sep 06 19:11:01 2010 +0200
    20.2 +++ b/src/HOL/IMPP/Hoare.thy	Mon Sep 06 19:13:10 2010 +0200
    20.3 @@ -218,7 +218,7 @@
    20.4  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)
    20.5  prefer 7
    20.6  apply          (rule_tac hoare_derivs.Body, drule_tac spec, erule_tac mp, fast)
    20.7 -apply         (tactic {* ALLGOALS (resolve_tac ((funpow 5 tl) (thms "hoare_derivs.intros")) THEN_ALL_NEW (fast_tac @{claset})) *})
    20.8 +apply         (tactic {* ALLGOALS (resolve_tac ((funpow 5 tl) @{thms hoare_derivs.intros}) THEN_ALL_NEW (fast_tac @{claset})) *})
    20.9  done
   20.10  
   20.11  lemma weak_Body: "G|-{P}. the (body pn) .{Q} ==> G|-{P}. BODY pn .{Q}"
   20.12 @@ -278,7 +278,7 @@
   20.13  
   20.14  lemma hoare_sound: "G||-ts ==> G||=ts"
   20.15  apply (erule hoare_derivs.induct)
   20.16 -apply              (tactic {* TRYALL (eresolve_tac [thm "Loop_sound_lemma", thm "Body_sound_lemma"] THEN_ALL_NEW atac) *})
   20.17 +apply              (tactic {* TRYALL (eresolve_tac [@{thm Loop_sound_lemma}, @{thm Body_sound_lemma}] THEN_ALL_NEW atac) *})
   20.18  apply            (unfold hoare_valids_def)
   20.19  apply            blast
   20.20  apply           blast
   20.21 @@ -349,7 +349,7 @@
   20.22    rule_tac [3] P1 = "%Z' s. s= (Z[Loc loc::=fun Z])" in hoare_derivs.Local [THEN conseq1],
   20.23    erule_tac [3] conseq12)
   20.24  apply         (erule_tac [5] hoare_derivs.Comp, erule_tac [5] conseq12)
   20.25 -apply         (tactic {* (rtac (thm "hoare_derivs.If") THEN_ALL_NEW etac (thm "conseq12")) 6 *})
   20.26 +apply         (tactic {* (rtac @{thm hoare_derivs.If} THEN_ALL_NEW etac @{thm conseq12}) 6 *})
   20.27  apply          (rule_tac [8] hoare_derivs.Loop [THEN conseq2], erule_tac [8] conseq12)
   20.28  apply           auto
   20.29  done
    21.1 --- a/src/HOL/IMPP/Natural.thy	Mon Sep 06 19:11:01 2010 +0200
    21.2 +++ b/src/HOL/IMPP/Natural.thy	Mon Sep 06 19:13:10 2010 +0200
    21.3 @@ -114,7 +114,7 @@
    21.4  
    21.5  lemma evaln_evalc: "<c,s> -n-> t ==> <c,s> -c-> t"
    21.6  apply (erule evaln.induct)
    21.7 -apply (tactic {* ALLGOALS (resolve_tac (thms "evalc.intros") THEN_ALL_NEW atac) *})
    21.8 +apply (tactic {* ALLGOALS (resolve_tac @{thms evalc.intros} THEN_ALL_NEW atac) *})
    21.9  done
   21.10  
   21.11  lemma Suc_le_D_lemma: "[| Suc n <= m'; (!!m. n <= m ==> P (Suc m)) |] ==> P m'"
   21.12 @@ -124,8 +124,8 @@
   21.13  
   21.14  lemma evaln_nonstrict [rule_format]: "<c,s> -n-> t ==> !m. n<=m --> <c,s> -m-> t"
   21.15  apply (erule evaln.induct)
   21.16 -apply (tactic {* ALLGOALS (EVERY'[strip_tac,TRY o etac (thm "Suc_le_D_lemma"), REPEAT o smp_tac 1]) *})
   21.17 -apply (tactic {* ALLGOALS (resolve_tac (thms "evaln.intros") THEN_ALL_NEW atac) *})
   21.18 +apply (tactic {* ALLGOALS (EVERY'[strip_tac,TRY o etac @{thm Suc_le_D_lemma}, REPEAT o smp_tac 1]) *})
   21.19 +apply (tactic {* ALLGOALS (resolve_tac @{thms evaln.intros} THEN_ALL_NEW atac) *})
   21.20  done
   21.21  
   21.22  lemma evaln_Suc: "<c,s> -n-> s' ==> <c,s> -Suc n-> s'"
   21.23 @@ -142,8 +142,8 @@
   21.24  lemma evalc_evaln: "<c,s> -c-> t ==> ? n. <c,s> -n-> t"
   21.25  apply (erule evalc.induct)
   21.26  apply (tactic {* ALLGOALS (REPEAT o etac exE) *})
   21.27 -apply (tactic {* TRYALL (EVERY'[datac (thm "evaln_max2") 1, REPEAT o eresolve_tac [exE, conjE]]) *})
   21.28 -apply (tactic {* ALLGOALS (rtac exI THEN' resolve_tac (thms "evaln.intros") THEN_ALL_NEW atac) *})
   21.29 +apply (tactic {* TRYALL (EVERY' [datac @{thm evaln_max2} 1, REPEAT o eresolve_tac [exE, conjE]]) *})
   21.30 +apply (tactic {* ALLGOALS (rtac exI THEN' resolve_tac @{thms evaln.intros} THEN_ALL_NEW atac) *})
   21.31  done
   21.32  
   21.33  lemma eval_eq: "<c,s> -c-> t = (? n. <c,s> -n-> t)"
    22.1 --- a/src/HOL/IOA/Solve.thy	Mon Sep 06 19:11:01 2010 +0200
    22.2 +++ b/src/HOL/IOA/Solve.thy	Mon Sep 06 19:13:10 2010 +0200
    22.3 @@ -146,7 +146,7 @@
    22.4    apply (simp (no_asm) add: conj_disj_distribR cong add: conj_cong split add: split_if)
    22.5    apply (tactic {*
    22.6      REPEAT((resolve_tac [conjI,impI] 1 ORELSE etac conjE 1) THEN
    22.7 -      asm_full_simp_tac(@{simpset} addsimps[thm "comp1_reachable", thm "comp2_reachable"]) 1) *})
    22.8 +      asm_full_simp_tac(@{simpset} addsimps [@{thm comp1_reachable}, @{thm comp2_reachable}]) 1) *})
    22.9    done
   22.10  
   22.11  
    23.1 --- a/src/HOL/Import/hol4rews.ML	Mon Sep 06 19:11:01 2010 +0200
    23.2 +++ b/src/HOL/Import/hol4rews.ML	Mon Sep 06 19:13:10 2010 +0200
    23.3 @@ -156,13 +156,10 @@
    23.4  val hol4_debug = Unsynchronized.ref false
    23.5  fun message s = if !hol4_debug then writeln s else ()
    23.6  
    23.7 -local
    23.8 -  val eq_reflection = thm "eq_reflection"
    23.9 -in
   23.10  fun add_hol4_rewrite (Context.Theory thy, th) =
   23.11      let
   23.12          val _ = message "Adding HOL4 rewrite"
   23.13 -        val th1 = th RS eq_reflection
   23.14 +        val th1 = th RS @{thm eq_reflection}
   23.15          val current_rews = HOL4Rewrites.get thy
   23.16          val new_rews = insert Thm.eq_thm th1 current_rews
   23.17          val updated_thy  = HOL4Rewrites.put new_rews thy
   23.18 @@ -170,7 +167,6 @@
   23.19          (Context.Theory updated_thy,th1)
   23.20      end
   23.21    | add_hol4_rewrite (context, th) = (context, th RS eq_reflection);
   23.22 -end
   23.23  
   23.24  fun ignore_hol4 bthy bthm thy =
   23.25      let
    24.1 --- a/src/HOL/Import/proof_kernel.ML	Mon Sep 06 19:11:01 2010 +0200
    24.2 +++ b/src/HOL/Import/proof_kernel.ML	Mon Sep 06 19:13:10 2010 +0200
    24.3 @@ -977,28 +977,28 @@
    24.4            | NONE => raise ERR "uniq_compose" "No result"
    24.5      end
    24.6  
    24.7 -val reflexivity_thm = thm "refl"
    24.8 -val substitution_thm = thm "subst"
    24.9 -val mp_thm = thm "mp"
   24.10 -val imp_antisym_thm = thm "light_imp_as"
   24.11 -val disch_thm = thm "impI"
   24.12 -val ccontr_thm = thm "ccontr"
   24.13 +val reflexivity_thm = @{thm refl}
   24.14 +val substitution_thm = @{thm subst}
   24.15 +val mp_thm = @{thm mp}
   24.16 +val imp_antisym_thm = @{thm light_imp_as}
   24.17 +val disch_thm = @{thm impI}
   24.18 +val ccontr_thm = @{thm ccontr}
   24.19  
   24.20 -val meta_eq_to_obj_eq_thm = thm "meta_eq_to_obj_eq"
   24.21 +val meta_eq_to_obj_eq_thm = @{thm meta_eq_to_obj_eq}
   24.22  
   24.23 -val gen_thm = thm "HOLallI"
   24.24 -val choose_thm = thm "exE"
   24.25 -val exists_thm = thm "exI"
   24.26 -val conj_thm = thm "conjI"
   24.27 -val conjunct1_thm = thm "conjunct1"
   24.28 -val conjunct2_thm = thm "conjunct2"
   24.29 -val spec_thm = thm "spec"
   24.30 -val disj_cases_thm = thm "disjE"
   24.31 -val disj1_thm = thm "disjI1"
   24.32 -val disj2_thm = thm "disjI2"
   24.33 +val gen_thm = @{thm HOLallI}
   24.34 +val choose_thm = @{thm exE}
   24.35 +val exists_thm = @{thm exI}
   24.36 +val conj_thm = @{thm conjI}
   24.37 +val conjunct1_thm = @{thm conjunct1}
   24.38 +val conjunct2_thm = @{thm conjunct2}
   24.39 +val spec_thm = @{thm spec}
   24.40 +val disj_cases_thm = @{thm disjE}
   24.41 +val disj1_thm = @{thm disjI1}
   24.42 +val disj2_thm = @{thm disjI2}
   24.43  
   24.44  local
   24.45 -    val th = thm "not_def"
   24.46 +    val th = @{thm not_def}
   24.47      val thy = theory_of_thm th
   24.48      val pp = Thm.reflexive (cterm_of thy (Const(@{const_name Trueprop},HOLogic.boolT-->propT)))
   24.49  in
   24.50 @@ -1006,13 +1006,13 @@
   24.51  end
   24.52  
   24.53  val not_intro_thm = Thm.symmetric not_elim_thm
   24.54 -val abs_thm = thm "ext"
   24.55 -val trans_thm = thm "trans"
   24.56 -val symmetry_thm = thm "sym"
   24.57 -val transitivity_thm = thm "trans"
   24.58 -val eqmp_thm = thm "iffD1"
   24.59 -val eqimp_thm = thm "HOL4Setup.eq_imp"
   24.60 -val comb_thm = thm "cong"
   24.61 +val abs_thm = @{thm ext}
   24.62 +val trans_thm = @{thm trans}
   24.63 +val symmetry_thm = @{thm sym}
   24.64 +val transitivity_thm = @{thm trans}
   24.65 +val eqmp_thm = @{thm iffD1}
   24.66 +val eqimp_thm = @{thm HOL4Setup.eq_imp}
   24.67 +val comb_thm = @{thm cong}
   24.68  
   24.69  (* Beta-eta normalizes a theorem (only the conclusion, not the *
   24.70  hypotheses!)  *)
   24.71 @@ -1971,9 +1971,6 @@
   24.72          (thy22',hth)
   24.73      end
   24.74  
   24.75 -local
   24.76 -    val helper = thm "termspec_help"
   24.77 -in
   24.78  fun new_specification thyname thmname names hth thy =
   24.79      case HOL4DefThy.get thy of
   24.80          Replaying _ => (thy,hth)
   24.81 @@ -2054,8 +2051,6 @@
   24.82              intern_store_thm false thyname thmname hth thy''
   24.83          end
   24.84  
   24.85 -end
   24.86 -
   24.87  fun new_axiom name tm thy = raise ERR "new_axiom" ("Oh, no you don't! (" ^ name ^ ")")
   24.88  
   24.89  fun to_isa_thm (hth as HOLThm(_,th)) =
   24.90 @@ -2068,10 +2063,10 @@
   24.91  fun to_isa_term tm = tm
   24.92  
   24.93  local
   24.94 -    val light_nonempty = thm "light_ex_imp_nonempty"
   24.95 -    val ex_imp_nonempty = thm "ex_imp_nonempty"
   24.96 -    val typedef_hol2hol4 = thm "typedef_hol2hol4"
   24.97 -    val typedef_hol2hollight = thm "typedef_hol2hollight"
   24.98 +    val light_nonempty = @{thm light_ex_imp_nonempty}
   24.99 +    val ex_imp_nonempty = @{thm ex_imp_nonempty}
  24.100 +    val typedef_hol2hol4 = @{thm typedef_hol2hol4}
  24.101 +    val typedef_hol2hollight = @{thm typedef_hol2hollight}
  24.102  in
  24.103  fun new_type_definition thyname thmname tycname hth thy =
  24.104      case HOL4DefThy.get thy of
    25.1 --- a/src/HOL/Import/shuffler.ML	Mon Sep 06 19:11:01 2010 +0200
    25.2 +++ b/src/HOL/Import/shuffler.ML	Mon Sep 06 19:13:10 2010 +0200
    25.3 @@ -346,7 +346,7 @@
    25.4  fun beta_fun thy assume t =
    25.5      SOME (Thm.beta_conversion true (cterm_of thy t))
    25.6  
    25.7 -val meta_sym_rew = thm "refl"
    25.8 +val meta_sym_rew = @{thm refl}
    25.9  
   25.10  fun equals_fun thy assume t =
   25.11      case t of
    26.1 --- a/src/HOL/MicroJava/J/JTypeSafe.thy	Mon Sep 06 19:11:01 2010 +0200
    26.2 +++ b/src/HOL/MicroJava/J/JTypeSafe.thy	Mon Sep 06 19:13:10 2010 +0200
    26.3 @@ -201,7 +201,7 @@
    26.4  -- "several simplifications, XcptE, XcptEs, XcptS, Skip, Nil??"
    26.5  apply( simp_all)
    26.6  apply( tactic "ALLGOALS strip_tac")
    26.7 -apply( tactic {* ALLGOALS (eresolve_tac [thm "ty_expr.cases", thm "ty_exprs.cases", thm "wt_stmt.cases"]
    26.8 +apply( tactic {* ALLGOALS (eresolve_tac [@{thm ty_expr.cases}, @{thm ty_exprs.cases}, @{thm wt_stmt.cases}]
    26.9                   THEN_ALL_NEW (full_simp_tac (global_simpset_of @{theory Conform}))) *})
   26.10  apply(tactic "ALLGOALS (EVERY' [REPEAT o (etac conjE), REPEAT o hyp_subst_tac])")
   26.11  
   26.12 @@ -241,7 +241,7 @@
   26.13  apply( fast elim: conforms_localD [THEN lconfD])
   26.14  
   26.15  -- "for FAss"
   26.16 -apply( tactic {* EVERY'[eresolve_tac [thm "ty_expr.cases", thm "ty_exprs.cases", thm "wt_stmt.cases"] 
   26.17 +apply( tactic {* EVERY'[eresolve_tac [@{thm ty_expr.cases}, @{thm ty_exprs.cases}, @{thm wt_stmt.cases}] 
   26.18         THEN_ALL_NEW (full_simp_tac @{simpset}), REPEAT o (etac conjE), hyp_subst_tac] 3*})
   26.19  
   26.20  -- "for if"
   26.21 @@ -277,7 +277,7 @@
   26.22  
   26.23  -- "7 LAss"
   26.24  apply (fold fun_upd_def)
   26.25 -apply( tactic {* (eresolve_tac [thm "ty_expr.cases", thm "ty_exprs.cases", thm "wt_stmt.cases"] 
   26.26 +apply( tactic {* (eresolve_tac [@{thm ty_expr.cases}, @{thm ty_exprs.cases}, @{thm wt_stmt.cases}] 
   26.27                   THEN_ALL_NEW (full_simp_tac @{simpset})) 1 *})
   26.28  apply (intro strip)
   26.29  apply (case_tac E)
    27.1 --- a/src/HOL/NSA/NSA.thy	Mon Sep 06 19:11:01 2010 +0200
    27.2 +++ b/src/HOL/NSA/NSA.thy	Mon Sep 06 19:13:10 2010 +0200
    27.3 @@ -663,9 +663,9 @@
    27.4   ***)
    27.5  
    27.6  (*reorientation simprules using ==, for the following simproc*)
    27.7 -val meta_zero_approx_reorient = thm "zero_approx_reorient" RS eq_reflection;
    27.8 -val meta_one_approx_reorient = thm "one_approx_reorient" RS eq_reflection;
    27.9 -val meta_number_of_approx_reorient = thm "number_of_approx_reorient" RS eq_reflection
   27.10 +val meta_zero_approx_reorient = @{thm zero_approx_reorient} RS eq_reflection;
   27.11 +val meta_one_approx_reorient = @{thm one_approx_reorient} RS eq_reflection;
   27.12 +val meta_number_of_approx_reorient = @{thm number_of_approx_reorient} RS eq_reflection
   27.13  
   27.14  (*reorientation simplification procedure: reorients (polymorphic)
   27.15    0 = x, 1 = x, nnn = x provided x isn't 0, 1 or a numeral.*)
    28.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Mon Sep 06 19:11:01 2010 +0200
    28.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Mon Sep 06 19:13:10 2010 +0200
    28.3 @@ -24,18 +24,18 @@
    28.4  structure NominalDatatype : NOMINAL_DATATYPE =
    28.5  struct
    28.6  
    28.7 -val finite_emptyI = thm "finite.emptyI";
    28.8 -val finite_Diff = thm "finite_Diff";
    28.9 -val finite_Un = thm "finite_Un";
   28.10 -val Un_iff = thm "Un_iff";
   28.11 -val In0_eq = thm "In0_eq";
   28.12 -val In1_eq = thm "In1_eq";
   28.13 -val In0_not_In1 = thm "In0_not_In1";
   28.14 -val In1_not_In0 = thm "In1_not_In0";
   28.15 -val Un_assoc = thm "Un_assoc";
   28.16 -val Collect_disj_eq = thm "Collect_disj_eq";
   28.17 +val finite_emptyI = @{thm finite.emptyI};
   28.18 +val finite_Diff = @{thm finite_Diff};
   28.19 +val finite_Un = @{thm finite_Un};
   28.20 +val Un_iff = @{thm Un_iff};
   28.21 +val In0_eq = @{thm In0_eq};
   28.22 +val In1_eq = @{thm In1_eq};
   28.23 +val In0_not_In1 = @{thm In0_not_In1};
   28.24 +val In1_not_In0 = @{thm In1_not_In0};
   28.25 +val Un_assoc = @{thm Un_assoc};
   28.26 +val Collect_disj_eq = @{thm Collect_disj_eq};
   28.27  val Collect_False_empty = @{thm empty_def [THEN sym, THEN eq_reflection]};
   28.28 -val empty_iff = thm "empty_iff";
   28.29 +val empty_iff = @{thm empty_iff};
   28.30  
   28.31  open Datatype_Aux;
   28.32  open NominalAtoms;
   28.33 @@ -119,7 +119,7 @@
   28.34  
   28.35  (** simplification procedure for sorting permutations **)
   28.36  
   28.37 -val dj_cp = thm "dj_cp";
   28.38 +val dj_cp = @{thm dj_cp};
   28.39  
   28.40  fun dest_permT (Type ("fun", [Type ("List.list", [Type (@{type_name Product_Type.prod}, [T, _])]),
   28.41        Type ("fun", [_, U])])) = (T, U);
   28.42 @@ -148,23 +148,21 @@
   28.43  val perm_simproc =
   28.44    Simplifier.simproc_global @{theory} "perm_simp" ["pi1 \<bullet> (pi2 \<bullet> x)"] perm_simproc';
   28.45  
   28.46 -val meta_spec = thm "meta_spec";
   28.47 -
   28.48  fun projections rule =
   28.49    Project_Rule.projections (ProofContext.init_global (Thm.theory_of_thm rule)) rule
   28.50    |> map (Drule.export_without_context #> Rule_Cases.save rule);
   28.51  
   28.52 -val supp_prod = thm "supp_prod";
   28.53 -val fresh_prod = thm "fresh_prod";
   28.54 -val supports_fresh = thm "supports_fresh";
   28.55 -val supports_def = thm "Nominal.supports_def";
   28.56 -val fresh_def = thm "fresh_def";
   28.57 -val supp_def = thm "supp_def";
   28.58 -val rev_simps = thms "rev.simps";
   28.59 -val app_simps = thms "append.simps";
   28.60 -val at_fin_set_supp = thm "at_fin_set_supp";
   28.61 -val at_fin_set_fresh = thm "at_fin_set_fresh";
   28.62 -val abs_fun_eq1 = thm "abs_fun_eq1";
   28.63 +val supp_prod = @{thm supp_prod};
   28.64 +val fresh_prod = @{thm fresh_prod};
   28.65 +val supports_fresh = @{thm supports_fresh};
   28.66 +val supports_def = @{thm Nominal.supports_def};
   28.67 +val fresh_def = @{thm fresh_def};
   28.68 +val supp_def = @{thm supp_def};
   28.69 +val rev_simps = @{thms rev.simps};
   28.70 +val app_simps = @{thms append.simps};
   28.71 +val at_fin_set_supp = @{thm at_fin_set_supp};
   28.72 +val at_fin_set_fresh = @{thm at_fin_set_fresh};
   28.73 +val abs_fun_eq1 = @{thm abs_fun_eq1};
   28.74  
   28.75  val collect_simp = rewrite_rule [mk_meta_eq mem_Collect_eq];
   28.76  
   28.77 @@ -1406,7 +1404,7 @@
   28.78           [rtac induct_aux' 1,
   28.79            REPEAT (resolve_tac fs_atoms 1),
   28.80            REPEAT ((resolve_tac prems THEN_ALL_NEW
   28.81 -            (etac meta_spec ORELSE' full_simp_tac (HOL_basic_ss addsimps [fresh_def]))) 1)])
   28.82 +            (etac @{thm meta_spec} ORELSE' full_simp_tac (HOL_basic_ss addsimps [fresh_def]))) 1)])
   28.83  
   28.84      val (_, thy10) = thy9 |>
   28.85        Sign.add_path big_name |>
    29.1 --- a/src/HOL/Nominal/nominal_inductive.ML	Mon Sep 06 19:11:01 2010 +0200
    29.2 +++ b/src/HOL/Nominal/nominal_inductive.ML	Mon Sep 06 19:13:10 2010 +0200
    29.3 @@ -30,10 +30,10 @@
    29.4  
    29.5  fun preds_of ps t = inter (op = o apfst dest_Free) (Term.add_frees t []) ps;
    29.6  
    29.7 -val fresh_prod = thm "fresh_prod";
    29.8 +val fresh_prod = @{thm fresh_prod};
    29.9  
   29.10 -val perm_bool = mk_meta_eq (thm "perm_bool");
   29.11 -val perm_boolI = thm "perm_boolI";
   29.12 +val perm_bool = mk_meta_eq @{thm perm_bool};
   29.13 +val perm_boolI = @{thm perm_boolI};
   29.14  val (_, [perm_boolI_pi, _]) = Drule.strip_comb (snd (Thm.dest_comb
   29.15    (Drule.strip_imp_concl (cprop_of perm_boolI))));
   29.16  
    30.1 --- a/src/HOL/Nominal/nominal_inductive2.ML	Mon Sep 06 19:11:01 2010 +0200
    30.2 +++ b/src/HOL/Nominal/nominal_inductive2.ML	Mon Sep 06 19:13:10 2010 +0200
    30.3 @@ -36,8 +36,8 @@
    30.4  
    30.5  fun preds_of ps t = inter (op = o apfst dest_Free) (Term.add_frees t []) ps;
    30.6  
    30.7 -val perm_bool = mk_meta_eq (thm "perm_bool");
    30.8 -val perm_boolI = thm "perm_boolI";
    30.9 +val perm_bool = mk_meta_eq @{thm perm_bool};
   30.10 +val perm_boolI = @{thm perm_boolI};
   30.11  val (_, [perm_boolI_pi, _]) = Drule.strip_comb (snd (Thm.dest_comb
   30.12    (Drule.strip_imp_concl (cprop_of perm_boolI))));
   30.13  
    31.1 --- a/src/HOL/Old_Number_Theory/Chinese.thy	Mon Sep 06 19:11:01 2010 +0200
    31.2 +++ b/src/HOL/Old_Number_Theory/Chinese.thy	Mon Sep 06 19:13:10 2010 +0200
    31.3 @@ -169,11 +169,11 @@
    31.4    "0 < n ==> i \<le> n ==> m_cond n mf ==> km_cond n kf mf
    31.5      ==> \<exists>!x. 0 \<le> x \<and> x < mf i \<and> [kf i * mhf mf n i * x = bf i] (mod mf i)"
    31.6    apply (rule zcong_lineq_unique)
    31.7 -   apply (tactic {* stac (thm "zgcd_zmult_cancel") 2 *})
    31.8 +   apply (tactic {* stac @{thm zgcd_zmult_cancel} 2 *})
    31.9      apply (unfold m_cond_def km_cond_def mhf_def)
   31.10      apply (simp_all (no_asm_simp))
   31.11    apply safe
   31.12 -    apply (tactic {* stac (thm "zgcd_zmult_cancel") 3 *})
   31.13 +    apply (tactic {* stac @{thm zgcd_zmult_cancel} 3 *})
   31.14       apply (rule_tac [!] funprod_zgcd)
   31.15       apply safe
   31.16       apply simp_all
   31.17 @@ -231,12 +231,12 @@
   31.18    apply (rule_tac x = "x_sol n kf bf mf mod funprod mf 0 n" in exI)
   31.19    apply (unfold lincong_sol_def)
   31.20    apply safe
   31.21 -    apply (tactic {* stac (thm "zcong_zmod") 3 *})
   31.22 -    apply (tactic {* stac (thm "mod_mult_eq") 3 *})
   31.23 -    apply (tactic {* stac (thm "mod_mod_cancel") 3 *})
   31.24 -      apply (tactic {* stac (thm "x_sol_lin") 4 *})
   31.25 -        apply (tactic {* stac (thm "mod_mult_eq" RS sym) 6 *})
   31.26 -        apply (tactic {* stac (thm "zcong_zmod" RS sym) 6 *})
   31.27 +    apply (tactic {* stac @{thm zcong_zmod} 3 *})
   31.28 +    apply (tactic {* stac @{thm mod_mult_eq} 3 *})
   31.29 +    apply (tactic {* stac @{thm mod_mod_cancel} 3 *})
   31.30 +      apply (tactic {* stac @{thm x_sol_lin} 4 *})
   31.31 +        apply (tactic {* stac (@{thm mod_mult_eq} RS sym) 6 *})
   31.32 +        apply (tactic {* stac (@{thm zcong_zmod} RS sym) 6 *})
   31.33          apply (subgoal_tac [6]
   31.34            "0 \<le> xilin_sol i n kf bf mf \<and> xilin_sol i n kf bf mf < mf i
   31.35            \<and> [kf i * mhf mf n i * xilin_sol i n kf bf mf = bf i] (mod mf i)")
    32.1 --- a/src/HOL/Old_Number_Theory/IntPrimes.thy	Mon Sep 06 19:11:01 2010 +0200
    32.2 +++ b/src/HOL/Old_Number_Theory/IntPrimes.thy	Mon Sep 06 19:13:10 2010 +0200
    32.3 @@ -399,7 +399,7 @@
    32.4      zgcd a n = 1 ==> \<exists>!x. 0 \<le> x \<and> x < n \<and> [a * x = b] (mod n)"
    32.5    apply auto
    32.6     apply (rule_tac [2] zcong_zless_imp_eq)
    32.7 -       apply (tactic {* stac (thm "zcong_cancel2" RS sym) 6 *})
    32.8 +       apply (tactic {* stac (@{thm zcong_cancel2} RS sym) 6 *})
    32.9           apply (rule_tac [8] zcong_trans)
   32.10            apply (simp_all (no_asm_simp))
   32.11     prefer 2
    33.1 --- a/src/HOL/Old_Number_Theory/WilsonBij.thy	Mon Sep 06 19:11:01 2010 +0200
    33.2 +++ b/src/HOL/Old_Number_Theory/WilsonBij.thy	Mon Sep 06 19:13:10 2010 +0200
    33.3 @@ -145,9 +145,9 @@
    33.4    apply (unfold inj_on_def)
    33.5    apply auto
    33.6    apply (rule zcong_zless_imp_eq)
    33.7 -      apply (tactic {* stac (thm "zcong_cancel" RS sym) 5 *})
    33.8 +      apply (tactic {* stac (@{thm zcong_cancel} RS sym) 5 *})
    33.9          apply (rule_tac [7] zcong_trans)
   33.10 -         apply (tactic {* stac (thm "zcong_sym") 8 *})
   33.11 +         apply (tactic {* stac @{thm zcong_sym} 8 *})
   33.12           apply (erule_tac [7] inv_is_inv)
   33.13            apply (tactic "asm_simp_tac @{simpset} 9")
   33.14            apply (erule_tac [9] inv_is_inv)
   33.15 @@ -198,15 +198,15 @@
   33.16    apply (unfold reciR_def uniqP_def)
   33.17    apply auto
   33.18     apply (rule zcong_zless_imp_eq)
   33.19 -       apply (tactic {* stac (thm "zcong_cancel2" RS sym) 5 *})
   33.20 +       apply (tactic {* stac (@{thm zcong_cancel2} RS sym) 5 *})
   33.21           apply (rule_tac [7] zcong_trans)
   33.22 -          apply (tactic {* stac (thm "zcong_sym") 8 *})
   33.23 +          apply (tactic {* stac @{thm zcong_sym} 8 *})
   33.24            apply (rule_tac [6] zless_zprime_imp_zrelprime)
   33.25              apply auto
   33.26    apply (rule zcong_zless_imp_eq)
   33.27 -      apply (tactic {* stac (thm "zcong_cancel" RS sym) 5 *})
   33.28 +      apply (tactic {* stac (@{thm zcong_cancel} RS sym) 5 *})
   33.29          apply (rule_tac [7] zcong_trans)
   33.30 -         apply (tactic {* stac (thm "zcong_sym") 8 *})
   33.31 +         apply (tactic {* stac @{thm zcong_sym} 8 *})
   33.32           apply (rule_tac [6] zless_zprime_imp_zrelprime)
   33.33             apply auto
   33.34    done
    34.1 --- a/src/HOL/Old_Number_Theory/WilsonRuss.thy	Mon Sep 06 19:11:01 2010 +0200
    34.2 +++ b/src/HOL/Old_Number_Theory/WilsonRuss.thy	Mon Sep 06 19:13:10 2010 +0200
    34.3 @@ -257,7 +257,7 @@
    34.4     apply (subst wset.simps)
    34.5     apply (auto, unfold Let_def, auto)
    34.6    apply (subst setprod_insert)
    34.7 -    apply (tactic {* stac (thm "setprod_insert") 3 *})
    34.8 +    apply (tactic {* stac @{thm setprod_insert} 3 *})
    34.9        apply (subgoal_tac [5]
   34.10          "zcong (a * inv p a * (\<Prod>x\<in>wset (a - 1) p. x)) (1 * 1) p")
   34.11         prefer 5
    35.1 --- a/src/HOL/Option.thy	Mon Sep 06 19:11:01 2010 +0200
    35.2 +++ b/src/HOL/Option.thy	Mon Sep 06 19:13:10 2010 +0200
    35.3 @@ -47,7 +47,7 @@
    35.4    by simp
    35.5  
    35.6  declaration {* fn _ =>
    35.7 -  Classical.map_cs (fn cs => cs addSD2 ("ospec", thm "ospec"))
    35.8 +  Classical.map_cs (fn cs => cs addSD2 ("ospec", @{thm ospec}))
    35.9  *}
   35.10  
   35.11  lemma elem_set [iff]: "(x : set xo) = (xo = Some x)"
    36.1 --- a/src/HOL/Proofs/Lambda/Commutation.thy	Mon Sep 06 19:11:01 2010 +0200
    36.2 +++ b/src/HOL/Proofs/Lambda/Commutation.thy	Mon Sep 06 19:13:10 2010 +0200
    36.3 @@ -130,9 +130,9 @@
    36.4    apply (tactic {* safe_tac HOL_cs *})
    36.5     apply (tactic {*
    36.6       blast_tac (HOL_cs addIs
    36.7 -       [thm "sup_ge2" RS thm "rtranclp_mono" RS thm "predicate2D" RS thm "rtranclp_trans",
    36.8 -        thm "rtranclp_converseI", thm "conversepI",
    36.9 -        thm "sup_ge1" RS thm "rtranclp_mono" RS thm "predicate2D"]) 1 *})
   36.10 +       [@{thm sup_ge2} RS @{thm rtranclp_mono} RS @{thm predicate2D} RS @{thm rtranclp_trans},
   36.11 +        @{thm rtranclp_converseI}, @{thm conversepI},
   36.12 +        @{thm sup_ge1} RS @{thm rtranclp_mono} RS @{thm predicate2D}]) 1 *})
   36.13    apply (erule rtranclp_induct)
   36.14     apply blast
   36.15    apply (blast del: rtranclp.rtrancl_refl intro: rtranclp_trans)
    37.1 --- a/src/HOL/Statespace/distinct_tree_prover.ML	Mon Sep 06 19:11:01 2010 +0200
    37.2 +++ b/src/HOL/Statespace/distinct_tree_prover.ML	Mon Sep 06 19:13:10 2010 +0200
    37.3 @@ -23,18 +23,19 @@
    37.4  
    37.5  structure DistinctTreeProver : DISTINCT_TREE_PROVER =
    37.6  struct
    37.7 -val all_distinct_left = thm "DistinctTreeProver.all_distinct_left";
    37.8 -val all_distinct_right = thm "DistinctTreeProver.all_distinct_right";
    37.9 +
   37.10 +val all_distinct_left = @{thm DistinctTreeProver.all_distinct_left};
   37.11 +val all_distinct_right = @{thm DistinctTreeProver.all_distinct_right};
   37.12  
   37.13 -val distinct_left = thm "DistinctTreeProver.distinct_left";
   37.14 -val distinct_right = thm "DistinctTreeProver.distinct_right";
   37.15 -val distinct_left_right = thm "DistinctTreeProver.distinct_left_right";
   37.16 -val in_set_root = thm "DistinctTreeProver.in_set_root";
   37.17 -val in_set_left = thm "DistinctTreeProver.in_set_left";
   37.18 -val in_set_right = thm "DistinctTreeProver.in_set_right";
   37.19 +val distinct_left = @{thm DistinctTreeProver.distinct_left};
   37.20 +val distinct_right = @{thm DistinctTreeProver.distinct_right};
   37.21 +val distinct_left_right = @{thm DistinctTreeProver.distinct_left_right};
   37.22 +val in_set_root = @{thm DistinctTreeProver.in_set_root};
   37.23 +val in_set_left = @{thm DistinctTreeProver.in_set_left};
   37.24 +val in_set_right = @{thm DistinctTreeProver.in_set_right};
   37.25  
   37.26 -val swap_neq = thm "DistinctTreeProver.swap_neq";
   37.27 -val neq_to_eq_False = thm "DistinctTreeProver.neq_to_eq_False"
   37.28 +val swap_neq = @{thm DistinctTreeProver.swap_neq};
   37.29 +val neq_to_eq_False = @{thm DistinctTreeProver.neq_to_eq_False};
   37.30  
   37.31  datatype Direction = Left | Right 
   37.32  
   37.33 @@ -273,9 +274,9 @@
   37.34    end  
   37.35  
   37.36  
   37.37 -val delete_root = thm "DistinctTreeProver.delete_root";
   37.38 -val delete_left = thm "DistinctTreeProver.delete_left";
   37.39 -val delete_right = thm "DistinctTreeProver.delete_right";
   37.40 +val delete_root = @{thm DistinctTreeProver.delete_root};
   37.41 +val delete_left = @{thm DistinctTreeProver.delete_left};
   37.42 +val delete_right = @{thm DistinctTreeProver.delete_right};
   37.43  
   37.44  fun deleteProver dist_thm [] = delete_root OF [dist_thm]
   37.45    | deleteProver dist_thm (p::ps) =
   37.46 @@ -286,10 +287,10 @@
   37.47         val del = deleteProver dist_thm' ps;
   37.48       in discharge [dist_thm, del] del_rule end;
   37.49  
   37.50 -val subtract_Tip = thm "DistinctTreeProver.subtract_Tip";
   37.51 -val subtract_Node = thm "DistinctTreeProver.subtract_Node";
   37.52 -val delete_Some_all_distinct = thm "DistinctTreeProver.delete_Some_all_distinct";
   37.53 -val subtract_Some_all_distinct_res = thm "DistinctTreeProver.subtract_Some_all_distinct_res";
   37.54 +val subtract_Tip = @{thm DistinctTreeProver.subtract_Tip};
   37.55 +val subtract_Node = @{thm DistinctTreeProver.subtract_Node};
   37.56 +val delete_Some_all_distinct = @{thm DistinctTreeProver.delete_Some_all_distinct};
   37.57 +val subtract_Some_all_distinct_res = @{thm DistinctTreeProver.subtract_Some_all_distinct_res};
   37.58  
   37.59  local
   37.60    val (alpha,v) = 
   37.61 @@ -320,7 +321,7 @@
   37.62      in discharge [del_tree, sub_l, sub_r] subtract_Node end
   37.63  end
   37.64  
   37.65 -val subtract_Some_all_distinct = thm "DistinctTreeProver.subtract_Some_all_distinct";
   37.66 +val subtract_Some_all_distinct = @{thm DistinctTreeProver.subtract_Some_all_distinct};
   37.67  fun distinct_implProver dist_thm ct =
   37.68    let
   37.69      val ctree = ct |> Thm.dest_comb |> #2 |> Thm.dest_comb |> #2;
    38.1 --- a/src/HOL/Statespace/state_fun.ML	Mon Sep 06 19:11:01 2010 +0200
    38.2 +++ b/src/HOL/Statespace/state_fun.ML	Mon Sep 06 19:13:10 2010 +0200
    38.3 @@ -38,10 +38,10 @@
    38.4                 
    38.5  local
    38.6  
    38.7 -val conj1_False = thm "conj1_False";
    38.8 -val conj2_False = thm "conj2_False";
    38.9 -val conj_True = thm "conj_True";
   38.10 -val conj_cong = thm "conj_cong";
   38.11 +val conj1_False = @{thm conj1_False};
   38.12 +val conj2_False = @{thm conj2_False};
   38.13 +val conj_True = @{thm conj_True};
   38.14 +val conj_cong = @{thm conj_cong};
   38.15  
   38.16  fun isFalse (Const (@{const_name False},_)) = true
   38.17    | isFalse _ = false;
   38.18 @@ -255,7 +255,7 @@
   38.19  
   38.20  
   38.21  local
   38.22 -val swap_ex_eq = thm "StateFun.swap_ex_eq";
   38.23 +val swap_ex_eq = @{thm StateFun.swap_ex_eq};
   38.24  fun is_selector thy T sel =
   38.25       let 
   38.26         val (flds,more) = Record.get_recT_fields thy T 
    39.1 --- a/src/HOL/TLA/Memory/Memory.thy	Mon Sep 06 19:11:01 2010 +0200
    39.2 +++ b/src/HOL/TLA/Memory/Memory.thy	Mon Sep 06 19:13:10 2010 +0200
    39.3 @@ -181,10 +181,10 @@
    39.4        |- Calling ch p & (rs!p ~= #NotAResult)
    39.5           --> Enabled (<MemReturn ch rs p>_(rtrner ch ! p, rs!p))"
    39.6    apply (tactic
    39.7 -    {* action_simp_tac @{simpset} [thm "MemReturn_change" RSN (2, thm "enabled_mono") ] [] 1 *})
    39.8 +    {* action_simp_tac @{simpset} [@{thm MemReturn_change} RSN (2, @{thm enabled_mono}) ] [] 1 *})
    39.9    apply (tactic
   39.10 -    {* action_simp_tac (@{simpset} addsimps [thm "MemReturn_def", thm "Return_def",
   39.11 -      thm "rtrner_def"]) [exI] [thm "base_enabled", thm "Pair_inject"] 1 *})
   39.12 +    {* action_simp_tac (@{simpset} addsimps [@{thm MemReturn_def}, @{thm Return_def},
   39.13 +      @{thm rtrner_def}]) [exI] [@{thm base_enabled}, @{thm Pair_inject}] 1 *})
   39.14    done
   39.15  
   39.16  lemma ReadInner_enabled: "!!p. basevars (rtrner ch ! p, rs!p) ==>
   39.17 @@ -227,13 +227,13 @@
   39.18           --> Enabled (<RNext ch mm rs p>_(rtrner ch ! p, rs!p))"
   39.19    apply (auto simp: enabled_disj [try_rewrite] intro!: RWRNext_enabled [temp_use])
   39.20    apply (case_tac "arg (ch w p)")
   39.21 -   apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "Read_def",
   39.22 -     temp_rewrite (thm "enabled_ex")]) [thm "ReadInner_enabled", exI] [] 1 *})
   39.23 +   apply (tactic {* action_simp_tac (@{simpset} addsimps [@{thm Read_def},
   39.24 +     temp_rewrite @{thm enabled_ex}]) [@{thm ReadInner_enabled}, exI] [] 1 *})
   39.25     apply (force dest: base_pair [temp_use])
   39.26    apply (erule contrapos_np)
   39.27 -  apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "Write_def",
   39.28 -    temp_rewrite (thm "enabled_ex")])
   39.29 -    [thm "WriteInner_enabled", exI] [] 1 *})
   39.30 +  apply (tactic {* action_simp_tac (@{simpset} addsimps [@{thm Write_def},
   39.31 +    temp_rewrite @{thm enabled_ex}])
   39.32 +    [@{thm WriteInner_enabled}, exI] [] 1 *})
   39.33    done
   39.34  
   39.35  end
    40.1 --- a/src/HOL/TLA/Memory/MemoryImplementation.thy	Mon Sep 06 19:11:01 2010 +0200
    40.2 +++ b/src/HOL/TLA/Memory/MemoryImplementation.thy	Mon Sep 06 19:13:10 2010 +0200
    40.3 @@ -255,10 +255,10 @@
    40.4    apply (rule historyI)
    40.5        apply assumption+
    40.6    apply (rule MI_base)
    40.7 -  apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "HInit_def"]) [] [] 1 *})
    40.8 +  apply (tactic {* action_simp_tac (@{simpset} addsimps [@{thm HInit_def}]) [] [] 1 *})
    40.9     apply (erule fun_cong)
   40.10 -  apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "HNext_def"])
   40.11 -    [thm "busy_squareI"] [] 1 *})
   40.12 +  apply (tactic {* action_simp_tac (@{simpset} addsimps [@{thm HNext_def}])
   40.13 +    [@{thm busy_squareI}] [] 1 *})
   40.14    apply (erule fun_cong)
   40.15    done
   40.16  
   40.17 @@ -346,22 +346,22 @@
   40.18      caller_def rtrner_def MVNROKBA_def S_def S1_def S2_def Calling_def)
   40.19  
   40.20  lemma S1ClerkUnch: "|- [MClkNext memCh crCh cst p]_(c p) & $(S1 rmhist p) --> unchanged (c p)"
   40.21 -  by (tactic {* auto_tac (MI_fast_css addSDs2 [temp_use (thm "MClkidle")]
   40.22 -    addsimps2 [thm "S_def", thm "S1_def"]) *})
   40.23 +  by (tactic {* auto_tac (MI_fast_css addSDs2 [temp_use @{thm MClkidle}]
   40.24 +    addsimps2 [@{thm S_def}, @{thm S1_def}]) *})
   40.25  
   40.26  lemma S1RPCUnch: "|- [RPCNext crCh rmCh rst p]_(r p) & $(S1 rmhist p) --> unchanged (r p)"
   40.27 -  by (tactic {* auto_tac (MI_fast_css addSDs2 [temp_use (thm "RPCidle")]
   40.28 -    addsimps2 [thm "S_def", thm "S1_def"]) *})
   40.29 +  by (tactic {* auto_tac (MI_fast_css addSDs2 [temp_use @{thm RPCidle}]
   40.30 +    addsimps2 [@{thm S_def}, @{thm S1_def}]) *})
   40.31  
   40.32  lemma S1MemUnch: "|- [RNext rmCh mm ires p]_(m p) & $(S1 rmhist p) --> unchanged (m p)"
   40.33 -  by (tactic {* auto_tac (MI_fast_css addSDs2 [temp_use (thm "Memoryidle")]
   40.34 -    addsimps2 [thm "S_def", thm "S1_def"]) *})
   40.35 +  by (tactic {* auto_tac (MI_fast_css addSDs2 [temp_use @{thm Memoryidle}]
   40.36 +    addsimps2 [@{thm S_def}, @{thm S1_def}]) *})
   40.37  
   40.38  lemma S1Hist: "|- [HNext rmhist p]_(c p,r p,m p,rmhist!p) & $(S1 rmhist p)
   40.39           --> unchanged (rmhist!p)"
   40.40 -  by (tactic {* action_simp_tac (@{simpset} addsimps [thm "HNext_def", thm "S_def",
   40.41 -    thm "S1_def", thm "MemReturn_def", thm "RPCFail_def", thm "MClkReply_def",
   40.42 -    thm "Return_def"]) [] [temp_use (thm "squareE")] 1 *})
   40.43 +  by (tactic {* action_simp_tac (@{simpset} addsimps [@{thm HNext_def}, @{thm S_def},
   40.44 +    @{thm S1_def}, @{thm MemReturn_def}, @{thm RPCFail_def}, @{thm MClkReply_def},
   40.45 +    @{thm Return_def}]) [] [temp_use @{thm squareE}] 1 *})
   40.46  
   40.47  
   40.48  (* ------------------------------ State S2 ---------------------------------------- *)
   40.49 @@ -375,9 +375,9 @@
   40.50  lemma S2Forward: "|- $(S2 rmhist p) & MClkFwd memCh crCh cst p
   40.51           & unchanged (e p, r p, m p, rmhist!p)
   40.52           --> (S3 rmhist p)$"
   40.53 -  by (tactic {* action_simp_tac (@{simpset} addsimps [thm "MClkFwd_def",
   40.54 -    thm "Call_def", thm "e_def", thm "r_def", thm "m_def", thm "caller_def",
   40.55 -    thm "rtrner_def", thm "S_def", thm "S2_def", thm "S3_def", thm "Calling_def"]) [] [] 1 *})
   40.56 +  by (tactic {* action_simp_tac (@{simpset} addsimps [@{thm MClkFwd_def},
   40.57 +    @{thm Call_def}, @{thm e_def}, @{thm r_def}, @{thm m_def}, @{thm caller_def},
   40.58 +    @{thm rtrner_def}, @{thm S_def}, @{thm S2_def}, @{thm S3_def}, @{thm Calling_def}]) [] [] 1 *})
   40.59  
   40.60  lemma S2RPCUnch: "|- [RPCNext crCh rmCh rst p]_(r p) & $(S2 rmhist p) --> unchanged (r p)"
   40.61    by (auto simp: S_def S2_def dest!: RPCidle [temp_use])
   40.62 @@ -387,8 +387,8 @@
   40.63  
   40.64  lemma S2Hist: "|- [HNext rmhist p]_(c p,r p,m p,rmhist!p) & $(S2 rmhist p)
   40.65           --> unchanged (rmhist!p)"
   40.66 -  by (tactic {* auto_tac (MI_fast_css addsimps2 [thm "HNext_def", thm "MemReturn_def",
   40.67 -    thm "RPCFail_def", thm "MClkReply_def", thm "Return_def", thm "S_def", thm "S2_def"]) *})
   40.68 +  by (tactic {* auto_tac (MI_fast_css addsimps2 [@{thm HNext_def}, @{thm MemReturn_def},
   40.69 +    @{thm RPCFail_def}, @{thm MClkReply_def}, @{thm Return_def}, @{thm S_def}, @{thm S2_def}]) *})
   40.70  
   40.71  (* ------------------------------ State S3 ---------------------------------------- *)
   40.72  
   40.73 @@ -411,19 +411,19 @@
   40.74  lemma S3Forward: "|- RPCFwd crCh rmCh rst p & HNext rmhist p & $(S3 rmhist p)
   40.75           & unchanged (e p, c p, m p)
   40.76           --> (S4 rmhist p)$ & unchanged (rmhist!p)"
   40.77 -  by (tactic {* action_simp_tac (@{simpset} addsimps [thm "RPCFwd_def",
   40.78 -    thm "HNext_def", thm "MemReturn_def", thm "RPCFail_def",
   40.79 -    thm "MClkReply_def", thm "Return_def", thm "Call_def", thm "e_def",
   40.80 -    thm "c_def", thm "m_def", thm "caller_def", thm "rtrner_def", thm "S_def",
   40.81 -    thm "S3_def", thm "S4_def", thm "Calling_def"]) [] [] 1 *})
   40.82 +  by (tactic {* action_simp_tac (@{simpset} addsimps [@{thm RPCFwd_def},
   40.83 +    @{thm HNext_def}, @{thm MemReturn_def}, @{thm RPCFail_def},
   40.84 +    @{thm MClkReply_def}, @{thm Return_def}, @{thm Call_def}, @{thm e_def},
   40.85 +    @{thm c_def}, @{thm m_def}, @{thm caller_def}, @{thm rtrner_def}, @{thm S_def},
   40.86 +    @{thm S3_def}, @{thm S4_def}, @{thm Calling_def}]) [] [] 1 *})
   40.87  
   40.88  lemma S3Fail: "|- RPCFail crCh rmCh rst p & $(S3 rmhist p) & HNext rmhist p
   40.89           & unchanged (e p, c p, m p)
   40.90           --> (S6 rmhist p)$"
   40.91 -  by (tactic {* action_simp_tac (@{simpset} addsimps [thm "HNext_def",
   40.92 -    thm "RPCFail_def", thm "Return_def", thm "e_def", thm "c_def",
   40.93 -    thm "m_def", thm "caller_def", thm "rtrner_def", thm "MVOKBARF_def",
   40.94 -    thm "S_def", thm "S3_def", thm "S6_def", thm "Calling_def"]) [] [] 1 *})
   40.95 +  by (tactic {* action_simp_tac (@{simpset} addsimps [@{thm HNext_def},
   40.96 +    @{thm RPCFail_def}, @{thm Return_def}, @{thm e_def}, @{thm c_def},
   40.97 +    @{thm m_def}, @{thm caller_def}, @{thm rtrner_def}, @{thm MVOKBARF_def},
   40.98 +    @{thm S_def}, @{thm S3_def}, @{thm S6_def}, @{thm Calling_def}]) [] [] 1 *})
   40.99  
  40.100  lemma S3MemUnch: "|- [RNext rmCh mm ires p]_(m p) & $(S3 rmhist p) --> unchanged (m p)"
  40.101    by (auto simp: S_def S3_def dest!: Memoryidle [temp_use])
  40.102 @@ -441,18 +441,18 @@
  40.103    by (auto simp: S_def S4_def dest!: MClkbusy [temp_use])
  40.104  
  40.105  lemma S4RPCUnch: "|- [RPCNext crCh rmCh rst p]_(r p) & $(S4 rmhist p) --> unchanged (r p)"
  40.106 -  by (tactic {* auto_tac (MI_fast_css addsimps2 [thm "S_def", thm "S4_def"]
  40.107 -    addSDs2 [temp_use (thm "RPCbusy")]) *})
  40.108 +  by (tactic {* auto_tac (MI_fast_css addsimps2 [@{thm S_def}, @{thm S4_def}]
  40.109 +    addSDs2 [temp_use @{thm RPCbusy}]) *})
  40.110  
  40.111  lemma S4ReadInner: "|- ReadInner rmCh mm ires p l & $(S4 rmhist p) & unchanged (e p, c p, r p)
  40.112           & HNext rmhist p & $(MemInv mm l)
  40.113           --> (S4 rmhist p)$ & unchanged (rmhist!p)"
  40.114 -  by (tactic {* action_simp_tac (@{simpset} addsimps [thm "ReadInner_def",
  40.115 -    thm "GoodRead_def", thm "BadRead_def", thm "HNext_def", thm "MemReturn_def",
  40.116 -    thm "RPCFail_def", thm "MClkReply_def", thm "Return_def", thm "e_def",
  40.117 -    thm "c_def", thm "r_def", thm "rtrner_def", thm "caller_def",
  40.118 -    thm "MVNROKBA_def", thm "S_def", thm "S4_def", thm "RdRequest_def",
  40.119 -    thm "Calling_def", thm "MemInv_def"]) [] [] 1 *})
  40.120 +  by (tactic {* action_simp_tac (@{simpset} addsimps [@{thm ReadInner_def},
  40.121 +    @{thm GoodRead_def}, @{thm BadRead_def}, @{thm HNext_def}, @{thm MemReturn_def},
  40.122 +    @{thm RPCFail_def}, @{thm MClkReply_def}, @{thm Return_def}, @{thm e_def},
  40.123 +    @{thm c_def}, @{thm r_def}, @{thm rtrner_def}, @{thm caller_def},
  40.124 +    @{thm MVNROKBA_def}, @{thm S_def}, @{thm S4_def}, @{thm RdRequest_def},
  40.125 +    @{thm Calling_def}, @{thm MemInv_def}]) [] [] 1 *})
  40.126  
  40.127  lemma S4Read: "|- Read rmCh mm ires p & $(S4 rmhist p) & unchanged (e p, c p, r p)
  40.128           & HNext rmhist p & (!l. $MemInv mm l)
  40.129 @@ -461,11 +461,11 @@
  40.130  
  40.131  lemma S4WriteInner: "|- WriteInner rmCh mm ires p l v & $(S4 rmhist p) & unchanged (e p, c p, r p)           & HNext rmhist p
  40.132           --> (S4 rmhist p)$ & unchanged (rmhist!p)"
  40.133 -  by (tactic {* action_simp_tac (@{simpset} addsimps [thm "WriteInner_def",
  40.134 -    thm "GoodWrite_def", thm "BadWrite_def", thm "HNext_def", thm "MemReturn_def",
  40.135 -    thm "RPCFail_def", thm "MClkReply_def", thm "Return_def", thm "e_def",
  40.136 -    thm "c_def", thm "r_def", thm "rtrner_def", thm "caller_def", thm "MVNROKBA_def",
  40.137 -    thm "S_def", thm "S4_def", thm "WrRequest_def", thm "Calling_def"]) [] [] 1 *})
  40.138 +  by (tactic {* action_simp_tac (@{simpset} addsimps [@{thm WriteInner_def},
  40.139 +    @{thm GoodWrite_def}, @{thm BadWrite_def}, @{thm HNext_def}, @{thm MemReturn_def},
  40.140 +    @{thm RPCFail_def}, @{thm MClkReply_def}, @{thm Return_def}, @{thm e_def},
  40.141 +    @{thm c_def}, @{thm r_def}, @{thm rtrner_def}, @{thm caller_def}, @{thm MVNROKBA_def},
  40.142 +    @{thm S_def}, @{thm S4_def}, @{thm WrRequest_def}, @{thm Calling_def}]) [] [] 1 *})
  40.143  
  40.144  lemma S4Write: "|- Write rmCh mm ires p l & $(S4 rmhist p) & unchanged (e p, c p, r p)
  40.145           & (HNext rmhist p)
  40.146 @@ -500,26 +500,26 @@
  40.147  
  40.148  lemma S5Reply: "|- RPCReply crCh rmCh rst p & $(S5 rmhist p) & unchanged (e p, c p, m p,rmhist!p)
  40.149         --> (S6 rmhist p)$"
  40.150 -  by (tactic {* action_simp_tac (@{simpset} addsimps [thm "RPCReply_def",
  40.151 -    thm "Return_def", thm "e_def", thm "c_def", thm "m_def", thm "MVOKBA_def",
  40.152 -    thm "MVOKBARF_def", thm "caller_def", thm "rtrner_def", thm "S_def",
  40.153 -    thm "S5_def", thm "S6_def", thm "Calling_def"]) [] [] 1 *})
  40.154 +  by (tactic {* action_simp_tac (@{simpset} addsimps [@{thm RPCReply_def},
  40.155 +    @{thm Return_def}, @{thm e_def}, @{thm c_def}, @{thm m_def}, @{thm MVOKBA_def},
  40.156 +    @{thm MVOKBARF_def}, @{thm caller_def}, @{thm rtrner_def}, @{thm S_def},
  40.157 +    @{thm S5_def}, @{thm S6_def}, @{thm Calling_def}]) [] [] 1 *})
  40.158  
  40.159  lemma S5Fail: "|- RPCFail crCh rmCh rst p & $(S5 rmhist p) & unchanged (e p, c p, m p,rmhist!p)
  40.160           --> (S6 rmhist p)$"
  40.161 -  by (tactic {* action_simp_tac (@{simpset} addsimps [thm "RPCFail_def",
  40.162 -    thm "Return_def", thm "e_def", thm "c_def", thm "m_def",
  40.163 -    thm "MVOKBARF_def", thm "caller_def", thm "rtrner_def",
  40.164 -    thm "S_def", thm "S5_def", thm "S6_def", thm "Calling_def"]) [] [] 1 *})
  40.165 +  by (tactic {* action_simp_tac (@{simpset} addsimps [@{thm RPCFail_def},
  40.166 +    @{thm Return_def}, @{thm e_def}, @{thm c_def}, @{thm m_def},
  40.167 +    @{thm MVOKBARF_def}, @{thm caller_def}, @{thm rtrner_def},
  40.168 +    @{thm S_def}, @{thm S5_def}, @{thm S6_def}, @{thm Calling_def}]) [] [] 1 *})
  40.169  
  40.170  lemma S5MemUnch: "|- [RNext rmCh mm ires p]_(m p) & $(S5 rmhist p) --> unchanged (m p)"
  40.171    by (auto simp: S_def S5_def dest!: Memoryidle [temp_use])
  40.172  
  40.173  lemma S5Hist: "|- [HNext rmhist p]_(c p, r p, m p, rmhist!p) & $(S5 rmhist p)
  40.174           --> (rmhist!p)$ = $(rmhist!p)"
  40.175 -  by (tactic {* auto_tac (MI_fast_css addsimps2 [thm "HNext_def",
  40.176 -    thm "MemReturn_def", thm "RPCFail_def", thm "MClkReply_def", thm "Return_def",
  40.177 -    thm "S_def", thm "S5_def"]) *})
  40.178 +  by (tactic {* auto_tac (MI_fast_css addsimps2 [@{thm HNext_def},
  40.179 +    @{thm MemReturn_def}, @{thm RPCFail_def}, @{thm MClkReply_def}, @{thm Return_def},
  40.180 +    @{thm S_def}, @{thm S5_def}]) *})
  40.181  
  40.182  (* ------------------------------ State S6 ---------------------------------------- *)
  40.183  
  40.184 @@ -533,18 +533,18 @@
  40.185  lemma S6Retry: "|- MClkRetry memCh crCh cst p & HNext rmhist p & $S6 rmhist p
  40.186           & unchanged (e p,r p,m p)
  40.187           --> (S3 rmhist p)$ & unchanged (rmhist!p)"
  40.188 -  by (tactic {* action_simp_tac (@{simpset} addsimps [thm "HNext_def",
  40.189 -    thm "MClkReply_def", thm "MClkRetry_def", thm "Call_def", thm "Return_def",
  40.190 -    thm "e_def", thm "r_def", thm "m_def", thm "caller_def", thm "rtrner_def",
  40.191 -    thm "S_def", thm "S6_def", thm "S3_def", thm "Calling_def"]) [] [] 1 *})
  40.192 +  by (tactic {* action_simp_tac (@{simpset} addsimps [@{thm HNext_def},
  40.193 +    @{thm MClkReply_def}, @{thm MClkRetry_def}, @{thm Call_def}, @{thm Return_def},
  40.194 +    @{thm e_def}, @{thm r_def}, @{thm m_def}, @{thm caller_def}, @{thm rtrner_def},
  40.195 +    @{thm S_def}, @{thm S6_def}, @{thm S3_def}, @{thm Calling_def}]) [] [] 1 *})
  40.196  
  40.197  lemma S6Reply: "|- MClkReply memCh crCh cst p & HNext rmhist p & $S6 rmhist p
  40.198           & unchanged (e p,r p,m p)
  40.199           --> (S1 rmhist p)$"
  40.200 -  by (tactic {* action_simp_tac (@{simpset} addsimps [thm "HNext_def",
  40.201 -    thm "MemReturn_def", thm "RPCFail_def", thm "Return_def", thm "MClkReply_def",
  40.202 -    thm "e_def", thm "r_def", thm "m_def", thm "caller_def", thm "rtrner_def",
  40.203 -    thm "S_def", thm "S6_def", thm "S1_def", thm "Calling_def"]) [] [] 1 *})
  40.204 +  by (tactic {* action_simp_tac (@{simpset} addsimps [@{thm HNext_def},
  40.205 +    @{thm MemReturn_def}, @{thm RPCFail_def}, @{thm Return_def}, @{thm MClkReply_def},
  40.206 +    @{thm e_def}, @{thm r_def}, @{thm m_def}, @{thm caller_def}, @{thm rtrner_def},
  40.207 +    @{thm S_def}, @{thm S6_def}, @{thm S1_def}, @{thm Calling_def}]) [] [] 1 *})
  40.208  
  40.209  lemma S6RPCUnch: "|- [RPCNext crCh rmCh rst p]_(r p) & $S6 rmhist p --> unchanged (r p)"
  40.210    by (auto simp: S_def S6_def dest!: RPCidle [temp_use])
  40.211 @@ -563,9 +563,9 @@
  40.212  (* The implementation's initial condition implies the state predicate S1 *)
  40.213  
  40.214  lemma Step1_1: "|- ImpInit p & HInit rmhist p --> S1 rmhist p"
  40.215 -  by (tactic {* auto_tac (MI_fast_css addsimps2 [thm "MVNROKBA_def",
  40.216 -    thm "MClkInit_def", thm "RPCInit_def", thm "PInit_def", thm "HInit_def",
  40.217 -    thm "ImpInit_def", thm "S_def", thm "S1_def"]) *})
  40.218 +  by (tactic {* auto_tac (MI_fast_css addsimps2 [@{thm MVNROKBA_def},
  40.219 +    @{thm MClkInit_def}, @{thm RPCInit_def}, @{thm PInit_def}, @{thm HInit_def},
  40.220 +    @{thm ImpInit_def}, @{thm S_def}, @{thm S1_def}]) *})
  40.221  
  40.222  (* ========== Step 1.2 ================================================== *)
  40.223  (* Figure 16 is a predicate-action diagram for the implementation. *)
  40.224 @@ -573,29 +573,29 @@
  40.225  lemma Step1_2_1: "|- [HNext rmhist p]_(c p,r p,m p, rmhist!p) & ImpNext p
  40.226           & ~unchanged (e p, c p, r p, m p, rmhist!p)  & $S1 rmhist p
  40.227           --> (S2 rmhist p)$ & ENext p & unchanged (c p, r p, m p)"
  40.228 -  apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "ImpNext_def"]) []
  40.229 -      (map temp_elim [thm "S1ClerkUnch", thm "S1RPCUnch", thm "S1MemUnch", thm "S1Hist"]) 1 *})
  40.230 -   apply (tactic {* auto_tac (MI_fast_css addSIs2 [temp_use (thm "S1Env")]) *})
  40.231 +  apply (tactic {* action_simp_tac (@{simpset} addsimps [@{thm ImpNext_def}]) []
  40.232 +      (map temp_elim [@{thm S1ClerkUnch}, @{thm S1RPCUnch}, @{thm S1MemUnch}, @{thm S1Hist}]) 1 *})
  40.233 +   apply (tactic {* auto_tac (MI_fast_css addSIs2 [temp_use @{thm S1Env}]) *})
  40.234    done
  40.235  
  40.236  lemma Step1_2_2: "|- [HNext rmhist p]_(c p,r p,m p, rmhist!p) & ImpNext p
  40.237           & ~unchanged (e p, c p, r p, m p, rmhist!p) & $S2 rmhist p
  40.238           --> (S3 rmhist p)$ & MClkFwd memCh crCh cst p
  40.239               & unchanged (e p, r p, m p, rmhist!p)"
  40.240 -  apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "ImpNext_def"]) []
  40.241 -    (map temp_elim [thm "S2EnvUnch", thm "S2RPCUnch", thm "S2MemUnch", thm "S2Hist"]) 1 *})
  40.242 -   apply (tactic {* auto_tac (MI_fast_css addSIs2 [temp_use (thm "S2Clerk"),
  40.243 -     temp_use (thm "S2Forward")]) *})
  40.244 +  apply (tactic {* action_simp_tac (@{simpset} addsimps [@{thm ImpNext_def}]) []
  40.245 +    (map temp_elim [@{thm S2EnvUnch}, @{thm S2RPCUnch}, @{thm S2MemUnch}, @{thm S2Hist}]) 1 *})
  40.246 +   apply (tactic {* auto_tac (MI_fast_css addSIs2 [temp_use @{thm S2Clerk},
  40.247 +     temp_use @{thm S2Forward}]) *})
  40.248    done
  40.249  
  40.250  lemma Step1_2_3: "|- [HNext rmhist p]_(c p,r p,m p, rmhist!p) & ImpNext p
  40.251           & ~unchanged (e p, c p, r p, m p, rmhist!p) & $S3 rmhist p
  40.252           --> ((S4 rmhist p)$ & RPCFwd crCh rmCh rst p & unchanged (e p, c p, m p, rmhist!p))
  40.253               | ((S6 rmhist p)$ & RPCFail crCh rmCh rst p & unchanged (e p, c p, m p))"
  40.254 -  apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "ImpNext_def"]) []
  40.255 -    (map temp_elim [thm "S3EnvUnch", thm "S3ClerkUnch", thm "S3MemUnch"]) 1 *})
  40.256 +  apply (tactic {* action_simp_tac (@{simpset} addsimps [@{thm ImpNext_def}]) []
  40.257 +    (map temp_elim [@{thm S3EnvUnch}, @{thm S3ClerkUnch}, @{thm S3MemUnch}]) 1 *})
  40.258    apply (tactic {* action_simp_tac @{simpset} []
  40.259 -    (thm "squareE" :: map temp_elim [thm "S3RPC", thm "S3Forward", thm "S3Fail"]) 1 *})
  40.260 +    (@{thm squareE} :: map temp_elim [@{thm S3RPC}, @{thm S3Forward}, @{thm S3Fail}]) 1 *})
  40.261     apply (auto dest!: S3Hist [temp_use])
  40.262    done
  40.263  
  40.264 @@ -605,10 +605,10 @@
  40.265           --> ((S4 rmhist p)$ & Read rmCh mm ires p & unchanged (e p, c p, r p, rmhist!p))
  40.266               | ((S4 rmhist p)$ & (? l. Write rmCh mm ires p l) & unchanged (e p, c p, r p, rmhist!p))
  40.267               | ((S5 rmhist p)$ & MemReturn rmCh ires p & unchanged (e p, c p, r p))"
  40.268 -  apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "ImpNext_def"]) []
  40.269 -    (map temp_elim [thm "S4EnvUnch", thm "S4ClerkUnch", thm "S4RPCUnch"]) 1 *})
  40.270 -  apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "RNext_def"]) []
  40.271 -    (thm "squareE" :: map temp_elim [thm "S4Read", thm "S4Write", thm "S4Return"]) 1 *})
  40.272 +  apply (tactic {* action_simp_tac (@{simpset} addsimps [@{thm ImpNext_def}]) []
  40.273 +    (map temp_elim [@{thm S4EnvUnch}, @{thm S4ClerkUnch}, @{thm S4RPCUnch}]) 1 *})
  40.274 +  apply (tactic {* action_simp_tac (@{simpset} addsimps [@{thm RNext_def}]) []
  40.275 +    (@{thm squareE} :: map temp_elim [@{thm S4Read}, @{thm S4Write}, @{thm S4Return}]) 1 *})
  40.276    apply (auto dest!: S4Hist [temp_use])
  40.277    done
  40.278  
  40.279 @@ -616,21 +616,21 @@
  40.280                & ~unchanged (e p, c p, r p, m p, rmhist!p) & $S5 rmhist p
  40.281           --> ((S6 rmhist p)$ & RPCReply crCh rmCh rst p & unchanged (e p, c p, m p))
  40.282               | ((S6 rmhist p)$ & RPCFail crCh rmCh rst p & unchanged (e p, c p, m p))"
  40.283 -  apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "ImpNext_def"]) []
  40.284 -    (map temp_elim [thm "S5EnvUnch", thm "S5ClerkUnch", thm "S5MemUnch", thm "S5Hist"]) 1 *})
  40.285 -  apply (tactic {* action_simp_tac @{simpset} [] [thm "squareE", temp_elim (thm "S5RPC")] 1 *})
  40.286 +  apply (tactic {* action_simp_tac (@{simpset} addsimps [@{thm ImpNext_def}]) []
  40.287 +    (map temp_elim [@{thm S5EnvUnch}, @{thm S5ClerkUnch}, @{thm S5MemUnch}, @{thm S5Hist}]) 1 *})
  40.288 +  apply (tactic {* action_simp_tac @{simpset} [] [@{thm squareE}, temp_elim @{thm S5RPC}] 1 *})
  40.289     apply (tactic {* auto_tac (MI_fast_css addSDs2
  40.290 -     [temp_use (thm "S5Reply"), temp_use (thm "S5Fail")]) *})
  40.291 +     [temp_use @{thm S5Reply}, temp_use @{thm S5Fail}]) *})
  40.292    done
  40.293  
  40.294  lemma Step1_2_6: "|- [HNext rmhist p]_(c p,r p,m p, rmhist!p) & ImpNext p
  40.295                & ~unchanged (e p, c p, r p, m p, rmhist!p) & $S6 rmhist p
  40.296           --> ((S1 rmhist p)$ & MClkReply memCh crCh cst p & unchanged (e p, r p, m p))
  40.297               | ((S3 rmhist p)$ & MClkRetry memCh crCh cst p & unchanged (e p,r p,m p,rmhist!p))"
  40.298 -  apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "ImpNext_def"]) []
  40.299 -    (map temp_elim [thm "S6EnvUnch", thm "S6RPCUnch", thm "S6MemUnch"]) 1 *})
  40.300 +  apply (tactic {* action_simp_tac (@{simpset} addsimps [@{thm ImpNext_def}]) []
  40.301 +    (map temp_elim [@{thm S6EnvUnch}, @{thm S6RPCUnch}, @{thm S6MemUnch}]) 1 *})
  40.302    apply (tactic {* action_simp_tac @{simpset} []
  40.303 -    (thm "squareE" :: map temp_elim [thm "S6Clerk", thm "S6Retry", thm "S6Reply"]) 1 *})
  40.304 +    (@{thm squareE} :: map temp_elim [@{thm S6Clerk}, @{thm S6Retry}, @{thm S6Reply}]) 1 *})
  40.305       apply (auto dest: S6Hist [temp_use])
  40.306    done
  40.307  
  40.308 @@ -641,8 +641,8 @@
  40.309  section "Initialization (Step 1.3)"
  40.310  
  40.311  lemma Step1_3: "|- S1 rmhist p --> PInit (resbar rmhist) p"
  40.312 -  by (tactic {* action_simp_tac (@{simpset} addsimps [thm "resbar_def",
  40.313 -    thm "PInit_def", thm "S_def", thm "S1_def"]) [] [] 1 *})
  40.314 +  by (tactic {* action_simp_tac (@{simpset} addsimps [@{thm resbar_def},
  40.315 +    @{thm PInit_def}, @{thm S_def}, @{thm S1_def}]) [] [] 1 *})
  40.316  
  40.317  (* ----------------------------------------------------------------------
  40.318     Step 1.4: Implementation's next-state relation simulates specification's
  40.319 @@ -653,23 +653,23 @@
  40.320  
  40.321  lemma Step1_4_1: "|- ENext p & $S1 rmhist p & (S2 rmhist p)$ & unchanged (c p, r p, m p)
  40.322           --> unchanged (rtrner memCh!p, resbar rmhist!p)"
  40.323 -  by (tactic {* auto_tac (MI_fast_css addsimps2 [thm "c_def", thm "r_def",
  40.324 -    thm "m_def", thm "resbar_def"]) *})
  40.325 +  by (tactic {* auto_tac (MI_fast_css addsimps2 [@{thm c_def}, @{thm r_def},
  40.326 +    @{thm m_def}, @{thm resbar_def}]) *})
  40.327  
  40.328  lemma Step1_4_2: "|- MClkFwd memCh crCh cst p & $S2 rmhist p & (S3 rmhist p)$
  40.329           & unchanged (e p, r p, m p, rmhist!p)
  40.330           --> unchanged (rtrner memCh!p, resbar rmhist!p)"
  40.331    by (tactic {* action_simp_tac
  40.332 -    (@{simpset} addsimps [thm "MClkFwd_def", thm "e_def", thm "r_def", thm "m_def",
  40.333 -    thm "resbar_def", thm "S_def", thm "S2_def", thm "S3_def"]) [] [] 1 *})
  40.334 +    (@{simpset} addsimps [@{thm MClkFwd_def}, @{thm e_def}, @{thm r_def}, @{thm m_def},
  40.335 +    @{thm resbar_def}, @{thm S_def}, @{thm S2_def}, @{thm S3_def}]) [] [] 1 *})
  40.336  
  40.337  lemma Step1_4_3a: "|- RPCFwd crCh rmCh rst p & $S3 rmhist p & (S4 rmhist p)$
  40.338           & unchanged (e p, c p, m p, rmhist!p)
  40.339           --> unchanged (rtrner memCh!p, resbar rmhist!p)"
  40.340    apply clarsimp
  40.341    apply (drule S3_excl [temp_use] S4_excl [temp_use])+
  40.342 -  apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "e_def",
  40.343 -    thm "c_def", thm "m_def", thm "resbar_def", thm "S_def", thm "S3_def"]) [] [] 1 *})
  40.344 +  apply (tactic {* action_simp_tac (@{simpset} addsimps [@{thm e_def},
  40.345 +    @{thm c_def}, @{thm m_def}, @{thm resbar_def}, @{thm S_def}, @{thm S3_def}]) [] [] 1 *})
  40.346    done
  40.347  
  40.348  lemma Step1_4_3b: "|- RPCFail crCh rmCh rst p & $S3 rmhist p & (S6 rmhist p)$
  40.349 @@ -687,13 +687,13 @@
  40.350           --> ReadInner memCh mm (resbar rmhist) p l"
  40.351    apply clarsimp
  40.352    apply (drule S4_excl [temp_use])+
  40.353 -  apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "ReadInner_def",
  40.354 -    thm "GoodRead_def", thm "BadRead_def", thm "e_def", thm "c_def", thm "m_def"]) [] [] 1 *})
  40.355 +  apply (tactic {* action_simp_tac (@{simpset} addsimps [@{thm ReadInner_def},
  40.356 +    @{thm GoodRead_def}, @{thm BadRead_def}, @{thm e_def}, @{thm c_def}, @{thm m_def}]) [] [] 1 *})
  40.357       apply (auto simp: resbar_def)
  40.358         apply (tactic {* ALLGOALS (action_simp_tac
  40.359 -                (@{simpset} addsimps [thm "RPCRelayArg_def", thm "MClkRelayArg_def",
  40.360 -                  thm "S_def", thm "S4_def", thm "RdRequest_def", thm "MemInv_def"])
  40.361 -                [] [thm "impE", thm "MemValNotAResultE"]) *})
  40.362 +                (@{simpset} addsimps [@{thm RPCRelayArg_def}, @{thm MClkRelayArg_def},
  40.363 +                  @{thm S_def}, @{thm S4_def}, @{thm RdRequest_def}, @{thm MemInv_def}])
  40.364 +                [] [@{thm impE}, @{thm MemValNotAResultE}]) *})
  40.365    done
  40.366  
  40.367  lemma Step1_4_4a: "|- Read rmCh mm ires p & $S4 rmhist p & (S4 rmhist p)$
  40.368 @@ -707,12 +707,12 @@
  40.369    apply clarsimp
  40.370    apply (drule S4_excl [temp_use])+
  40.371    apply (tactic {* action_simp_tac (@{simpset} addsimps
  40.372 -    [thm "WriteInner_def", thm "GoodWrite_def", thm "BadWrite_def", thm "e_def",
  40.373 -    thm "c_def", thm "m_def"]) [] [] 1 *})
  40.374 +    [@{thm WriteInner_def}, @{thm GoodWrite_def}, @{thm BadWrite_def}, @{thm e_def},
  40.375 +    @{thm c_def}, @{thm m_def}]) [] [] 1 *})
  40.376       apply (auto simp: resbar_def)
  40.377      apply (tactic {* ALLGOALS (action_simp_tac (@{simpset} addsimps
  40.378 -      [thm "RPCRelayArg_def", thm "MClkRelayArg_def", thm "S_def",
  40.379 -      thm "S4_def", thm "WrRequest_def"]) [] []) *})
  40.380 +      [@{thm RPCRelayArg_def}, @{thm MClkRelayArg_def}, @{thm S_def},
  40.381 +      @{thm S4_def}, @{thm WrRequest_def}]) [] []) *})
  40.382    done
  40.383  
  40.384  lemma Step1_4_4b: "|- Write rmCh mm ires p l & $S4 rmhist p & (S4 rmhist p)$
  40.385 @@ -723,10 +723,10 @@
  40.386  lemma Step1_4_4c: "|- MemReturn rmCh ires p & $S4 rmhist p & (S5 rmhist p)$
  40.387           & unchanged (e p, c p, r p)
  40.388           --> unchanged (rtrner memCh!p, resbar rmhist!p)"
  40.389 -  apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "e_def",
  40.390 -    thm "c_def", thm "r_def", thm "resbar_def"]) [] [] 1 *})
  40.391 +  apply (tactic {* action_simp_tac (@{simpset} addsimps [@{thm e_def},
  40.392 +    @{thm c_def}, @{thm r_def}, @{thm resbar_def}]) [] [] 1 *})
  40.393    apply (drule S4_excl [temp_use] S5_excl [temp_use])+
  40.394 -  apply (tactic {* auto_tac (MI_fast_css addsimps2 [thm "MemReturn_def", thm "Return_def"]) *})
  40.395 +  apply (tactic {* auto_tac (MI_fast_css addsimps2 [@{thm MemReturn_def}, @{thm Return_def}]) *})
  40.396    done
  40.397  
  40.398  lemma Step1_4_5a: "|- RPCReply crCh rmCh rst p & $S5 rmhist p & (S6 rmhist p)$
  40.399 @@ -752,12 +752,12 @@
  40.400           --> MemReturn memCh (resbar rmhist) p"
  40.401    apply clarsimp
  40.402    apply (drule S6_excl [temp_use])+
  40.403 -  apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "e_def",
  40.404 -    thm "r_def", thm "m_def", thm "MClkReply_def", thm "MemReturn_def",
  40.405 -    thm "Return_def", thm "resbar_def"]) [] [] 1 *})
  40.406 +  apply (tactic {* action_simp_tac (@{simpset} addsimps [@{thm e_def},
  40.407 +    @{thm r_def}, @{thm m_def}, @{thm MClkReply_def}, @{thm MemReturn_def},
  40.408 +    @{thm Return_def}, @{thm resbar_def}]) [] [] 1 *})
  40.409      apply simp_all (* simplify if-then-else *)
  40.410      apply (tactic {* ALLGOALS (action_simp_tac (@{simpset} addsimps
  40.411 -      [thm "MClkReplyVal_def", thm "S6_def", thm "S_def"]) [] [thm "MVOKBARFnotNR"]) *})
  40.412 +      [@{thm MClkReplyVal_def}, @{thm S6_def}, @{thm S_def}]) [] [@{thm MVOKBARFnotNR}]) *})
  40.413    done
  40.414  
  40.415  lemma Step1_4_6b: "|- MClkRetry memCh crCh cst p & $S6 rmhist p & (S3 rmhist p)$
  40.416 @@ -765,8 +765,8 @@
  40.417           --> MemFail memCh (resbar rmhist) p"
  40.418    apply clarsimp
  40.419    apply (drule S3_excl [temp_use])+
  40.420 -  apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "e_def", thm "r_def",
  40.421 -    thm "m_def", thm "MClkRetry_def", thm "MemFail_def", thm "resbar_def"]) [] [] 1 *})
  40.422 +  apply (tactic {* action_simp_tac (@{simpset} addsimps [@{thm e_def}, @{thm r_def},
  40.423 +    @{thm m_def}, @{thm MClkRetry_def}, @{thm MemFail_def}, @{thm resbar_def}]) [] [] 1 *})
  40.424     apply (auto simp: S6_def S_def)
  40.425    done
  40.426  
  40.427 @@ -816,7 +816,7 @@
  40.428  lemma unchanged_safe: "|- (~unchanged (e p, c p, r p, m p, rmhist!p)
  40.429               --> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p))
  40.430           --> [UNext memCh mm (resbar rmhist) p]_(rtrner memCh!p, resbar rmhist!p)"
  40.431 -  apply (tactic {* split_idle_tac @{context} [thm "square_def"] 1 *})
  40.432 +  apply (tactic {* split_idle_tac @{context} [@{thm square_def}] 1 *})
  40.433    apply force
  40.434    done
  40.435  (* turn into (unsafe, looping!) introduction rule *)
  40.436 @@ -898,15 +898,15 @@
  40.437  
  40.438  lemma S1_RNextdisabled: "|- S1 rmhist p -->
  40.439           ~Enabled (<RNext memCh mm (resbar rmhist) p>_(rtrner memCh!p, resbar rmhist!p))"
  40.440 -  apply (tactic {* action_simp_tac (@{simpset} addsimps [thm "angle_def",
  40.441 -    thm "S_def", thm "S1_def"]) [notI] [thm "enabledE", temp_elim (thm "Memoryidle")] 1 *})
  40.442 +  apply (tactic {* action_simp_tac (@{simpset} addsimps [@{thm angle_def},
  40.443 +    @{thm S_def}, @{thm S1_def}]) [notI] [@{thm enabledE}, temp_elim @{thm Memoryidle}] 1 *})
  40.444    apply force
  40.445    done
  40.446  
  40.447  lemma S1_Returndisabled: "|- S1 rmhist p -->
  40.448           ~Enabled (<MemReturn memCh (resbar rmhist) p>_(rtrner memCh!p, resbar rmhist!p))"
  40.449 -  by (tactic {* action_simp_tac (@{simpset} addsimps [thm "angle_def", thm "MemReturn_def",
  40.450 -    thm "Return_def", thm "S_def", thm "S1_def"]) [notI] [thm "enabledE"] 1 *})
  40.451 +  by (tactic {* action_simp_tac (@{simpset} addsimps [@{thm angle_def}, @{thm MemReturn_def},
  40.452 +    @{thm Return_def}, @{thm S_def}, @{thm S1_def}]) [notI] [@{thm enabledE}] 1 *})
  40.453  
  40.454  lemma RNext_fair: "|- []<>S1 rmhist p
  40.455           --> WF(RNext memCh mm (resbar rmhist) p)_(rtrner memCh!p, resbar rmhist!p)"
  40.456 @@ -986,7 +986,7 @@
  40.457           & ImpNext p & [HNext rmhist p]_(c p,r p,m p,rmhist!p) & (ALL l. $MemInv mm l)
  40.458           --> (S4 rmhist p & ires!p = #NotAResult)$
  40.459               | ((S4 rmhist p & ires!p ~= #NotAResult) | S5 rmhist p)$"
  40.460 -  apply (tactic {* split_idle_tac @{context} [thm "m_def"] 1 *})
  40.461 +  apply (tactic {* split_idle_tac @{context} [@{thm m_def}] 1 *})
  40.462    apply (auto dest!: Step1_2_4 [temp_use])
  40.463    done
  40.464  
  40.465 @@ -1017,7 +1017,7 @@
  40.466  lemma S4b_successors: "|- $(S4 rmhist p & ires!p ~= #NotAResult)
  40.467           & ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) & (ALL l. $MemInv mm l)
  40.468           --> (S4 rmhist p & ires!p ~= #NotAResult)$ | (S5 rmhist p)$"
  40.469 -  apply (tactic {* split_idle_tac @{context} [thm "m_def"] 1 *})
  40.470 +  apply (tactic {* split_idle_tac @{context} [@{thm m_def}] 1 *})
  40.471    apply (auto dest!: WriteResult [temp_use] Step1_2_4 [temp_use] ReadResult [temp_use])
  40.472    done
  40.473  
  40.474 @@ -1084,16 +1084,16 @@
  40.475  
  40.476  lemma MClkReplyS6:
  40.477    "|- $ImpInv rmhist p & <MClkReply memCh crCh cst p>_(c p) --> $S6 rmhist p"
  40.478 -  by (tactic {* action_simp_tac (@{simpset} addsimps [thm "angle_def",
  40.479 -    thm "MClkReply_def", thm "Return_def", thm "ImpInv_def", thm "S_def",
  40.480 -    thm "S1_def", thm "S2_def", thm "S3_def", thm "S4_def", thm "S5_def"]) [] [] 1 *})
  40.481 +  by (tactic {* action_simp_tac (@{simpset} addsimps [@{thm angle_def},
  40.482 +    @{thm MClkReply_def}, @{thm Return_def}, @{thm ImpInv_def}, @{thm S_def},
  40.483 +    @{thm S1_def}, @{thm S2_def}, @{thm S3_def}, @{thm S4_def}, @{thm S5_def}]) [] [] 1 *})
  40.484  
  40.485  lemma S6MClkReply_enabled: "|- S6 rmhist p --> Enabled (<MClkReply memCh crCh cst p>_(c p))"
  40.486    apply (auto simp: c_def intro!: MClkReply_enabled [temp_use])
  40.487       apply (cut_tac MI_base)
  40.488       apply (blast dest: base_pair)
  40.489      apply (tactic {* ALLGOALS (action_simp_tac (@{simpset}
  40.490 -      addsimps [thm "S_def", thm "S6_def"]) [] []) *})
  40.491 +      addsimps [@{thm S_def}, @{thm S6_def}]) [] []) *})
  40.492    done
  40.493  
  40.494  lemma S6_live: "|- [](ImpNext p & [HNext rmhist p]_(c p,r p,m p, rmhist!p) & $(ImpInv rmhist p))
  40.495 @@ -1104,7 +1104,7 @@
  40.496     apply (erule InfiniteEnsures)
  40.497      apply assumption
  40.498     apply (tactic {* action_simp_tac @{simpset} []
  40.499 -     (map temp_elim [thm "MClkReplyS6", thm "S6MClkReply_successors"]) 1 *})
  40.500 +     (map temp_elim [@{thm MClkReplyS6}, @{thm S6MClkReply_successors}]) 1 *})
  40.501    apply (auto simp: SF_def)
  40.502    apply (erule contrapos_np)
  40.503    apply (auto intro!: S6MClkReply_enabled [temp_use] elim!: STL4E [temp_use] DmdImplE [temp_use])
  40.504 @@ -1191,7 +1191,7 @@
  40.505        ==> sigma |= []<>S1 rmhist p"
  40.506    apply (rule classical)
  40.507    apply (tactic {* asm_lr_simp_tac (@{simpset} addsimps
  40.508 -    [temp_use (thm "NotBox"), temp_rewrite (thm "NotDmd")]) 1 *})
  40.509 +    [temp_use @{thm NotBox}, temp_rewrite @{thm NotDmd}]) 1 *})
  40.510    apply (auto elim!: leadsto_infinite [temp_use] mp dest!: DBImplBD [temp_use])
  40.511    done
  40.512  
    41.1 --- a/src/HOL/TLA/Memory/RPC.thy	Mon Sep 06 19:11:01 2010 +0200
    41.2 +++ b/src/HOL/TLA/Memory/RPC.thy	Mon Sep 06 19:13:10 2010 +0200
    41.3 @@ -103,15 +103,15 @@
    41.4  (* Enabledness of some actions *)
    41.5  lemma RPCFail_enabled: "!!p. basevars (rtrner send!p, caller rcv!p, rst!p) ==>  
    41.6      |- ~Calling rcv p & Calling send p --> Enabled (RPCFail send rcv rst p)"
    41.7 -  by (tactic {* action_simp_tac (@{simpset} addsimps [thm "RPCFail_def",
    41.8 -    thm "Return_def", thm "caller_def", thm "rtrner_def"]) [exI]
    41.9 -    [thm "base_enabled", thm "Pair_inject"] 1 *})
   41.10 +  by (tactic {* action_simp_tac (@{simpset} addsimps [@{thm RPCFail_def},
   41.11 +    @{thm Return_def}, @{thm caller_def}, @{thm rtrner_def}]) [exI]
   41.12 +    [@{thm base_enabled}, @{thm Pair_inject}] 1 *})
   41.13  
   41.14  lemma RPCReply_enabled: "!!p. basevars (rtrner send!p, caller rcv!p, rst!p) ==>  
   41.15        |- ~Calling rcv p & Calling send p & rst!p = #rpcB  
   41.16           --> Enabled (RPCReply send rcv rst p)"
   41.17 -  by (tactic {* action_simp_tac (@{simpset} addsimps [thm "RPCReply_def",
   41.18 -    thm "Return_def", thm "caller_def", thm "rtrner_def"]) [exI]
   41.19 -    [thm "base_enabled", thm "Pair_inject"] 1 *})
   41.20 +  by (tactic {* action_simp_tac (@{simpset} addsimps [@{thm RPCReply_def},
   41.21 +    @{thm Return_def}, @{thm caller_def}, @{thm rtrner_def}]) [exI]
   41.22 +    [@{thm base_enabled}, @{thm Pair_inject}] 1 *})
   41.23  
   41.24  end
    42.1 --- a/src/HOL/Tools/Qelim/cooper.ML	Mon Sep 06 19:11:01 2010 +0200
    42.2 +++ b/src/HOL/Tools/Qelim/cooper.ML	Mon Sep 06 19:13:10 2010 +0200
    42.3 @@ -423,7 +423,7 @@
    42.4  val emptyIS = @{cterm "{}::int set"};
    42.5  val insert_tm = @{cterm "insert :: int => _"};
    42.6  fun mkISet cts = fold_rev (Thm.capply insert_tm #> Thm.capply) cts emptyIS;
    42.7 -val eqelem_imp_imp = (thm"eqelem_imp_iff") RS iffD1;
    42.8 +val eqelem_imp_imp = @{thm eqelem_imp_iff} RS iffD1;
    42.9  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
   42.10                                        |> Thm.dest_abs NONE |> snd |> Thm.dest_fun |> Thm.dest_arg)
   42.11                        [asetP,bsetP];
    43.1 --- a/src/HOL/Tools/TFL/casesplit.ML	Mon Sep 06 19:11:01 2010 +0200
    43.2 +++ b/src/HOL/Tools/TFL/casesplit.ML	Mon Sep 06 19:13:10 2010 +0200
    43.3 @@ -32,9 +32,9 @@
    43.4  val dest_Trueprop = HOLogic.dest_Trueprop;
    43.5  val mk_Trueprop = HOLogic.mk_Trueprop;
    43.6  
    43.7 -val atomize = thms "induct_atomize";
    43.8 -val rulify = thms "induct_rulify";
    43.9 -val rulify_fallback = thms "induct_rulify_fallback";
   43.10 +val atomize = @{thms induct_atomize};
   43.11 +val rulify = @{thms induct_rulify};
   43.12 +val rulify_fallback = @{thms induct_rulify_fallback};
   43.13  
   43.14  end;
   43.15  
    44.1 --- a/src/HOL/Tools/TFL/thms.ML	Mon Sep 06 19:11:01 2010 +0200
    44.2 +++ b/src/HOL/Tools/TFL/thms.ML	Mon Sep 06 19:13:10 2010 +0200
    44.3 @@ -1,20 +1,19 @@
    44.4  (*  Title:      HOL/Tools/TFL/thms.ML
    44.5 -    ID:         $Id$
    44.6      Author:     Konrad Slind, Cambridge University Computer Laboratory
    44.7      Copyright   1997  University of Cambridge
    44.8  *)
    44.9  
   44.10  structure Thms =
   44.11  struct
   44.12 -  val WFREC_COROLLARY = thm "tfl_wfrec";
   44.13 -  val WF_INDUCTION_THM = thm "tfl_wf_induct";
   44.14 -  val CUT_DEF = thm "cut_def";
   44.15 -  val eqT = thm "tfl_eq_True";
   44.16 -  val rev_eq_mp = thm "tfl_rev_eq_mp";
   44.17 -  val simp_thm = thm "tfl_simp_thm";
   44.18 -  val P_imp_P_iff_True = thm "tfl_P_imp_P_iff_True";
   44.19 -  val imp_trans = thm "tfl_imp_trans";
   44.20 -  val disj_assoc = thm "tfl_disj_assoc";
   44.21 -  val tfl_disjE = thm "tfl_disjE";
   44.22 -  val choose_thm = thm "tfl_exE";
   44.23 +  val WFREC_COROLLARY = @{thm tfl_wfrec};
   44.24 +  val WF_INDUCTION_THM = @{thm tfl_wf_induct};
   44.25 +  val CUT_DEF = @{thm cut_def};
   44.26 +  val eqT = @{thm tfl_eq_True};
   44.27 +  val rev_eq_mp = @{thm tfl_rev_eq_mp};
   44.28 +  val simp_thm = @{thm tfl_simp_thm};
   44.29 +  val P_imp_P_iff_True = @{thm tfl_P_imp_P_iff_True};
   44.30 +  val imp_trans = @{thm tfl_imp_trans};
   44.31 +  val disj_assoc = @{thm tfl_disj_assoc};
   44.32 +  val tfl_disjE = @{thm tfl_disjE};
   44.33 +  val choose_thm = @{thm tfl_exE};
   44.34  end;
    45.1 --- a/src/HOL/Tools/meson.ML	Mon Sep 06 19:11:01 2010 +0200
    45.2 +++ b/src/HOL/Tools/meson.ML	Mon Sep 06 19:13:10 2010 +0200
    45.3 @@ -68,24 +68,24 @@
    45.4  val ex_forward = @{thm ex_forward};
    45.5  val choice = @{thm choice};
    45.6  
    45.7 -val not_conjD = thm "meson_not_conjD";
    45.8 -val not_disjD = thm "meson_not_disjD";
    45.9 -val not_notD = thm "meson_not_notD";
   45.10 -val not_allD = thm "meson_not_allD";
   45.11 -val not_exD = thm "meson_not_exD";
   45.12 -val imp_to_disjD = thm "meson_imp_to_disjD";
   45.13 -val not_impD = thm "meson_not_impD";
   45.14 -val iff_to_disjD = thm "meson_iff_to_disjD";
   45.15 -val not_iffD = thm "meson_not_iffD";
   45.16 -val conj_exD1 = thm "meson_conj_exD1";
   45.17 -val conj_exD2 = thm "meson_conj_exD2";
   45.18 -val disj_exD = thm "meson_disj_exD";
   45.19 -val disj_exD1 = thm "meson_disj_exD1";
   45.20 -val disj_exD2 = thm "meson_disj_exD2";
   45.21 -val disj_assoc = thm "meson_disj_assoc";
   45.22 -val disj_comm = thm "meson_disj_comm";
   45.23 -val disj_FalseD1 = thm "meson_disj_FalseD1";
   45.24 -val disj_FalseD2 = thm "meson_disj_FalseD2";
   45.25 +val not_conjD = @{thm meson_not_conjD};
   45.26 +val not_disjD = @{thm meson_not_disjD};
   45.27 +val not_notD = @{thm meson_not_notD};
   45.28 +val not_allD = @{thm meson_not_allD};
   45.29 +val not_exD = @{thm meson_not_exD};
   45.30 +val imp_to_disjD = @{thm meson_imp_to_disjD};
   45.31 +val not_impD = @{thm meson_not_impD};
   45.32 +val iff_to_disjD = @{thm meson_iff_to_disjD};
   45.33 +val not_iffD = @{thm meson_not_iffD};
   45.34 +val conj_exD1 = @{thm meson_conj_exD1};
   45.35 +val conj_exD2 = @{thm meson_conj_exD2};
   45.36 +val disj_exD = @{thm meson_disj_exD};
   45.37 +val disj_exD1 = @{thm meson_disj_exD1};
   45.38 +val disj_exD2 = @{thm meson_disj_exD2};
   45.39 +val disj_assoc = @{thm meson_disj_assoc};
   45.40 +val disj_comm = @{thm meson_disj_comm};
   45.41 +val disj_FalseD1 = @{thm meson_disj_FalseD1};
   45.42 +val disj_FalseD2 = @{thm meson_disj_FalseD2};
   45.43  
   45.44  
   45.45  (**** Operators for forward proof ****)
   45.46 @@ -203,7 +203,7 @@
   45.47  (*They are typically functional reflexivity axioms and are the converses of
   45.48    injectivity equivalences*)
   45.49  
   45.50 -val not_refl_disj_D = thm"meson_not_refl_disj_D";
   45.51 +val not_refl_disj_D = @{thm meson_not_refl_disj_D};
   45.52  
   45.53  (*Is either term a Var that does not properly occur in the other term?*)
   45.54  fun eliminable (t as Var _, u) = t aconv u orelse not (Logic.occs(t,u))
    46.1 --- a/src/HOL/UNITY/Comp/Alloc.thy	Mon Sep 06 19:11:01 2010 +0200
    46.2 +++ b/src/HOL/UNITY/Comp/Alloc.thy	Mon Sep 06 19:13:10 2010 +0200
    46.3 @@ -426,7 +426,7 @@
    46.4    apply (rule fst_o_funPair)
    46.5    done
    46.6  
    46.7 -ML {* bind_thms ("fst_o_client_map'", make_o_equivs (thm "fst_o_client_map")) *}
    46.8 +ML {* bind_thms ("fst_o_client_map'", make_o_equivs @{thm fst_o_client_map}) *}
    46.9  declare fst_o_client_map' [simp]
   46.10  
   46.11  lemma snd_o_client_map: "snd o client_map = clientState_d.dummy"
   46.12 @@ -434,7 +434,7 @@
   46.13    apply (rule snd_o_funPair)
   46.14    done
   46.15  
   46.16 -ML {* bind_thms ("snd_o_client_map'", make_o_equivs (thm "snd_o_client_map")) *}
   46.17 +ML {* bind_thms ("snd_o_client_map'", make_o_equivs @{thm snd_o_client_map}) *}
   46.18  declare snd_o_client_map' [simp]
   46.19  
   46.20  
   46.21 @@ -444,28 +444,28 @@
   46.22    apply record_auto
   46.23    done
   46.24  
   46.25 -ML {* bind_thms ("client_o_sysOfAlloc'", make_o_equivs (thm "client_o_sysOfAlloc")) *}
   46.26 +ML {* bind_thms ("client_o_sysOfAlloc'", make_o_equivs @{thm client_o_sysOfAlloc}) *}
   46.27  declare client_o_sysOfAlloc' [simp]
   46.28  
   46.29  lemma allocGiv_o_sysOfAlloc_eq: "allocGiv o sysOfAlloc = allocGiv"
   46.30    apply record_auto
   46.31    done
   46.32  
   46.33 -ML {* bind_thms ("allocGiv_o_sysOfAlloc_eq'", make_o_equivs (thm "allocGiv_o_sysOfAlloc_eq")) *}
   46.34 +ML {* bind_thms ("allocGiv_o_sysOfAlloc_eq'", make_o_equivs @{thm allocGiv_o_sysOfAlloc_eq}) *}
   46.35  declare allocGiv_o_sysOfAlloc_eq' [simp]
   46.36  
   46.37  lemma allocAsk_o_sysOfAlloc_eq: "allocAsk o sysOfAlloc = allocAsk"
   46.38    apply record_auto
   46.39    done
   46.40  
   46.41 -ML {* bind_thms ("allocAsk_o_sysOfAlloc_eq'", make_o_equivs (thm "allocAsk_o_sysOfAlloc_eq")) *}
   46.42 +ML {* bind_thms ("allocAsk_o_sysOfAlloc_eq'", make_o_equivs @{thm allocAsk_o_sysOfAlloc_eq}) *}
   46.43  declare allocAsk_o_sysOfAlloc_eq' [simp]
   46.44  
   46.45  lemma allocRel_o_sysOfAlloc_eq: "allocRel o sysOfAlloc = allocRel"
   46.46    apply record_auto
   46.47    done
   46.48  
   46.49 -ML {* bind_thms ("allocRel_o_sysOfAlloc_eq'", make_o_equivs (thm "allocRel_o_sysOfAlloc_eq")) *}
   46.50 +ML {* bind_thms ("allocRel_o_sysOfAlloc_eq'", make_o_equivs @{thm allocRel_o_sysOfAlloc_eq}) *}
   46.51  declare allocRel_o_sysOfAlloc_eq' [simp]
   46.52  
   46.53  
   46.54 @@ -475,49 +475,49 @@
   46.55    apply record_auto
   46.56    done
   46.57  
   46.58 -ML {* bind_thms ("client_o_sysOfClient'", make_o_equivs (thm "client_o_sysOfClient")) *}
   46.59 +ML {* bind_thms ("client_o_sysOfClient'", make_o_equivs @{thm client_o_sysOfClient}) *}
   46.60  declare client_o_sysOfClient' [simp]
   46.61  
   46.62  lemma allocGiv_o_sysOfClient_eq: "allocGiv o sysOfClient = allocGiv o snd "
   46.63    apply record_auto
   46.64    done
   46.65  
   46.66 -ML {* bind_thms ("allocGiv_o_sysOfClient_eq'", make_o_equivs (thm "allocGiv_o_sysOfClient_eq")) *}
   46.67 +ML {* bind_thms ("allocGiv_o_sysOfClient_eq'", make_o_equivs @{thm allocGiv_o_sysOfClient_eq}) *}
   46.68  declare allocGiv_o_sysOfClient_eq' [simp]
   46.69  
   46.70  lemma allocAsk_o_sysOfClient_eq: "allocAsk o sysOfClient = allocAsk o snd "
   46.71    apply record_auto
   46.72    done
   46.73  
   46.74 -ML {* bind_thms ("allocAsk_o_sysOfClient_eq'", make_o_equivs (thm "allocAsk_o_sysOfClient_eq")) *}
   46.75 +ML {* bind_thms ("allocAsk_o_sysOfClient_eq'", make_o_equivs @{thm allocAsk_o_sysOfClient_eq}) *}
   46.76  declare allocAsk_o_sysOfClient_eq' [simp]
   46.77  
   46.78  lemma allocRel_o_sysOfClient_eq: "allocRel o sysOfClient = allocRel o snd "
   46.79    apply record_auto
   46.80    done
   46.81  
   46.82 -ML {* bind_thms ("allocRel_o_sysOfClient_eq'", make_o_equivs (thm "allocRel_o_sysOfClient_eq")) *}
   46.83 +ML {* bind_thms ("allocRel_o_sysOfClient_eq'", make_o_equivs @{thm allocRel_o_sysOfClient_eq}) *}
   46.84  declare allocRel_o_sysOfClient_eq' [simp]
   46.85  
   46.86  lemma allocGiv_o_inv_sysOfAlloc_eq: "allocGiv o inv sysOfAlloc = allocGiv"
   46.87    apply (simp add: o_def)
   46.88    done
   46.89  
   46.90 -ML {* bind_thms ("allocGiv_o_inv_sysOfAlloc_eq'", make_o_equivs (thm "allocGiv_o_inv_sysOfAlloc_eq")) *}
   46.91 +ML {* bind_thms ("allocGiv_o_inv_sysOfAlloc_eq'", make_o_equivs @{thm allocGiv_o_inv_sysOfAlloc_eq}) *}
   46.92  declare allocGiv_o_inv_sysOfAlloc_eq' [simp]
   46.93  
   46.94  lemma allocAsk_o_inv_sysOfAlloc_eq: "allocAsk o inv sysOfAlloc = allocAsk"
   46.95    apply (simp add: o_def)
   46.96    done
   46.97  
   46.98 -ML {* bind_thms ("allocAsk_o_inv_sysOfAlloc_eq'", make_o_equivs (thm "allocAsk_o_inv_sysOfAlloc_eq")) *}
   46.99 +ML {* bind_thms ("allocAsk_o_inv_sysOfAlloc_eq'", make_o_equivs @{thm allocAsk_o_inv_sysOfAlloc_eq}) *}
  46.100  declare allocAsk_o_inv_sysOfAlloc_eq' [simp]
  46.101  
  46.102  lemma allocRel_o_inv_sysOfAlloc_eq: "allocRel o inv sysOfAlloc = allocRel"
  46.103    apply (simp add: o_def)
  46.104    done
  46.105  
  46.106 -ML {* bind_thms ("allocRel_o_inv_sysOfAlloc_eq'", make_o_equivs (thm "allocRel_o_inv_sysOfAlloc_eq")) *}
  46.107 +ML {* bind_thms ("allocRel_o_inv_sysOfAlloc_eq'", make_o_equivs @{thm allocRel_o_inv_sysOfAlloc_eq}) *}
  46.108  declare allocRel_o_inv_sysOfAlloc_eq' [simp]
  46.109  
  46.110  lemma rel_inv_client_map_drop_map: "(rel o inv client_map o drop_map i o inv sysOfClient) =
  46.111 @@ -525,7 +525,7 @@
  46.112    apply (simp add: o_def drop_map_def)
  46.113    done
  46.114  
  46.115 -ML {* bind_thms ("rel_inv_client_map_drop_map'", make_o_equivs (thm "rel_inv_client_map_drop_map")) *}
  46.116 +ML {* bind_thms ("rel_inv_client_map_drop_map'", make_o_equivs @{thm rel_inv_client_map_drop_map}) *}
  46.117  declare rel_inv_client_map_drop_map [simp]
  46.118  
  46.119  lemma ask_inv_client_map_drop_map: "(ask o inv client_map o drop_map i o inv sysOfClient) =
  46.120 @@ -533,7 +533,7 @@
  46.121    apply (simp add: o_def drop_map_def)
  46.122    done
  46.123  
  46.124 -ML {* bind_thms ("ask_inv_client_map_drop_map'", make_o_equivs (thm "ask_inv_client_map_drop_map")) *}
  46.125 +ML {* bind_thms ("ask_inv_client_map_drop_map'", make_o_equivs @{thm ask_inv_client_map_drop_map}) *}
  46.126  declare ask_inv_client_map_drop_map [simp]
  46.127  
  46.128  
  46.129 @@ -812,7 +812,7 @@
  46.130  
  46.131  
  46.132  ML {*
  46.133 -bind_thms ("System_Increasing'", list_of_Int (thm "System_Increasing"))
  46.134 +bind_thms ("System_Increasing'", list_of_Int @{thm System_Increasing})
  46.135  *}
  46.136  
  46.137  declare System_Increasing' [intro!]
  46.138 @@ -903,9 +903,9 @@
  46.139  text{*safety (1), step 4 (final result!) *}
  46.140  theorem System_safety: "System : system_safety"
  46.141    apply (unfold system_safety_def)
  46.142 -  apply (tactic {* rtac (Always_Int_rule [thm "System_sum_bounded",
  46.143 -    thm "Always_tokens_giv_le_allocGiv", thm "Always_tokens_allocRel_le_rel"] RS
  46.144 -    thm "Always_weaken") 1 *})
  46.145 +  apply (tactic {* rtac (Always_Int_rule [@{thm System_sum_bounded},
  46.146 +    @{thm Always_tokens_giv_le_allocGiv}, @{thm Always_tokens_allocRel_le_rel}] RS
  46.147 +    @{thm Always_weaken}) 1 *})
  46.148    apply auto
  46.149    apply (rule setsum_fun_mono [THEN order_trans])
  46.150    apply (drule_tac [2] order_trans)
  46.151 @@ -946,8 +946,8 @@
  46.152  lemma System_Bounded_allocAsk: "System : Always {s. ALL i<Nclients.
  46.153                            ALL elt : set ((sub i o allocAsk) s). elt \<le> NbT}"
  46.154    apply (auto simp add: Collect_all_imp_eq)
  46.155 -  apply (tactic {* rtac (Always_Int_rule [thm "Always_allocAsk_le_ask",
  46.156 -    thm "System_Bounded_ask"] RS thm "Always_weaken") 1 *})
  46.157 +  apply (tactic {* rtac (Always_Int_rule [@{thm Always_allocAsk_le_ask},
  46.158 +    @{thm System_Bounded_ask}] RS @{thm Always_weaken}) 1 *})
  46.159    apply (auto dest: set_mono)
  46.160    done
  46.161  
    47.1 --- a/src/HOLCF/FOCUS/Fstream.thy	Mon Sep 06 19:11:01 2010 +0200
    47.2 +++ b/src/HOLCF/FOCUS/Fstream.thy	Mon Sep 06 19:13:10 2010 +0200
    47.3 @@ -156,12 +156,12 @@
    47.4  lemma slen_fscons_eq_rev:
    47.5          "(#x < Fin (Suc (Suc n))) = (!a y. x ~= a~> y | #y < Fin (Suc n))"
    47.6  apply (simp add: fscons_def2 slen_scons_eq_rev)
    47.7 -apply (tactic {* step_tac (HOL_cs addSEs [thm "DefE"]) 1 *})
    47.8 -apply (tactic {* step_tac (HOL_cs addSEs [thm "DefE"]) 1 *})
    47.9 -apply (tactic {* step_tac (HOL_cs addSEs [thm "DefE"]) 1 *})
   47.10 -apply (tactic {* step_tac (HOL_cs addSEs [thm "DefE"]) 1 *})
   47.11 -apply (tactic {* step_tac (HOL_cs addSEs [thm "DefE"]) 1 *})
   47.12 -apply (tactic {* step_tac (HOL_cs addSEs [thm "DefE"]) 1 *})
   47.13 +apply (tactic {* step_tac (HOL_cs addSEs @{thms DefE}) 1 *})
   47.14 +apply (tactic {* step_tac (HOL_cs addSEs @{thms DefE}) 1 *})
   47.15 +apply (tactic {* step_tac (HOL_cs addSEs @{thms DefE}) 1 *})
   47.16 +apply (tactic {* step_tac (HOL_cs addSEs @{thms DefE}) 1 *})
   47.17 +apply (tactic {* step_tac (HOL_cs addSEs @{thms DefE}) 1 *})
   47.18 +apply (tactic {* step_tac (HOL_cs addSEs @{thms DefE}) 1 *})
   47.19  apply (erule contrapos_np)
   47.20  apply (fast dest: not_Undef_is_Def [THEN iffD1] elim: DefE)
   47.21  done
    48.1 --- a/src/HOLCF/IOA/ABP/Correctness.thy	Mon Sep 06 19:11:01 2010 +0200
    48.2 +++ b/src/HOLCF/IOA/ABP/Correctness.thy	Mon Sep 06 19:13:10 2010 +0200
    48.3 @@ -164,16 +164,16 @@
    48.4  
    48.5  lemma sender_abstraction: "is_weak_ref_map reduce srch_ioa srch_fin_ioa"
    48.6  apply (tactic {*
    48.7 -  simp_tac (HOL_ss addsimps [thm "srch_fin_ioa_def", thm "rsch_fin_ioa_def",
    48.8 -    thm "srch_ioa_def", thm "rsch_ioa_def", thm "rename_through_pmap",
    48.9 -    thm "channel_abstraction"]) 1 *})
   48.10 +  simp_tac (HOL_ss addsimps [@{thm srch_fin_ioa_def}, @{thm rsch_fin_ioa_def},
   48.11 +    @{thm srch_ioa_def}, @{thm rsch_ioa_def}, @{thm rename_through_pmap},
   48.12 +    @{thm channel_abstraction}]) 1 *})
   48.13  done
   48.14  
   48.15  lemma receiver_abstraction: "is_weak_ref_map reduce rsch_ioa rsch_fin_ioa"
   48.16  apply (tactic {*
   48.17 -  simp_tac (HOL_ss addsimps [thm "srch_fin_ioa_def", thm "rsch_fin_ioa_def",
   48.18 -    thm "srch_ioa_def", thm "rsch_ioa_def", thm "rename_through_pmap",
   48.19 -    thm "channel_abstraction"]) 1 *})
   48.20 +  simp_tac (HOL_ss addsimps [@{thm srch_fin_ioa_def}, @{thm rsch_fin_ioa_def},
   48.21 +    @{thm srch_ioa_def}, @{thm rsch_ioa_def}, @{thm rename_through_pmap},
   48.22 +    @{thm channel_abstraction}]) 1 *})
   48.23  done
   48.24  
   48.25  
    49.1 --- a/src/HOLCF/IOA/meta_theory/CompoScheds.thy	Mon Sep 06 19:11:01 2010 +0200
    49.2 +++ b/src/HOLCF/IOA/meta_theory/CompoScheds.thy	Mon Sep 06 19:13:10 2010 +0200
    49.3 @@ -289,9 +289,9 @@
    49.4  ML {*
    49.5  
    49.6  local
    49.7 -  val defs = [thm "Filter_def", thm "Forall_def", thm "sforall_def", thm "mkex_def",
    49.8 -    thm "stutter_def"]
    49.9 -  val asigs = [thm "asig_of_par", thm "actions_asig_comp"]
   49.10 +  val defs = [@{thm Filter_def}, @{thm Forall_def}, @{thm sforall_def}, @{thm mkex_def},
   49.11 +    @{thm stutter_def}]
   49.12 +  val asigs = [@{thm asig_of_par}, @{thm actions_asig_comp}]
   49.13  in
   49.14  
   49.15  fun mkex_induct_tac ctxt sch exA exB =
    50.1 --- a/src/HOLCF/IOA/meta_theory/SimCorrectness.thy	Mon Sep 06 19:11:01 2010 +0200
    50.2 +++ b/src/HOLCF/IOA/meta_theory/SimCorrectness.thy	Mon Sep 06 19:13:10 2010 +0200
    50.3 @@ -171,7 +171,7 @@
    50.4           !s s'. reachable C s & is_exec_frag C (s,ex) & (s,s'): R -->
    50.5               mk_trace C$ex = mk_trace A$((corresp_ex_simC A R$ex) s')"
    50.6  
    50.7 -apply (tactic {* pair_induct_tac @{context} "ex" [thm "is_exec_frag_def"] 1 *})
    50.8 +apply (tactic {* pair_induct_tac @{context} "ex" [@{thm is_exec_frag_def}] 1 *})
    50.9  (* cons case *)
   50.10  apply auto
   50.11  apply (rename_tac ex a t s s')
    51.1 --- a/src/HOLCF/ex/Focus_ex.thy	Mon Sep 06 19:11:01 2010 +0200
    51.2 +++ b/src/HOLCF/ex/Focus_ex.thy	Mon Sep 06 19:13:10 2010 +0200
    51.3 @@ -180,7 +180,7 @@
    51.4  done
    51.5  
    51.6  lemma lemma3: "def_g(g) --> is_g(g)"
    51.7 -apply (tactic {* simp_tac (HOL_ss addsimps [thm "def_g_def", thm "lemma1", thm "lemma2"]) 1 *})
    51.8 +apply (tactic {* simp_tac (HOL_ss addsimps [@{thm def_g_def}, @{thm lemma1}, @{thm lemma2}]) 1 *})
    51.9  apply (rule impI)
   51.10  apply (erule exE)
   51.11  apply (rule_tac x = "f" in exI)
   51.12 @@ -205,7 +205,7 @@
   51.13  
   51.14  lemma lemma4: "is_g(g) --> def_g(g)"
   51.15  apply (tactic {* simp_tac (HOL_ss delsimps (@{thms HOL.ex_simps} @ @{thms HOL.all_simps})
   51.16 -  addsimps [thm "lemma1", thm "lemma2", thm "def_g_def"]) 1 *})
   51.17 +  addsimps [@{thm lemma1}, @{thm lemma2}, @{thm def_g_def}]) 1 *})
   51.18  apply (rule impI)
   51.19  apply (erule exE)
   51.20  apply (rule_tac x = "f" in exI)
    52.1 --- a/src/HOLCF/ex/Loop.thy	Mon Sep 06 19:11:01 2010 +0200
    52.2 +++ b/src/HOLCF/ex/Loop.thy	Mon Sep 06 19:13:10 2010 +0200
    52.3 @@ -104,12 +104,12 @@
    52.4  apply (simp (no_asm) add: step_def2)
    52.5  apply (rule_tac p = "b$ (iterate n$ (step$b$g) $x) " in trE)
    52.6  apply (erule notE)
    52.7 -apply (tactic {* asm_simp_tac (HOLCF_ss addsimps [thm "step_def2"]) 1 *})
    52.8 +apply (tactic {* asm_simp_tac (HOLCF_ss addsimps [@{thm step_def2}]) 1 *})
    52.9  apply (tactic "asm_simp_tac HOLCF_ss 1")
   52.10  apply (rule mp)
   52.11  apply (erule spec)
   52.12 -apply (tactic {* asm_simp_tac (HOLCF_ss delsimps [thm "iterate_Suc"]
   52.13 -  addsimps [thm "loop_lemma2"]) 1 *})
   52.14 +apply (tactic {* asm_simp_tac (HOLCF_ss delsimps [@{thm iterate_Suc}]
   52.15 +  addsimps [@{thm loop_lemma2}]) 1 *})
   52.16  apply (rule_tac s = "iterate (Suc n) $ (step$b$g) $x"
   52.17    and t = "g$ (iterate n$ (step$b$g) $x) " in ssubst)
   52.18  prefer 2 apply (assumption)
    53.1 --- a/src/Provers/quasi.ML	Mon Sep 06 19:11:01 2010 +0200
    53.2 +++ b/src/Provers/quasi.ML	Mon Sep 06 19:13:10 2010 +0200
    53.3 @@ -149,7 +149,7 @@
    53.4      | "~="  => if (x aconv y) then
    53.5                    raise Contr (Thm ([(Thm ([(Thm ([], Less.le_refl)) ,(Asm n)], Less.le_neq_trans))], Less.less_reflE))
    53.6                 else [ NotEq (x, y, Asm n),
    53.7 -                      NotEq (y, x,Thm ( [Asm n], thm "not_sym"))]
    53.8 +                      NotEq (y, x,Thm ( [Asm n], @{thm not_sym}))]
    53.9      | _     => error ("quasi_tac: unknown relation symbol ``" ^ rel ^
   53.10                   "''returned by decomp_quasi."))
   53.11    | NONE => [];
   53.12 @@ -300,7 +300,7 @@
   53.13           let
   53.14            val leEdge  = Le (x,y, Thm ([p], Less.less_imp_le))
   53.15            val neqEdges = [ NotEq (x,y, Thm ([p], Less.less_imp_neq)),
   53.16 -                           NotEq (y,x, Thm ( [Thm ([p], Less.less_imp_neq)], thm "not_sym"))]
   53.17 +                           NotEq (y,x, Thm ( [Thm ([p], Less.less_imp_neq)], @{thm not_sym}))]
   53.18           in
   53.19             buildGraphs (ls, addEdge(y,[],(addEdge (x,[(y,leEdge)],leG))), neqEdges@neqE)
   53.20           end
   53.21 @@ -459,9 +459,10 @@
   53.22     let
   53.23      fun findParallelNeq []  = NONE
   53.24      |   findParallelNeq (e::es)  =
   53.25 -     if      (x aconv (lower e) andalso y aconv (upper e)) then SOME e
   53.26 -     else if (y aconv (lower e) andalso x aconv (upper e)) then SOME (NotEq (x,y, (Thm ([getprf e], thm "not_sym"))))
   53.27 -     else findParallelNeq es ;
   53.28 +     if (x aconv (lower e) andalso y aconv (upper e)) then SOME e
   53.29 +     else if (y aconv (lower e) andalso x aconv (upper e))
   53.30 +     then SOME (NotEq (x,y, (Thm ([getprf e], @{thm not_sym}))))
   53.31 +     else findParallelNeq es;
   53.32     in
   53.33     (* test if there is a edge x ~= y respectivly  y ~= x and     *)
   53.34     (* if it possible to find a path x <= y in leG, thus we can conclude x < y *)
   53.35 @@ -483,7 +484,7 @@
   53.36    (case (Library.find_first (fn fact => fact subsumes subgoal) neqE, subgoal) of
   53.37      (SOME (NotEq (x, y, p)), NotEq (x', y', _)) =>
   53.38        if  (x aconv x' andalso y aconv y') then p
   53.39 -      else Thm ([p], thm "not_sym")
   53.40 +      else Thm ([p], @{thm not_sym})
   53.41      | _  => raise Cannot
   53.42    )
   53.43  
    54.1 --- a/src/Sequents/ILL.thy	Mon Sep 06 19:11:01 2010 +0200
    54.2 +++ b/src/Sequents/ILL.thy	Mon Sep 06 19:13:10 2010 +0200
    54.3 @@ -126,24 +126,16 @@
    54.4  
    54.5  
    54.6  ML {*
    54.7 -
    54.8  val lazy_cs = empty_pack
    54.9 -  add_safes [thm "tensl", thm "conjr", thm "disjl", thm "promote0",
   54.10 -    thm "context2", thm "context3"]
   54.11 -  add_unsafes [thm "identity", thm "zerol", thm "conjll", thm "conjlr",
   54.12 -    thm "disjrl", thm "disjrr", thm "impr", thm "tensr", thm "impl",
   54.13 -    thm "derelict", thm "weaken", thm "promote1", thm "promote2",
   54.14 -    thm "context1", thm "context4a", thm "context4b"];
   54.15 +  add_safes [@{thm tensl}, @{thm conjr}, @{thm disjl}, @{thm promote0},
   54.16 +    @{thm context2}, @{thm context3}]
   54.17 +  add_unsafes [@{thm identity}, @{thm zerol}, @{thm conjll}, @{thm conjlr},
   54.18 +    @{thm disjrl}, @{thm disjrr}, @{thm impr}, @{thm tensr}, @{thm impl},
   54.19 +    @{thm derelict}, @{thm weaken}, @{thm promote1}, @{thm promote2},
   54.20 +    @{thm context1}, @{thm context4a}, @{thm context4b}];
   54.21  
   54.22 -local
   54.23 -  val promote0 = thm "promote0"
   54.24 -  val promote1 = thm "promote1"
   54.25 -  val promote2 = thm "promote2"
   54.26 -in
   54.27 -
   54.28 -fun prom_tac n = REPEAT (resolve_tac [promote0,promote1,promote2] n)
   54.29 -
   54.30 -end
   54.31 +fun prom_tac n =
   54.32 +  REPEAT (resolve_tac [@{thm promote0}, @{thm promote1}, @{thm promote2}] n)
   54.33  *}
   54.34  
   54.35  method_setup best_lazy =
   54.36 @@ -272,13 +264,12 @@
   54.37    done
   54.38  
   54.39  ML {*
   54.40 +val safe_cs = lazy_cs add_safes [@{thm conj_lemma}, @{thm ll_mp}, @{thm contrad1},
   54.41 +                                 @{thm contrad2}, @{thm mp_rule1}, @{thm mp_rule2}, @{thm o_a_rule},
   54.42 +                                 @{thm a_not_a_rule}]
   54.43 +                      add_unsafes [@{thm aux_impl}];
   54.44  
   54.45 -val safe_cs = lazy_cs add_safes [thm "conj_lemma", thm "ll_mp", thm "contrad1",
   54.46 -                                 thm "contrad2", thm "mp_rule1", thm "mp_rule2", thm "o_a_rule",
   54.47 -                                 thm "a_not_a_rule"]
   54.48 -                      add_unsafes [thm "aux_impl"];
   54.49 -
   54.50 -val power_cs = safe_cs add_unsafes [thm "impr_contr_der"];
   54.51 +val power_cs = safe_cs add_unsafes [@{thm impr_contr_der}];
   54.52  *}
   54.53  
   54.54  
    55.1 --- a/src/Sequents/LK0.thy	Mon Sep 06 19:11:01 2010 +0200
    55.2 +++ b/src/Sequents/LK0.thy	Mon Sep 06 19:13:10 2010 +0200
    55.3 @@ -210,27 +210,19 @@
    55.4  
    55.5  ML {*
    55.6  val prop_pack = empty_pack add_safes
    55.7 -                [thm "basic", thm "refl", thm "TrueR", thm "FalseL",
    55.8 -                 thm "conjL", thm "conjR", thm "disjL", thm "disjR", thm "impL", thm "impR",
    55.9 -                 thm "notL", thm "notR", thm "iffL", thm "iffR"];
   55.10 +                [@{thm basic}, @{thm refl}, @{thm TrueR}, @{thm FalseL},
   55.11 +                 @{thm conjL}, @{thm conjR}, @{thm disjL}, @{thm disjR}, @{thm impL}, @{thm impR},
   55.12 +                 @{thm notL}, @{thm notR}, @{thm iffL}, @{thm iffR}];
   55.13  
   55.14 -val LK_pack = prop_pack add_safes   [thm "allR", thm "exL"]
   55.15 -                        add_unsafes [thm "allL_thin", thm "exR_thin", thm "the_equality"];
   55.16 +val LK_pack = prop_pack add_safes   [@{thm allR}, @{thm exL}]
   55.17 +                        add_unsafes [@{thm allL_thin}, @{thm exR_thin}, @{thm the_equality}];
   55.18  
   55.19 -val LK_dup_pack = prop_pack add_safes   [thm "allR", thm "exL"]
   55.20 -                            add_unsafes [thm "allL", thm "exR", thm "the_equality"];
   55.21 +val LK_dup_pack = prop_pack add_safes   [@{thm allR}, @{thm exL}]
   55.22 +                            add_unsafes [@{thm allL}, @{thm exR}, @{thm the_equality}];
   55.23  
   55.24  
   55.25 -local
   55.26 -  val thinR = thm "thinR"
   55.27 -  val thinL = thm "thinL"
   55.28 -  val cut = thm "cut"
   55.29 -in
   55.30 -
   55.31  fun lemma_tac th i =
   55.32 -    rtac (thinR RS cut) i THEN REPEAT (rtac thinL i) THEN rtac th i;
   55.33 -
   55.34 -end;
   55.35 +    rtac (@{thm thinR} RS @{thm cut}) i THEN REPEAT (rtac @{thm thinL} i) THEN rtac th i;
   55.36  *}
   55.37  
   55.38  method_setup fast_prop =
   55.39 @@ -321,10 +313,10 @@
   55.40  (** Equality **)
   55.41  
   55.42  lemma sym: "|- a=b --> b=a"
   55.43 -  by (tactic {* safe_tac (LK_pack add_safes [thm "subst"]) 1 *})
   55.44 +  by (tactic {* safe_tac (LK_pack add_safes [@{thm subst}]) 1 *})
   55.45  
   55.46  lemma trans: "|- a=b --> b=c --> a=c"
   55.47 -  by (tactic {* safe_tac (LK_pack add_safes [thm "subst"]) 1 *})
   55.48 +  by (tactic {* safe_tac (LK_pack add_safes [@{thm subst}]) 1 *})
   55.49  
   55.50  (* Symmetry of equality in hypotheses *)
   55.51  lemmas symL = sym [THEN L_of_imp, standard]
    56.1 --- a/src/Sequents/S4.thy	Mon Sep 06 19:11:01 2010 +0200
    56.2 +++ b/src/Sequents/S4.thy	Mon Sep 06 19:13:10 2010 +0200
    56.3 @@ -34,12 +34,12 @@
    56.4  ML {*
    56.5  structure S4_Prover = Modal_ProverFun
    56.6  (
    56.7 -  val rewrite_rls = thms "rewrite_rls"
    56.8 -  val safe_rls = thms "safe_rls"
    56.9 -  val unsafe_rls = thms "unsafe_rls" @ [thm "boxR", thm "diaL"]
   56.10 -  val bound_rls = thms "bound_rls" @ [thm "boxL", thm "diaR"]
   56.11 -  val aside_rls = [thm "lstar0", thm "lstar1", thm "lstar2", thm "rstar0",
   56.12 -    thm "rstar1", thm "rstar2"]
   56.13 +  val rewrite_rls = @{thms rewrite_rls}
   56.14 +  val safe_rls = @{thms safe_rls}
   56.15 +  val unsafe_rls = @{thms unsafe_rls} @ [@{thm boxR}, @{thm diaL}]
   56.16 +  val bound_rls = @{thms bound_rls} @ [@{thm boxL}, @{thm diaR}]
   56.17 +  val aside_rls = [@{thm lstar0}, @{thm lstar1}, @{thm lstar2}, @{thm rstar0},
   56.18 +    @{thm rstar1}, @{thm rstar2}]
   56.19  )
   56.20  *}
   56.21  
    57.1 --- a/src/Sequents/S43.thy	Mon Sep 06 19:11:01 2010 +0200
    57.2 +++ b/src/Sequents/S43.thy	Mon Sep 06 19:13:10 2010 +0200
    57.3 @@ -79,12 +79,12 @@
    57.4  ML {*
    57.5  structure S43_Prover = Modal_ProverFun
    57.6  (
    57.7 -  val rewrite_rls = thms "rewrite_rls"
    57.8 -  val safe_rls = thms "safe_rls"
    57.9 -  val unsafe_rls = thms "unsafe_rls" @ [thm "pi1", thm "pi2"]
   57.10 -  val bound_rls = thms "bound_rls" @ [thm "boxL", thm "diaR"]
   57.11 -  val aside_rls = [thm "lstar0", thm "lstar1", thm "lstar2", thm "rstar0",
   57.12 -    thm "rstar1", thm "rstar2", thm "S43pi0", thm "S43pi1", thm "S43pi2"]
   57.13 +  val rewrite_rls = @{thms rewrite_rls}
   57.14 +  val safe_rls = @{thms safe_rls}
   57.15 +  val unsafe_rls = @{thms unsafe_rls} @ [@{thm pi1}, @{thm pi2}]
   57.16 +  val bound_rls = @{thms bound_rls} @ [@{thm boxL}, @{thm diaR}]
   57.17 +  val aside_rls = [@{thm lstar0}, @{thm lstar1}, @{thm lstar2}, @{thm rstar0},
   57.18 +    @{thm rstar1}, @{thm rstar2}, @{thm S43pi0}, @{thm S43pi1}, @{thm S43pi2}]
   57.19  )
   57.20  *}
   57.21  
    58.1 --- a/src/Sequents/T.thy	Mon Sep 06 19:11:01 2010 +0200
    58.2 +++ b/src/Sequents/T.thy	Mon Sep 06 19:13:10 2010 +0200
    58.3 @@ -33,12 +33,12 @@
    58.4  ML {*
    58.5  structure T_Prover = Modal_ProverFun
    58.6  (
    58.7 -  val rewrite_rls = thms "rewrite_rls"
    58.8 -  val safe_rls = thms "safe_rls"
    58.9 -  val unsafe_rls = thms "unsafe_rls" @ [thm "boxR", thm "diaL"]
   58.10 -  val bound_rls = thms "bound_rls" @ [thm "boxL", thm "diaR"]
   58.11 -  val aside_rls = [thm "lstar0", thm "lstar1", thm "lstar2", thm "rstar0",
   58.12 -    thm "rstar1", thm "rstar2"]
   58.13 +  val rewrite_rls = @{thms rewrite_rls}
   58.14 +  val safe_rls = @{thms safe_rls}
   58.15 +  val unsafe_rls = @{thms unsafe_rls} @ [@{thm boxR}, @{thm diaL}]
   58.16 +  val bound_rls = @{thms bound_rls} @ [@{thm boxL}, @{thm diaR}]
   58.17 +  val aside_rls = [@{thm lstar0}, @{thm lstar1}, @{thm lstar2}, @{thm rstar0},
   58.18 +    @{thm rstar1}, @{thm rstar2}]
   58.19  )
   58.20  *}
   58.21  
    59.1 --- a/src/Sequents/Washing.thy	Mon Sep 06 19:11:01 2010 +0200
    59.2 +++ b/src/Sequents/Washing.thy	Mon Sep 06 19:13:10 2010 +0200
    59.3 @@ -33,27 +33,27 @@
    59.4  
    59.5  (* "activate" definitions for use in proof *)
    59.6  
    59.7 -ML {* bind_thms ("changeI", [thm "context1"] RL ([thm "change"] RLN (2,[thm "cut"]))) *}
    59.8 -ML {* bind_thms ("load1I", [thm "context1"] RL ([thm "load1"] RLN (2,[thm "cut"]))) *}
    59.9 -ML {* bind_thms ("washI", [thm "context1"] RL ([thm "wash"] RLN (2,[thm "cut"]))) *}
   59.10 -ML {* bind_thms ("dryI", [thm "context1"] RL ([thm "dry"] RLN (2,[thm "cut"]))) *}
   59.11 +ML {* bind_thms ("changeI", [@{thm context1}] RL ([@{thm change}] RLN (2,[@{thm cut}]))) *}
   59.12 +ML {* bind_thms ("load1I", [@{thm context1}] RL ([@{thm load1}] RLN (2,[@{thm cut}]))) *}
   59.13 +ML {* bind_thms ("washI", [@{thm context1}] RL ([@{thm wash}] RLN (2,[@{thm cut}]))) *}
   59.14 +ML {* bind_thms ("dryI", [@{thm context1}] RL ([@{thm dry}] RLN (2,[@{thm cut}]))) *}
   59.15  
   59.16  (* a load of dirty clothes and two dollars gives you clean clothes *)
   59.17  
   59.18  lemma "dollar , dollar , dirty |- clean"
   59.19 -  apply (tactic {* best_tac (lazy_cs add_safes (thms "changeI" @ thms "load1I" @ thms "washI" @ thms "dryI")) 1 *})
   59.20 +  apply (tactic {* best_tac (lazy_cs add_safes (@{thms changeI} @ @{thms load1I} @ @{thms washI} @ @{thms dryI})) 1 *})
   59.21    done
   59.22  
   59.23  (* order of premises doesn't matter *)
   59.24  
   59.25  lemma "dollar , dirty , dollar |- clean"
   59.26 -  apply (tactic {* best_tac (lazy_cs add_safes (thms "changeI" @ thms "load1I" @ thms "washI" @ thms "dryI")) 1 *})
   59.27 +  apply (tactic {* best_tac (lazy_cs add_safes (@{thms changeI} @ @{thms load1I} @ @{thms washI} @ @{thms dryI})) 1 *})
   59.28    done
   59.29  
   59.30  (* alternative formulation *)
   59.31  
   59.32  lemma "dollar , dollar |- dirty -o clean"
   59.33 -  apply (tactic {* best_tac (lazy_cs add_safes (thms "changeI" @ thms "load1I" @ thms "washI" @ thms "dryI")) 1 *})
   59.34 +  apply (tactic {* best_tac (lazy_cs add_safes (@{thms changeI} @ @{thms load1I} @ @{thms washI} @ @{thms dryI})) 1 *})
   59.35    done
   59.36  
   59.37  end
    60.1 --- a/src/ZF/Bool.thy	Mon Sep 06 19:11:01 2010 +0200
    60.2 +++ b/src/ZF/Bool.thy	Mon Sep 06 19:13:10 2010 +0200
    60.3 @@ -172,45 +172,44 @@
    60.4  
    60.5  ML
    60.6  {*
    60.7 -val bool_def = thm "bool_def";
    60.8 -
    60.9 -val bool_defs = thms "bool_defs";
   60.10 -val singleton_0 = thm "singleton_0";
   60.11 -val bool_1I = thm "bool_1I";
   60.12 -val bool_0I = thm "bool_0I";
   60.13 -val one_not_0 = thm "one_not_0";
   60.14 -val one_neq_0 = thm "one_neq_0";
   60.15 -val boolE = thm "boolE";
   60.16 -val cond_1 = thm "cond_1";
   60.17 -val cond_0 = thm "cond_0";
   60.18 -val cond_type = thm "cond_type";
   60.19 -val cond_simple_type = thm "cond_simple_type";
   60.20 -val def_cond_1 = thm "def_cond_1";
   60.21 -val def_cond_0 = thm "def_cond_0";
   60.22 -val not_1 = thm "not_1";
   60.23 -val not_0 = thm "not_0";
   60.24 -val and_1 = thm "and_1";
   60.25 -val and_0 = thm "and_0";
   60.26 -val or_1 = thm "or_1";
   60.27 -val or_0 = thm "or_0";
   60.28 -val xor_1 = thm "xor_1";
   60.29 -val xor_0 = thm "xor_0";
   60.30 -val not_type = thm "not_type";
   60.31 -val and_type = thm "and_type";
   60.32 -val or_type = thm "or_type";
   60.33 -val xor_type = thm "xor_type";
   60.34 -val bool_typechecks = thms "bool_typechecks";
   60.35 -val not_not = thm "not_not";
   60.36 -val not_and = thm "not_and";
   60.37 -val not_or = thm "not_or";
   60.38 -val and_absorb = thm "and_absorb";
   60.39 -val and_commute = thm "and_commute";
   60.40 -val and_assoc = thm "and_assoc";
   60.41 -val and_or_distrib = thm "and_or_distrib";
   60.42 -val or_absorb = thm "or_absorb";
   60.43 -val or_commute = thm "or_commute";
   60.44 -val or_assoc = thm "or_assoc";
   60.45 -val or_and_distrib = thm "or_and_distrib";
   60.46 +val bool_def = @{thm bool_def};
   60.47 +val bool_defs = @{thms bool_defs};
   60.48 +val singleton_0 = @{thm singleton_0};
   60.49 +val bool_1I = @{thm bool_1I};
   60.50 +val bool_0I = @{thm bool_0I};
   60.51 +val one_not_0 = @{thm one_not_0};
   60.52 +val one_neq_0 = @{thm one_neq_0};
   60.53 +val boolE = @{thm boolE};
   60.54 +val cond_1 = @{thm cond_1};
   60.55 +val cond_0 = @{thm cond_0};
   60.56 +val cond_type = @{thm cond_type};
   60.57 +val cond_simple_type = @{thm cond_simple_type};
   60.58 +val def_cond_1 = @{thm def_cond_1};
   60.59 +val def_cond_0 = @{thm def_cond_0};
   60.60 +val not_1 = @{thm not_1};
   60.61 +val not_0 = @{thm not_0};
   60.62 +val and_1 = @{thm and_1};
   60.63 +val and_0 = @{thm and_0};
   60.64 +val or_1 = @{thm or_1};
   60.65 +val or_0 = @{thm or_0};
   60.66 +val xor_1 = @{thm xor_1};
   60.67 +val xor_0 = @{thm xor_0};
   60.68 +val not_type = @{thm not_type};
   60.69 +val and_type = @{thm and_type};
   60.70 +val or_type = @{thm or_type};
   60.71 +val xor_type = @{thm xor_type};
   60.72 +val bool_typechecks = @{thms bool_typechecks};
   60.73 +val not_not = @{thm not_not};
   60.74 +val not_and = @{thm not_and};
   60.75 +val not_or = @{thm not_or};
   60.76 +val and_absorb = @{thm and_absorb};
   60.77 +val and_commute = @{thm and_commute};
   60.78 +val and_assoc = @{thm and_assoc};
   60.79 +val and_or_distrib = @{thm and_or_distrib};
   60.80 +val or_absorb = @{thm or_absorb};
   60.81 +val or_commute = @{thm or_commute};
   60.82 +val or_assoc = @{thm or_assoc};
   60.83 +val or_and_distrib = @{thm or_and_distrib};
   60.84  *}
   60.85  
   60.86  end
    61.1 --- a/src/ZF/Cardinal.thy	Mon Sep 06 19:11:01 2010 +0200
    61.2 +++ b/src/ZF/Cardinal.thy	Mon Sep 06 19:13:10 2010 +0200
    61.3 @@ -1044,134 +1044,134 @@
    61.4  
    61.5  ML
    61.6  {*
    61.7 -val Least_def = thm "Least_def";
    61.8 -val eqpoll_def = thm "eqpoll_def";
    61.9 -val lepoll_def = thm "lepoll_def";
   61.10 -val lesspoll_def = thm "lesspoll_def";
   61.11 -val cardinal_def = thm "cardinal_def";
   61.12 -val Finite_def = thm "Finite_def";
   61.13 -val Card_def = thm "Card_def";
   61.14 -val eq_imp_not_mem = thm "eq_imp_not_mem";
   61.15 -val decomp_bnd_mono = thm "decomp_bnd_mono";
   61.16 -val Banach_last_equation = thm "Banach_last_equation";
   61.17 -val decomposition = thm "decomposition";
   61.18 -val schroeder_bernstein = thm "schroeder_bernstein";
   61.19 -val bij_imp_eqpoll = thm "bij_imp_eqpoll";
   61.20 -val eqpoll_refl = thm "eqpoll_refl";
   61.21 -val eqpoll_sym = thm "eqpoll_sym";
   61.22 -val eqpoll_trans = thm "eqpoll_trans";
   61.23 -val subset_imp_lepoll = thm "subset_imp_lepoll";
   61.24 -val lepoll_refl = thm "lepoll_refl";
   61.25 -val le_imp_lepoll = thm "le_imp_lepoll";
   61.26 -val eqpoll_imp_lepoll = thm "eqpoll_imp_lepoll";
   61.27 -val lepoll_trans = thm "lepoll_trans";
   61.28 -val eqpollI = thm "eqpollI";
   61.29 -val eqpollE = thm "eqpollE";
   61.30 -val eqpoll_iff = thm "eqpoll_iff";
   61.31 -val lepoll_0_is_0 = thm "lepoll_0_is_0";
   61.32 -val empty_lepollI = thm "empty_lepollI";
   61.33 -val lepoll_0_iff = thm "lepoll_0_iff";
   61.34 -val Un_lepoll_Un = thm "Un_lepoll_Un";
   61.35 -val eqpoll_0_is_0 = thm "eqpoll_0_is_0";
   61.36 -val eqpoll_0_iff = thm "eqpoll_0_iff";
   61.37 -val eqpoll_disjoint_Un = thm "eqpoll_disjoint_Un";
   61.38 -val lesspoll_not_refl = thm "lesspoll_not_refl";
   61.39 -val lesspoll_irrefl = thm "lesspoll_irrefl";
   61.40 -val lesspoll_imp_lepoll = thm "lesspoll_imp_lepoll";
   61.41 -val lepoll_well_ord = thm "lepoll_well_ord";
   61.42 -val lepoll_iff_leqpoll = thm "lepoll_iff_leqpoll";
   61.43 -val inj_not_surj_succ = thm "inj_not_surj_succ";
   61.44 -val lesspoll_trans = thm "lesspoll_trans";
   61.45 -val lesspoll_trans1 = thm "lesspoll_trans1";
   61.46 -val lesspoll_trans2 = thm "lesspoll_trans2";
   61.47 -val Least_equality = thm "Least_equality";
   61.48 -val LeastI = thm "LeastI";
   61.49 -val Least_le = thm "Least_le";
   61.50 -val less_LeastE = thm "less_LeastE";
   61.51 -val LeastI2 = thm "LeastI2";
   61.52 -val Least_0 = thm "Least_0";
   61.53 -val Ord_Least = thm "Ord_Least";
   61.54 -val Least_cong = thm "Least_cong";
   61.55 -val cardinal_cong = thm "cardinal_cong";
   61.56 -val well_ord_cardinal_eqpoll = thm "well_ord_cardinal_eqpoll";
   61.57 -val Ord_cardinal_eqpoll = thm "Ord_cardinal_eqpoll";
   61.58 -val well_ord_cardinal_eqE = thm "well_ord_cardinal_eqE";
   61.59 -val well_ord_cardinal_eqpoll_iff = thm "well_ord_cardinal_eqpoll_iff";
   61.60 -val Ord_cardinal_le = thm "Ord_cardinal_le";
   61.61 -val Card_cardinal_eq = thm "Card_cardinal_eq";
   61.62 -val CardI = thm "CardI";
   61.63 -val Card_is_Ord = thm "Card_is_Ord";
   61.64 -val Card_cardinal_le = thm "Card_cardinal_le";
   61.65 -val Ord_cardinal = thm "Ord_cardinal";
   61.66 -val Card_iff_initial = thm "Card_iff_initial";
   61.67 -val lt_Card_imp_lesspoll = thm "lt_Card_imp_lesspoll";
   61.68 -val Card_0 = thm "Card_0";
   61.69 -val Card_Un = thm "Card_Un";
   61.70 -val Card_cardinal = thm "Card_cardinal";
   61.71 -val cardinal_mono = thm "cardinal_mono";
   61.72 -val cardinal_lt_imp_lt = thm "cardinal_lt_imp_lt";
   61.73 -val Card_lt_imp_lt = thm "Card_lt_imp_lt";
   61.74 -val Card_lt_iff = thm "Card_lt_iff";
   61.75 -val Card_le_iff = thm "Card_le_iff";
   61.76 -val well_ord_lepoll_imp_Card_le = thm "well_ord_lepoll_imp_Card_le";
   61.77 -val lepoll_cardinal_le = thm "lepoll_cardinal_le";
   61.78 -val lepoll_Ord_imp_eqpoll = thm "lepoll_Ord_imp_eqpoll";
   61.79 -val lesspoll_imp_eqpoll = thm "lesspoll_imp_eqpoll";
   61.80 -val cardinal_subset_Ord = thm "cardinal_subset_Ord";
   61.81 -val cons_lepoll_consD = thm "cons_lepoll_consD";
   61.82 -val cons_eqpoll_consD = thm "cons_eqpoll_consD";
   61.83 -val succ_lepoll_succD = thm "succ_lepoll_succD";
   61.84 -val nat_lepoll_imp_le = thm "nat_lepoll_imp_le";
   61.85 -val nat_eqpoll_iff = thm "nat_eqpoll_iff";
   61.86 -val nat_into_Card = thm "nat_into_Card";
   61.87 -val cardinal_0 = thm "cardinal_0";
   61.88 -val cardinal_1 = thm "cardinal_1";
   61.89 -val succ_lepoll_natE = thm "succ_lepoll_natE";
   61.90 -val n_lesspoll_nat = thm "n_lesspoll_nat";
   61.91 -val nat_lepoll_imp_ex_eqpoll_n = thm "nat_lepoll_imp_ex_eqpoll_n";
   61.92 -val lepoll_imp_lesspoll_succ = thm "lepoll_imp_lesspoll_succ";
   61.93 -val lesspoll_succ_imp_lepoll = thm "lesspoll_succ_imp_lepoll";
   61.94 -val lesspoll_succ_iff = thm "lesspoll_succ_iff";
   61.95 -val lepoll_succ_disj = thm "lepoll_succ_disj";
   61.96 -val lesspoll_cardinal_lt = thm "lesspoll_cardinal_lt";
   61.97 -val lt_not_lepoll = thm "lt_not_lepoll";
   61.98 -val Ord_nat_eqpoll_iff = thm "Ord_nat_eqpoll_iff";
   61.99 -val Card_nat = thm "Card_nat";
  61.100 -val nat_le_cardinal = thm "nat_le_cardinal";
  61.101 -val cons_lepoll_cong = thm "cons_lepoll_cong";
  61.102 -val cons_eqpoll_cong = thm "cons_eqpoll_cong";
  61.103 -val cons_lepoll_cons_iff = thm "cons_lepoll_cons_iff";
  61.104 -val cons_eqpoll_cons_iff = thm "cons_eqpoll_cons_iff";
  61.105 -val singleton_eqpoll_1 = thm "singleton_eqpoll_1";
  61.106 -val cardinal_singleton = thm "cardinal_singleton";
  61.107 -val not_0_is_lepoll_1 = thm "not_0_is_lepoll_1";
  61.108 -val succ_eqpoll_cong = thm "succ_eqpoll_cong";
  61.109 -val sum_eqpoll_cong = thm "sum_eqpoll_cong";
  61.110 -val prod_eqpoll_cong = thm "prod_eqpoll_cong";
  61.111 -val inj_disjoint_eqpoll = thm "inj_disjoint_eqpoll";
  61.112 -val Diff_sing_lepoll = thm "Diff_sing_lepoll";
  61.113 -val lepoll_Diff_sing = thm "lepoll_Diff_sing";
  61.114 -val Diff_sing_eqpoll = thm "Diff_sing_eqpoll";
  61.115 -val lepoll_1_is_sing = thm "lepoll_1_is_sing";
  61.116 -val Un_lepoll_sum = thm "Un_lepoll_sum";
  61.117 -val well_ord_Un = thm "well_ord_Un";
  61.118 -val disj_Un_eqpoll_sum = thm "disj_Un_eqpoll_sum";
  61.119 -val Finite_0 = thm "Finite_0";
  61.120 -val lepoll_nat_imp_Finite = thm "lepoll_nat_imp_Finite";
  61.121 -val lesspoll_nat_is_Finite = thm "lesspoll_nat_is_Finite";
  61.122 -val lepoll_Finite = thm "lepoll_Finite";
  61.123 -val subset_Finite = thm "subset_Finite";
  61.124 -val Finite_Diff = thm "Finite_Diff";
  61.125 -val Finite_cons = thm "Finite_cons";
  61.126 -val Finite_succ = thm "Finite_succ";
  61.127 -val nat_le_infinite_Ord = thm "nat_le_infinite_Ord";
  61.128 -val Finite_imp_well_ord = thm "Finite_imp_well_ord";
  61.129 -val nat_wf_on_converse_Memrel = thm "nat_wf_on_converse_Memrel";
  61.130 -val nat_well_ord_converse_Memrel = thm "nat_well_ord_converse_Memrel";
  61.131 -val well_ord_converse = thm "well_ord_converse";
  61.132 -val ordertype_eq_n = thm "ordertype_eq_n";
  61.133 -val Finite_well_ord_converse = thm "Finite_well_ord_converse";
  61.134 -val nat_into_Finite = thm "nat_into_Finite";
  61.135 +val Least_def = @{thm Least_def};
  61.136 +val eqpoll_def = @{thm eqpoll_def};
  61.137 +val lepoll_def = @{thm lepoll_def};
  61.138 +val lesspoll_def = @{thm lesspoll_def};
  61.139 +val cardinal_def = @{thm cardinal_def};
  61.140 +val Finite_def = @{thm Finite_def};
  61.141 +val Card_def = @{thm Card_def};
  61.142 +val eq_imp_not_mem = @{thm eq_imp_not_mem};
  61.143 +val decomp_bnd_mono = @{thm decomp_bnd_mono};
  61.144 +val Banach_last_equation = @{thm Banach_last_equation};
  61.145 +val decomposition = @{thm decomposition};
  61.146 +val schroeder_bernstein = @{thm schroeder_bernstein};
  61.147 +val bij_imp_eqpoll = @{thm bij_imp_eqpoll};
  61.148 +val eqpoll_refl = @{thm eqpoll_refl};
  61.149 +val eqpoll_sym = @{thm eqpoll_sym};
  61.150 +val eqpoll_trans = @{thm eqpoll_trans};
  61.151 +val subset_imp_lepoll = @{thm subset_imp_lepoll};
  61.152 +val lepoll_refl = @{thm lepoll_refl};
  61.153 +val le_imp_lepoll = @{thm le_imp_lepoll};
  61.154 +val eqpoll_imp_lepoll = @{thm eqpoll_imp_lepoll};
  61.155 +val lepoll_trans = @{thm lepoll_trans};
  61.156 +val eqpollI = @{thm eqpollI};
  61.157 +val eqpollE = @{thm eqpollE};
  61.158 +val eqpoll_iff = @{thm eqpoll_iff};
  61.159 +val lepoll_0_is_0 = @{thm lepoll_0_is_0};
  61.160 +val empty_lepollI = @{thm empty_lepollI};
  61.161 +val lepoll_0_iff = @{thm lepoll_0_iff};
  61.162 +val Un_lepoll_Un = @{thm Un_lepoll_Un};
  61.163 +val eqpoll_0_is_0 = @{thm eqpoll_0_is_0};
  61.164 +val eqpoll_0_iff = @{thm eqpoll_0_iff};
  61.165 +val eqpoll_disjoint_Un = @{thm eqpoll_disjoint_Un};
  61.166 +val lesspoll_not_refl = @{thm lesspoll_not_refl};
  61.167 +val lesspoll_irrefl = @{thm lesspoll_irrefl};
  61.168 +val lesspoll_imp_lepoll = @{thm lesspoll_imp_lepoll};
  61.169 +val lepoll_well_ord = @{thm lepoll_well_ord};
  61.170 +val lepoll_iff_leqpoll = @{thm lepoll_iff_leqpoll};
  61.171 +val inj_not_surj_succ = @{thm inj_not_surj_succ};
  61.172 +val lesspoll_trans = @{thm lesspoll_trans};
  61.173 +val lesspoll_trans1 = @{thm lesspoll_trans1};
  61.174 +val lesspoll_trans2 = @{thm lesspoll_trans2};
  61.175 +val Least_equality = @{thm Least_equality};
  61.176 +val LeastI = @{thm LeastI};
  61.177 +val Least_le = @{thm Least_le};
  61.178 +val less_LeastE = @{thm less_LeastE};
  61.179 +val LeastI2 = @{thm LeastI2};
  61.180 +val Least_0 = @{thm Least_0};
  61.181 +val Ord_Least = @{thm Ord_Least};
  61.182 +val Least_cong = @{thm Least_cong};
  61.183 +val cardinal_cong = @{thm cardinal_cong};
  61.184 +val well_ord_cardinal_eqpoll = @{thm well_ord_cardinal_eqpoll};
  61.185 +val Ord_cardinal_eqpoll = @{thm Ord_cardinal_eqpoll};
  61.186 +val well_ord_cardinal_eqE = @{thm well_ord_cardinal_eqE};
  61.187 +val well_ord_cardinal_eqpoll_iff = @{thm well_ord_cardinal_eqpoll_iff};
  61.188 +val Ord_cardinal_le = @{thm Ord_cardinal_le};
  61.189 +val Card_cardinal_eq = @{thm Card_cardinal_eq};
  61.190 +val CardI = @{thm CardI};
  61.191 +val Card_is_Ord = @{thm Card_is_Ord};
  61.192 +val Card_cardinal_le = @{thm Card_cardinal_le};
  61.193 +val Ord_cardinal = @{thm Ord_cardinal};
  61.194 +val Card_iff_initial = @{thm Card_iff_initial};
  61.195 +val lt_Card_imp_lesspoll = @{thm lt_Card_imp_lesspoll};
  61.196 +val Card_0 = @{thm Card_0};
  61.197 +val Card_Un = @{thm Card_Un};
  61.198 +val Card_cardinal = @{thm Card_cardinal};
  61.199 +val cardinal_mono = @{thm cardinal_mono};
  61.200 +val cardinal_lt_imp_lt = @{thm cardinal_lt_imp_lt};
  61.201 +val Card_lt_imp_lt = @{thm Card_lt_imp_lt};
  61.202 +val Card_lt_iff = @{thm Card_lt_iff};
  61.203 +val Card_le_iff = @{thm Card_le_iff};
  61.204 +val well_ord_lepoll_imp_Card_le = @{thm well_ord_lepoll_imp_Card_le};
  61.205 +val lepoll_cardinal_le = @{thm lepoll_cardinal_le};
  61.206 +val lepoll_Ord_imp_eqpoll = @{thm lepoll_Ord_imp_eqpoll};
  61.207 +val lesspoll_imp_eqpoll = @{thm lesspoll_imp_eqpoll};
  61.208 +val cardinal_subset_Ord = @{thm cardinal_subset_Ord};
  61.209 +val cons_lepoll_consD = @{thm cons_lepoll_consD};
  61.210 +val cons_eqpoll_consD = @{thm cons_eqpoll_consD};
  61.211 +val succ_lepoll_succD = @{thm succ_lepoll_succD};
  61.212 +val nat_lepoll_imp_le = @{thm nat_lepoll_imp_le};
  61.213 +val nat_eqpoll_iff = @{thm nat_eqpoll_iff};
  61.214 +val nat_into_Card = @{thm nat_into_Card};
  61.215 +val cardinal_0 = @{thm cardinal_0};
  61.216 +val cardinal_1 = @{thm cardinal_1};
  61.217 +val succ_lepoll_natE = @{thm succ_lepoll_natE};
  61.218 +val n_lesspoll_nat = @{thm n_lesspoll_nat};
  61.219 +val nat_lepoll_imp_ex_eqpoll_n = @{thm nat_lepoll_imp_ex_eqpoll_n};
  61.220 +val lepoll_imp_lesspoll_succ = @{thm lepoll_imp_lesspoll_succ};
  61.221 +val lesspoll_succ_imp_lepoll = @{thm lesspoll_succ_imp_lepoll};
  61.222 +val lesspoll_succ_iff = @{thm lesspoll_succ_iff};
  61.223 +val lepoll_succ_disj = @{thm lepoll_succ_disj};
  61.224 +val lesspoll_cardinal_lt = @{thm lesspoll_cardinal_lt};
  61.225 +val lt_not_lepoll = @{thm lt_not_lepoll};
  61.226 +val Ord_nat_eqpoll_iff = @{thm Ord_nat_eqpoll_iff};
  61.227 +val Card_nat = @{thm Card_nat};
  61.228 +val nat_le_cardinal = @{thm nat_le_cardinal};
  61.229 +val cons_lepoll_cong = @{thm cons_lepoll_cong};
  61.230 +val cons_eqpoll_cong = @{thm cons_eqpoll_cong};
  61.231 +val cons_lepoll_cons_iff = @{thm cons_lepoll_cons_iff};
  61.232 +val cons_eqpoll_cons_iff = @{thm cons_eqpoll_cons_iff};
  61.233 +val singleton_eqpoll_1 = @{thm singleton_eqpoll_1};
  61.234 +val cardinal_singleton = @{thm cardinal_singleton};
  61.235 +val not_0_is_lepoll_1 = @{thm not_0_is_lepoll_1};
  61.236 +val succ_eqpoll_cong = @{thm succ_eqpoll_cong};
  61.237 +val sum_eqpoll_cong = @{thm sum_eqpoll_cong};
  61.238 +val prod_eqpoll_cong = @{thm prod_eqpoll_cong};
  61.239 +val inj_disjoint_eqpoll = @{thm inj_disjoint_eqpoll};
  61.240 +val Diff_sing_lepoll = @{thm Diff_sing_lepoll};
  61.241 +val lepoll_Diff_sing = @{thm lepoll_Diff_sing};
  61.242 +val Diff_sing_eqpoll = @{thm Diff_sing_eqpoll};
  61.243 +val lepoll_1_is_sing = @{thm lepoll_1_is_sing};
  61.244 +val Un_lepoll_sum = @{thm Un_lepoll_sum};
  61.245 +val well_ord_Un = @{thm well_ord_Un};
  61.246 +val disj_Un_eqpoll_sum = @{thm disj_Un_eqpoll_sum};
  61.247 +val Finite_0 = @{thm Finite_0};
  61.248 +val lepoll_nat_imp_Finite = @{thm lepoll_nat_imp_Finite};
  61.249 +val lesspoll_nat_is_Finite = @{thm lesspoll_nat_is_Finite};
  61.250 +val lepoll_Finite = @{thm lepoll_Finite};
  61.251 +val subset_Finite = @{thm subset_Finite};
  61.252 +val Finite_Diff = @{thm Finite_Diff};
  61.253 +val Finite_cons = @{thm Finite_cons};
  61.254 +val Finite_succ = @{thm Finite_succ};
  61.255 +val nat_le_infinite_Ord = @{thm nat_le_infinite_Ord};
  61.256 +val Finite_imp_well_ord = @{thm Finite_imp_well_ord};
  61.257 +val nat_wf_on_converse_Memrel = @{thm nat_wf_on_converse_Memrel};
  61.258 +val nat_well_ord_converse_Memrel = @{thm nat_well_ord_converse_Memrel};
  61.259 +val well_ord_converse = @{thm well_ord_converse};
  61.260 +val ordertype_eq_n = @{thm ordertype_eq_n};
  61.261 +val Finite_well_ord_converse = @{thm Finite_well_ord_converse};
  61.262 +val nat_into_Finite = @{thm nat_into_Finite};
  61.263  *}
  61.264  
  61.265  end
    62.1 --- a/src/ZF/CardinalArith.thy	Mon Sep 06 19:11:01 2010 +0200
    62.2 +++ b/src/ZF/CardinalArith.thy	Mon Sep 06 19:13:10 2010 +0200
    62.3 @@ -911,89 +911,89 @@
    62.4  
    62.5  
    62.6  ML{*
    62.7 -val InfCard_def = thm "InfCard_def"
    62.8 -val cmult_def = thm "cmult_def"
    62.9 -val cadd_def = thm "cadd_def"
   62.10 -val jump_cardinal_def = thm "jump_cardinal_def"
   62.11 -val csucc_def = thm "csucc_def"
   62.12 +val InfCard_def = @{thm InfCard_def};
   62.13 +val cmult_def = @{thm cmult_def};
   62.14 +val cadd_def = @{thm cadd_def};
   62.15 +val jump_cardinal_def = @{thm jump_cardinal_def};
   62.16 +val csucc_def = @{thm csucc_def};
   62.17  
   62.18 -val sum_commute_eqpoll = thm "sum_commute_eqpoll";
   62.19 -val cadd_commute = thm "cadd_commute";
   62.20 -val sum_assoc_eqpoll = thm "sum_assoc_eqpoll";
   62.21 -val well_ord_cadd_assoc = thm "well_ord_cadd_assoc";
   62.22 -val sum_0_eqpoll = thm "sum_0_eqpoll";
   62.23 -val cadd_0 = thm "cadd_0";
   62.24 -val sum_lepoll_self = thm "sum_lepoll_self";
   62.25 -val cadd_le_self = thm "cadd_le_self";
   62.26 -val sum_lepoll_mono = thm "sum_lepoll_mono";
   62.27 -val cadd_le_mono = thm "cadd_le_mono";
   62.28 -val eq_imp_not_mem = thm "eq_imp_not_mem";
   62.29 -val sum_succ_eqpoll = thm "sum_succ_eqpoll";
   62.30 -val nat_cadd_eq_add = thm "nat_cadd_eq_add";
   62.31 -val prod_commute_eqpoll = thm "prod_commute_eqpoll";
   62.32 -val cmult_commute = thm "cmult_commute";
   62.33 -val prod_assoc_eqpoll = thm "prod_assoc_eqpoll";
   62.34 -val well_ord_cmult_assoc = thm "well_ord_cmult_assoc";
   62.35 -val sum_prod_distrib_eqpoll = thm "sum_prod_distrib_eqpoll";
   62.36 -val well_ord_cadd_cmult_distrib = thm "well_ord_cadd_cmult_distrib";
   62.37 -val prod_0_eqpoll = thm "prod_0_eqpoll";
   62.38 -val cmult_0 = thm "cmult_0";
   62.39 -val prod_singleton_eqpoll = thm "prod_singleton_eqpoll";
   62.40 -val cmult_1 = thm "cmult_1";
   62.41 -val prod_lepoll_self = thm "prod_lepoll_self";
   62.42 -val cmult_le_self = thm "cmult_le_self";
   62.43 -val prod_lepoll_mono = thm "prod_lepoll_mono";
   62.44 -val cmult_le_mono = thm "cmult_le_mono";
   62.45 -val prod_succ_eqpoll = thm "prod_succ_eqpoll";
   62.46 -val nat_cmult_eq_mult = thm "nat_cmult_eq_mult";
   62.47 -val cmult_2 = thm "cmult_2";
   62.48 -val sum_lepoll_prod = thm "sum_lepoll_prod";
   62.49 -val lepoll_imp_sum_lepoll_prod = thm "lepoll_imp_sum_lepoll_prod";
   62.50 -val nat_cons_lepoll = thm "nat_cons_lepoll";
   62.51 -val nat_cons_eqpoll = thm "nat_cons_eqpoll";
   62.52 -val nat_succ_eqpoll = thm "nat_succ_eqpoll";
   62.53 -val InfCard_nat = thm "InfCard_nat";
   62.54 -val InfCard_is_Card = thm "InfCard_is_Card";
   62.55 -val InfCard_Un = thm "InfCard_Un";
   62.56 -val InfCard_is_Limit = thm "InfCard_is_Limit";
   62.57 -val ordermap_eqpoll_pred = thm "ordermap_eqpoll_pred";
   62.58 -val ordermap_z_lt = thm "ordermap_z_lt";
   62.59 -val InfCard_le_cmult_eq = thm "InfCard_le_cmult_eq";
   62.60 -val InfCard_cmult_eq = thm "InfCard_cmult_eq";
   62.61 -val InfCard_cdouble_eq = thm "InfCard_cdouble_eq";
   62.62 -val InfCard_le_cadd_eq = thm "InfCard_le_cadd_eq";
   62.63 -val InfCard_cadd_eq = thm "InfCard_cadd_eq";
   62.64 -val Ord_jump_cardinal = thm "Ord_jump_cardinal";
   62.65 -val jump_cardinal_iff = thm "jump_cardinal_iff";
   62.66 -val K_lt_jump_cardinal = thm "K_lt_jump_cardinal";
   62.67 -val Card_jump_cardinal = thm "Card_jump_cardinal";
   62.68 -val csucc_basic = thm "csucc_basic";
   62.69 -val Card_csucc = thm "Card_csucc";
   62.70 -val lt_csucc = thm "lt_csucc";
   62.71 -val Ord_0_lt_csucc = thm "Ord_0_lt_csucc";
   62.72 -val csucc_le = thm "csucc_le";
   62.73 -val lt_csucc_iff = thm "lt_csucc_iff";
   62.74 -val Card_lt_csucc_iff = thm "Card_lt_csucc_iff";
   62.75 -val InfCard_csucc = thm "InfCard_csucc";
   62.76 -val Finite_into_Fin = thm "Finite_into_Fin";
   62.77 -val Fin_into_Finite = thm "Fin_into_Finite";
   62.78 -val Finite_Fin_iff = thm "Finite_Fin_iff";
   62.79 -val Finite_Un = thm "Finite_Un";
   62.80 -val Finite_Union = thm "Finite_Union";
   62.81 -val Finite_induct = thm "Finite_induct";
   62.82 -val Fin_imp_not_cons_lepoll = thm "Fin_imp_not_cons_lepoll";
   62.83 -val Finite_imp_cardinal_cons = thm "Finite_imp_cardinal_cons";
   62.84 -val Finite_imp_succ_cardinal_Diff = thm "Finite_imp_succ_cardinal_Diff";
   62.85 -val Finite_imp_cardinal_Diff = thm "Finite_imp_cardinal_Diff";
   62.86 -val nat_implies_well_ord = thm "nat_implies_well_ord";
   62.87 -val nat_sum_eqpoll_sum = thm "nat_sum_eqpoll_sum";
   62.88 -val Diff_sing_Finite = thm "Diff_sing_Finite";
   62.89 -val Diff_Finite = thm "Diff_Finite";
   62.90 -val Ord_subset_natD = thm "Ord_subset_natD";
   62.91 -val Ord_nat_subset_into_Card = thm "Ord_nat_subset_into_Card";
   62.92 -val Finite_cardinal_in_nat = thm "Finite_cardinal_in_nat";
   62.93 -val Finite_Diff_sing_eq_diff_1 = thm "Finite_Diff_sing_eq_diff_1";
   62.94 -val cardinal_lt_imp_Diff_not_0 = thm "cardinal_lt_imp_Diff_not_0";
   62.95 +val sum_commute_eqpoll = @{thm sum_commute_eqpoll};
   62.96 +val cadd_commute = @{thm cadd_commute};
   62.97 +val sum_assoc_eqpoll = @{thm sum_assoc_eqpoll};
   62.98 +val well_ord_cadd_assoc = @{thm well_ord_cadd_assoc};
   62.99 +val sum_0_eqpoll = @{thm sum_0_eqpoll};
  62.100 +val cadd_0 = @{thm cadd_0};
  62.101 +val sum_lepoll_self = @{thm sum_lepoll_self};
  62.102 +val cadd_le_self = @{thm cadd_le_self};
  62.103 +val sum_lepoll_mono = @{thm sum_lepoll_mono};
  62.104 +val cadd_le_mono = @{thm cadd_le_mono};
  62.105 +val eq_imp_not_mem = @{thm eq_imp_not_mem};
  62.106 +val sum_succ_eqpoll = @{thm sum_succ_eqpoll};
  62.107 +val nat_cadd_eq_add = @{thm nat_cadd_eq_add};
  62.108 +val prod_commute_eqpoll = @{thm prod_commute_eqpoll};
  62.109 +val cmult_commute = @{thm cmult_commute};
  62.110 +val prod_assoc_eqpoll = @{thm prod_assoc_eqpoll};
  62.111 +val well_ord_cmult_assoc = @{thm well_ord_cmult_assoc};
  62.112 +val sum_prod_distrib_eqpoll = @{thm sum_prod_distrib_eqpoll};
  62.113 +val well_ord_cadd_cmult_distrib = @{thm well_ord_cadd_cmult_distrib};
  62.114 +val prod_0_eqpoll = @{thm prod_0_eqpoll};
  62.115 +val cmult_0 = @{thm cmult_0};
  62.116 +val prod_singleton_eqpoll = @{thm prod_singleton_eqpoll};
  62.117 +val cmult_1 = @{thm cmult_1};
  62.118 +val prod_lepoll_self = @{thm prod_lepoll_self};
  62.119 +val cmult_le_self = @{thm cmult_le_self};
  62.120 +val prod_lepoll_mono = @{thm prod_lepoll_mono};
  62.121 +val cmult_le_mono = @{thm cmult_le_mono};
  62.122 +val prod_succ_eqpoll = @{thm prod_succ_eqpoll};
  62.123 +val nat_cmult_eq_mult = @{thm nat_cmult_eq_mult};
  62.124 +val cmult_2 = @{thm cmult_2};
  62.125 +val sum_lepoll_prod = @{thm sum_lepoll_prod};
  62.126 +val lepoll_imp_sum_lepoll_prod = @{thm lepoll_imp_sum_lepoll_prod};
  62.127 +val nat_cons_lepoll = @{thm nat_cons_lepoll};
  62.128 +val nat_cons_eqpoll = @{thm nat_cons_eqpoll};
  62.129 +val nat_succ_eqpoll = @{thm nat_succ_eqpoll};
  62.130 +val InfCard_nat = @{thm InfCard_nat};
  62.131 +val InfCard_is_Card = @{thm InfCard_is_Card};
  62.132 +val InfCard_Un = @{thm InfCard_Un};
  62.133 +val InfCard_is_Limit = @{thm InfCard_is_Limit};
  62.134 +val ordermap_eqpoll_pred = @{thm ordermap_eqpoll_pred};
  62.135 +val ordermap_z_lt = @{thm ordermap_z_lt};
  62.136 +val InfCard_le_cmult_eq = @{thm InfCard_le_cmult_eq};
  62.137 +val InfCard_cmult_eq = @{thm InfCard_cmult_eq};
  62.138 +val InfCard_cdouble_eq = @{thm InfCard_cdouble_eq};
  62.139 +val InfCard_le_cadd_eq = @{thm InfCard_le_cadd_eq};
  62.140 +val InfCard_cadd_eq = @{thm InfCard_cadd_eq};
  62.141 +val Ord_jump_cardinal = @{thm Ord_jump_cardinal};
  62.142 +val jump_cardinal_iff = @{thm jump_cardinal_iff};
  62.143 +val K_lt_jump_cardinal = @{thm K_lt_jump_cardinal};
  62.144 +val Card_jump_cardinal = @{thm Card_jump_cardinal};
  62.145 +val csucc_basic = @{thm csucc_basic};
  62.146 +val Card_csucc = @{thm Card_csucc};
  62.147 +val lt_csucc = @{thm lt_csucc};
  62.148 +val Ord_0_lt_csucc = @{thm Ord_0_lt_csucc};
  62.149 +val csucc_le = @{thm csucc_le};
  62.150 +val lt_csucc_iff = @{thm lt_csucc_iff};
  62.151 +val Card_lt_csucc_iff = @{thm Card_lt_csucc_iff};
  62.152 +val InfCard_csucc = @{thm InfCard_csucc};
  62.153 +val Finite_into_Fin = @{thm Finite_into_Fin};
  62.154 +val Fin_into_Finite = @{thm Fin_into_Finite};
  62.155 +val Finite_Fin_iff = @{thm Finite_Fin_iff};
  62.156 +val Finite_Un = @{thm Finite_Un};
  62.157 +val Finite_Union = @{thm Finite_Union};
  62.158 +val Finite_induct = @{thm Finite_induct};
  62.159 +val Fin_imp_not_cons_lepoll = @{thm Fin_imp_not_cons_lepoll};
  62.160 +val Finite_imp_cardinal_cons = @{thm Finite_imp_cardinal_cons};
  62.161 +val Finite_imp_succ_cardinal_Diff = @{thm Finite_imp_succ_cardinal_Diff};
  62.162 +val Finite_imp_cardinal_Diff = @{thm Finite_imp_cardinal_Diff};
  62.163 +val nat_implies_well_ord = @{thm nat_implies_well_ord};
  62.164 +val nat_sum_eqpoll_sum = @{thm nat_sum_eqpoll_sum};
  62.165 +val Diff_sing_Finite = @{thm Diff_sing_Finite};
  62.166 +val Diff_Finite = @{thm Diff_Finite};
  62.167 +val Ord_subset_natD = @{thm Ord_subset_natD};
  62.168 +val Ord_nat_subset_into_Card = @{thm Ord_nat_subset_into_Card};
  62.169 +val Finite_cardinal_in_nat = @{thm Finite_cardinal_in_nat};
  62.170 +val Finite_Diff_sing_eq_diff_1 = @{thm Finite_Diff_sing_eq_diff_1};
  62.171 +val cardinal_lt_imp_Diff_not_0 = @{thm cardinal_lt_imp_Diff_not_0};
  62.172  *}
  62.173  
  62.174  end
    63.1 --- a/src/ZF/Cardinal_AC.thy	Mon Sep 06 19:11:01 2010 +0200
    63.2 +++ b/src/ZF/Cardinal_AC.thy	Mon Sep 06 19:13:10 2010 +0200
    63.3 @@ -193,8 +193,8 @@
    63.4  
    63.5  ML
    63.6  {*
    63.7 -val cardinal_0_iff_0 = thm "cardinal_0_iff_0";
    63.8 -val cardinal_lt_iff_lesspoll = thm "cardinal_lt_iff_lesspoll";
    63.9 +val cardinal_0_iff_0 = @{thm cardinal_0_iff_0};
   63.10 +val cardinal_lt_iff_lesspoll = @{thm cardinal_lt_iff_lesspoll};
   63.11  *}
   63.12  
   63.13  end
    64.1 --- a/src/ZF/Epsilon.thy	Mon Sep 06 19:11:01 2010 +0200
    64.2 +++ b/src/ZF/Epsilon.thy	Mon Sep 06 19:13:10 2010 +0200
    64.3 @@ -398,56 +398,56 @@
    64.4  
    64.5  ML
    64.6  {*
    64.7 -val arg_subset_eclose = thm "arg_subset_eclose";
    64.8 -val arg_into_eclose = thm "arg_into_eclose";
    64.9 -val Transset_eclose = thm "Transset_eclose";
   64.10 -val eclose_subset = thm "eclose_subset";
   64.11 -val ecloseD = thm "ecloseD";
   64.12 -val arg_in_eclose_sing = thm "arg_in_eclose_sing";
   64.13 -val arg_into_eclose_sing = thm "arg_into_eclose_sing";
   64.14 -val eclose_induct = thm "eclose_induct";
   64.15 -val eps_induct = thm "eps_induct";
   64.16 -val eclose_least = thm "eclose_least";
   64.17 -val eclose_induct_down = thm "eclose_induct_down";
   64.18 -val Transset_eclose_eq_arg = thm "Transset_eclose_eq_arg";
   64.19 -val mem_eclose_trans = thm "mem_eclose_trans";
   64.20 -val mem_eclose_sing_trans = thm "mem_eclose_sing_trans";
   64.21 -val under_Memrel = thm "under_Memrel";
   64.22 -val under_Memrel_eclose = thm "under_Memrel_eclose";
   64.23 -val wfrec_ssubst = thm "wfrec_ssubst";
   64.24 -val wfrec_eclose_eq = thm "wfrec_eclose_eq";
   64.25 -val wfrec_eclose_eq2 = thm "wfrec_eclose_eq2";
   64.26 -val transrec = thm "transrec";
   64.27 -val def_transrec = thm "def_transrec";
   64.28 -val transrec_type = thm "transrec_type";
   64.29 -val eclose_sing_Ord = thm "eclose_sing_Ord";
   64.30 -val Ord_transrec_type = thm "Ord_transrec_type";
   64.31 -val rank = thm "rank";
   64.32 -val Ord_rank = thm "Ord_rank";
   64.33 -val rank_of_Ord = thm "rank_of_Ord";
   64.34 -val rank_lt = thm "rank_lt";
   64.35 -val eclose_rank_lt = thm "eclose_rank_lt";
   64.36 -val rank_mono = thm "rank_mono";
   64.37 -val rank_Pow = thm "rank_Pow";
   64.38 -val rank_0 = thm "rank_0";
   64.39 -val rank_succ = thm "rank_succ";
   64.40 -val rank_Union = thm "rank_Union";
   64.41 -val rank_eclose = thm "rank_eclose";
   64.42 -val rank_pair1 = thm "rank_pair1";
   64.43 -val rank_pair2 = thm "rank_pair2";
   64.44 -val the_equality_if = thm "the_equality_if";
   64.45 -val rank_apply = thm "rank_apply";
   64.46 -val mem_eclose_subset = thm "mem_eclose_subset";
   64.47 -val eclose_mono = thm "eclose_mono";
   64.48 -val eclose_idem = thm "eclose_idem";
   64.49 -val transrec2_0 = thm "transrec2_0";
   64.50 -val transrec2_succ = thm "transrec2_succ";
   64.51 -val transrec2_Limit = thm "transrec2_Limit";
   64.52 -val recursor_0 = thm "recursor_0";
   64.53 -val recursor_succ = thm "recursor_succ";
   64.54 -val rec_0 = thm "rec_0";
   64.55 -val rec_succ = thm "rec_succ";
   64.56 -val rec_type = thm "rec_type";
   64.57 +val arg_subset_eclose = @{thm arg_subset_eclose};
   64.58 +val arg_into_eclose = @{thm arg_into_eclose};
   64.59 +val Transset_eclose = @{thm Transset_eclose};
   64.60 +val eclose_subset = @{thm eclose_subset};
   64.61 +val ecloseD = @{thm ecloseD};
   64.62 +val arg_in_eclose_sing = @{thm arg_in_eclose_sing};
   64.63 +val arg_into_eclose_sing = @{thm arg_into_eclose_sing};
   64.64 +val eclose_induct = @{thm eclose_induct};
   64.65 +val eps_induct = @{thm eps_induct};
   64.66 +val eclose_least = @{thm eclose_least};
   64.67 +val eclose_induct_down = @{thm eclose_induct_down};
   64.68 +val Transset_eclose_eq_arg = @{thm Transset_eclose_eq_arg};
   64.69 +val mem_eclose_trans = @{thm mem_eclose_trans};
   64.70 +val mem_eclose_sing_trans = @{thm mem_eclose_sing_trans};
   64.71 +val under_Memrel = @{thm under_Memrel};
   64.72 +val under_Memrel_eclose = @{thm under_Memrel_eclose};
   64.73 +val wfrec_ssubst = @{thm wfrec_ssubst};
   64.74 +val wfrec_eclose_eq = @{thm wfrec_eclose_eq};
   64.75 +val wfrec_eclose_eq2 = @{thm wfrec_eclose_eq2};
   64.76 +val transrec = @{thm transrec};
   64.77 +val def_transrec = @{thm def_transrec};
   64.78 +val transrec_type = @{thm transrec_type};
   64.79 +val eclose_sing_Ord = @{thm eclose_sing_Ord};
   64.80 +val Ord_transrec_type = @{thm Ord_transrec_type};
   64.81 +val rank = @{thm rank};
   64.82 +val Ord_rank = @{thm Ord_rank};
   64.83 +val rank_of_Ord = @{thm rank_of_Ord};
   64.84 +val rank_lt = @{thm rank_lt};
   64.85 +val eclose_rank_lt = @{thm eclose_rank_lt};
   64.86 +val rank_mono = @{thm rank_mono};
   64.87 +val rank_Pow = @{thm rank_Pow};
   64.88 +val rank_0 = @{thm rank_0};
   64.89 +val rank_succ = @{thm rank_succ};
   64.90 +val rank_Union = @{thm rank_Union};
   64.91 +val rank_eclose = @{thm rank_eclose};
   64.92 +val rank_pair1 = @{thm rank_pair1};
   64.93 +val rank_pair2 = @{thm rank_pair2};
   64.94 +val the_equality_if = @{thm the_equality_if};
   64.95 +val rank_apply = @{thm rank_apply};
   64.96 +val mem_eclose_subset = @{thm mem_eclose_subset};
   64.97 +val eclose_mono = @{thm eclose_mono};
   64.98 +val eclose_idem = @{thm eclose_idem};
   64.99 +val transrec2_0 = @{thm transrec2_0};
  64.100 +val transrec2_succ = @{thm transrec2_succ};
  64.101 +val transrec2_Limit = @{thm transrec2_Limit};
  64.102 +val recursor_0 = @{thm recursor_0};
  64.103 +val recursor_succ = @{thm recursor_succ};
  64.104 +val rec_0 = @{thm rec_0};
  64.105 +val rec_succ = @{thm rec_succ};
  64.106 +val rec_type = @{thm rec_type};
  64.107  *}
  64.108  
  64.109  end