simplified/unified method_setup/attribute_setup;
authorwenzelm
Sun May 15 17:45:53 2011 +0200 (2011-05-15)
changeset 428145af15f1e2ef6
parent 42813 6c841fa92fa2
child 42815 61668e617a3b
simplified/unified method_setup/attribute_setup;
src/CCL/CCL.thy
src/CCL/Term.thy
src/CCL/Type.thy
src/Cube/Example.thy
src/FOL/FOL.thy
src/HOL/Algebra/abstract/Ring2.thy
src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
src/HOL/HOLCF/IOA/meta_theory/Abstraction.thy
src/HOL/HOLCF/Lift.thy
src/HOL/Library/Reflection.thy
src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy
src/HOL/Multivariate_Analysis/Euclidean_Space.thy
src/HOL/Prolog/HOHH.thy
src/HOL/Quotient.thy
src/HOL/SET_Protocol/Cardholder_Registration.thy
src/HOL/SET_Protocol/Purchase.thy
src/HOL/TLA/Action.thy
src/HOL/TLA/Intensional.thy
src/HOL/TLA/Memory/MemoryImplementation.thy
src/HOL/TLA/TLA.thy
src/HOL/UNITY/Comp/Alloc.thy
src/HOL/ex/Binary.thy
src/HOL/ex/Iff_Oracle.thy
src/Sequents/ILL.thy
src/Sequents/LK0.thy
src/Sequents/S4.thy
src/Sequents/S43.thy
src/Sequents/T.thy
src/ZF/UNITY/Mutex.thy
src/ZF/UNITY/SubstAx.thy
     1.1 --- a/src/CCL/CCL.thy	Sun May 15 17:06:35 2011 +0200
     1.2 +++ b/src/CCL/CCL.thy	Sun May 15 17:45:53 2011 +0200
     1.3 @@ -205,7 +205,7 @@
     1.4  
     1.5  method_setup inj_rl = {*
     1.6    Attrib.thms >> (fn rews => fn ctxt => SIMPLE_METHOD' (inj_rl_tac ctxt rews))
     1.7 -*} ""
     1.8 +*}
     1.9  
    1.10  lemma ccl_injs:
    1.11    "<a,b> = <a',b'> <-> (a=a' & b=b')"
     2.1 --- a/src/CCL/Term.thy	Sun May 15 17:06:35 2011 +0200
     2.2 +++ b/src/CCL/Term.thy	Sun May 15 17:45:53 2011 +0200
     2.3 @@ -205,7 +205,7 @@
     2.4    Scan.succeed (fn ctxt =>
     2.5      SIMPLE_METHOD' (CHANGED o
     2.6        simp_tac (simpset_of ctxt addsimps @{thms rawBs} setloop (stac @{thm letrecB}))))
     2.7 -*} ""
     2.8 +*}
     2.9  
    2.10  lemma ifBtrue: "if true then t else u = t"
    2.11    and ifBfalse: "if false then t else u = u"
     3.1 --- a/src/CCL/Type.thy	Sun May 15 17:06:35 2011 +0200
     3.2 +++ b/src/CCL/Type.thy	Sun May 15 17:45:53 2011 +0200
     3.3 @@ -137,7 +137,7 @@
     3.4  
     3.5  method_setup ncanT = {*
     3.6    Scan.succeed (SIMPLE_METHOD' o mk_ncanT_tac @{thms case_rls} @{thms case_rls})
     3.7 -*} ""
     3.8 +*}
     3.9  
    3.10  lemma ifT:
    3.11    "[| b:Bool; b=true ==> t:A(true); b=false ==> u:A(false) |] ==>
    3.12 @@ -278,7 +278,7 @@
    3.13  
    3.14  method_setup incanT = {*
    3.15    Scan.succeed (SIMPLE_METHOD' o mk_ncanT_tac @{thms icase_rls} @{thms case_rls})
    3.16 -*} ""
    3.17 +*}
    3.18  
    3.19  lemma ncaseT:
    3.20    "[| n:Nat; n=zero ==> b:C(zero); !!x.[| x:Nat;  n=succ(x) |] ==> c(x):C(succ(x)) |]
    3.21 @@ -400,9 +400,7 @@
    3.22      fast_tac (ctxt addIs (mono RS @{thm coinduct3_mono_lemma} RS @{thm lfpI}) :: prems) 1);
    3.23  *}
    3.24  
    3.25 -method_setup coinduct3 = {*
    3.26 -  Scan.succeed (SIMPLE_METHOD' o coinduct3_tac)
    3.27 -*} ""
    3.28 +method_setup coinduct3 = {* Scan.succeed (SIMPLE_METHOD' o coinduct3_tac) *}
    3.29  
    3.30  lemma ci3_RI: "[| mono(Agen);  a : R |] ==> a : lfp(%x. Agen(x) Un R Un A)"
    3.31    by coinduct3
    3.32 @@ -423,9 +421,9 @@
    3.33  *}
    3.34  
    3.35  method_setup genIs = {*
    3.36 -  Attrib.thm -- Attrib.thm >> (fn (genXH, gen_mono) => fn ctxt =>
    3.37 -    SIMPLE_METHOD' (genIs_tac ctxt genXH gen_mono))
    3.38 -*} ""
    3.39 +  Attrib.thm -- Attrib.thm >>
    3.40 +    (fn (genXH, gen_mono) => fn ctxt => SIMPLE_METHOD' (genIs_tac ctxt genXH gen_mono))
    3.41 +*}
    3.42  
    3.43  
    3.44  subsection {* POgen *}
     4.1 --- a/src/Cube/Example.thy	Sun May 15 17:06:35 2011 +0200
     4.2 +++ b/src/Cube/Example.thy	Sun May 15 17:45:53 2011 +0200
     4.3 @@ -13,19 +13,19 @@
     4.4  
     4.5  method_setup depth_solve = {*
     4.6    Attrib.thms >> (fn thms => K (METHOD (fn facts =>
     4.7 -  (DEPTH_SOLVE (HEADGOAL (ares_tac (facts @ thms)))))))
     4.8 -*} ""
     4.9 +    (DEPTH_SOLVE (HEADGOAL (ares_tac (facts @ thms)))))))
    4.10 +*}
    4.11  
    4.12  method_setup depth_solve1 = {*
    4.13    Attrib.thms >> (fn thms => K (METHOD (fn facts =>
    4.14 -  (DEPTH_SOLVE_1 (HEADGOAL (ares_tac (facts @ thms)))))))
    4.15 -*} ""
    4.16 +    (DEPTH_SOLVE_1 (HEADGOAL (ares_tac (facts @ thms)))))))
    4.17 +*}
    4.18  
    4.19  method_setup strip_asms =  {*
    4.20    Attrib.thms >> (fn thms => K (METHOD (fn facts =>
    4.21      REPEAT (resolve_tac [@{thm strip_b}, @{thm strip_s}] 1 THEN
    4.22      DEPTH_SOLVE_1 (ares_tac (facts @ thms) 1)))))
    4.23 -*} ""
    4.24 +*}
    4.25  
    4.26  
    4.27  subsection {* Simple types *}
     5.1 --- a/src/FOL/FOL.thy	Sun May 15 17:06:35 2011 +0200
     5.2 +++ b/src/FOL/FOL.thy	Sun May 15 17:45:53 2011 +0200
     5.3 @@ -73,7 +73,7 @@
     5.4  
     5.5  method_setup case_tac = {*
     5.6    Args.goal_spec -- Scan.lift Args.name_source >>
     5.7 -  (fn (quant, s) => fn ctxt => SIMPLE_METHOD'' quant (case_tac ctxt s))
     5.8 +    (fn (quant, s) => fn ctxt => SIMPLE_METHOD'' quant (case_tac ctxt s))
     5.9  *} "case_tac emulation (dynamic instantiation!)"
    5.10  
    5.11  
     6.1 --- a/src/HOL/Algebra/abstract/Ring2.thy	Sun May 15 17:06:35 2011 +0200
     6.2 +++ b/src/HOL/Algebra/abstract/Ring2.thy	Sun May 15 17:45:53 2011 +0200
     6.3 @@ -218,9 +218,9 @@
     6.4     @{thm r_distr}, @{thm l_null}, @{thm r_null}, @{thm l_minus}, @{thm r_minus}];
     6.5  *}   (* Note: r_one is not necessary in ring_ss *)
     6.6  
     6.7 -method_setup ring =
     6.8 -  {* Scan.succeed (K (SIMPLE_METHOD' (full_simp_tac ring_ss))) *}
     6.9 -  {* computes distributive normal form in rings *}
    6.10 +method_setup ring = {*
    6.11 +  Scan.succeed (K (SIMPLE_METHOD' (full_simp_tac ring_ss)))
    6.12 +*} "compute distributive normal form in rings"
    6.13  
    6.14  
    6.15  subsection {* Rings and the summation operator *}
     7.1 --- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Sun May 15 17:06:35 2011 +0200
     7.2 +++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Sun May 15 17:45:53 2011 +0200
     7.3 @@ -3044,7 +3044,7 @@
     7.4   (keyword typN |-- typ) -- (keyword parsN |-- terms) >>
     7.5    (fn (T,ps) => fn ctxt => SIMPLE_METHOD' (FRParTac.frpar_tac T ps ctxt))
     7.6  end
     7.7 -*} "Parametric QE for linear Arithmetic over fields, Version 1"
     7.8 +*} "parametric QE for linear Arithmetic over fields, Version 1"
     7.9  
    7.10  method_setup frpar2 = {*
    7.11  let
    7.12 @@ -3061,7 +3061,7 @@
    7.13   (keyword typN |-- typ) -- (keyword parsN |-- terms) >>
    7.14    (fn (T,ps) => fn ctxt => SIMPLE_METHOD' (FRParTac.frpar2_tac T ps ctxt))
    7.15  end
    7.16 -*} "Parametric QE for linear Arithmetic over fields, Version 2"
    7.17 +*} "parametric QE for linear Arithmetic over fields, Version 2"
    7.18  
    7.19  
    7.20  lemma "\<exists>(x::'a::{linordered_field_inverse_zero, number_ring}). y \<noteq> -1 \<longrightarrow> (y + 1)*x < 0"
     8.1 --- a/src/HOL/HOLCF/IOA/meta_theory/Abstraction.thy	Sun May 15 17:06:35 2011 +0200
     8.2 +++ b/src/HOL/HOLCF/IOA/meta_theory/Abstraction.thy	Sun May 15 17:45:53 2011 +0200
     8.3 @@ -610,6 +610,6 @@
     8.4          ss addsimps [@{thm state_strengthening_def}, @{thm state_weakening_def}])))
     8.5  *}
     8.6  
     8.7 -method_setup abstraction = {* Scan.succeed (SIMPLE_METHOD' o abstraction_tac) *} ""
     8.8 +method_setup abstraction = {* Scan.succeed (SIMPLE_METHOD' o abstraction_tac) *}
     8.9  
    8.10  end
     9.1 --- a/src/HOL/HOLCF/Lift.thy	Sun May 15 17:06:35 2011 +0200
     9.2 +++ b/src/HOL/HOLCF/Lift.thy	Sun May 15 17:45:53 2011 +0200
     9.3 @@ -47,7 +47,7 @@
     9.4  method_setup defined = {*
     9.5    Scan.succeed (fn ctxt => SIMPLE_METHOD'
     9.6      (etac @{thm lift_definedE} THEN' asm_simp_tac (simpset_of ctxt)))
     9.7 -*} ""
     9.8 +*}
     9.9  
    9.10  lemma DefE: "Def x = \<bottom> \<Longrightarrow> R"
    9.11    by simp
    10.1 --- a/src/HOL/Library/Reflection.thy	Sun May 15 17:06:35 2011 +0200
    10.2 +++ b/src/HOL/Library/Reflection.thy	Sun May 15 17:45:53 2011 +0200
    10.3 @@ -41,6 +41,6 @@
    10.4        val raw_eqs = eqs@ceqs
    10.5      in SIMPLE_METHOD' (Reflection.reflection_tac ctxt corr_thms raw_eqs to) end)
    10.6  end
    10.7 -*} "reflection"
    10.8 +*}
    10.9  
   10.10  end
    11.1 --- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Sun May 15 17:06:35 2011 +0200
    11.2 +++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Sun May 15 17:45:53 2011 +0200
    11.3 @@ -108,7 +108,7 @@
    11.4   in
    11.5    Attrib.thms >> (fn ths => K (SIMPLE_METHOD' (vector_arith_tac ths)))
    11.6   end
    11.7 -*} "Lifts trivial vector statements to real arith statements"
    11.8 +*} "lift trivial vector statements to real arith statements"
    11.9  
   11.10  lemma vec_0[simp]: "vec 0 = 0" by (vector vector_zero_def)
   11.11  lemma vec_1[simp]: "vec 1 = 1" by (vector vector_one_def)
    12.1 --- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Sun May 15 17:06:35 2011 +0200
    12.2 +++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Sun May 15 17:45:53 2011 +0200
    12.3 @@ -321,7 +321,7 @@
    12.4  use "normarith.ML"
    12.5  
    12.6  method_setup norm = {* Scan.succeed (SIMPLE_METHOD' o NormArith.norm_arith_tac)
    12.7 -*} "Proves simple linear statements about vector norms"
    12.8 +*} "prove simple linear statements about vector norms"
    12.9  
   12.10  
   12.11  text{* Hence more metric properties. *}
    13.1 --- a/src/HOL/Prolog/HOHH.thy	Sun May 15 17:06:35 2011 +0200
    13.2 +++ b/src/HOL/Prolog/HOHH.thy	Sun May 15 17:45:53 2011 +0200
    13.3 @@ -11,7 +11,7 @@
    13.4  
    13.5  method_setup ptac =
    13.6    {* Attrib.thms >> (fn thms => fn ctxt => SIMPLE_METHOD' (Prolog.ptac ctxt thms)) *}
    13.7 -  "Basic Lambda Prolog interpreter"
    13.8 +  "basic Lambda Prolog interpreter"
    13.9  
   13.10  method_setup prolog =
   13.11    {* Attrib.thms >> (fn thms => fn ctxt => SIMPLE_METHOD (Prolog.prolog_tac ctxt thms)) *}
    14.1 --- a/src/HOL/Quotient.thy	Sun May 15 17:06:35 2011 +0200
    14.2 +++ b/src/HOL/Quotient.thy	Sun May 15 17:45:53 2011 +0200
    14.3 @@ -728,36 +728,36 @@
    14.4  method_setup lifting =
    14.5    {* Attrib.thms >> (fn thms => fn ctxt => 
    14.6         SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.lift_tac ctxt [] thms))) *}
    14.7 -  {* lifts theorems to quotient types *}
    14.8 +  {* lift theorems to quotient types *}
    14.9  
   14.10  method_setup lifting_setup =
   14.11    {* Attrib.thm >> (fn thm => fn ctxt => 
   14.12         SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.lift_procedure_tac ctxt [] thm))) *}
   14.13 -  {* sets up the three goals for the quotient lifting procedure *}
   14.14 +  {* set up the three goals for the quotient lifting procedure *}
   14.15  
   14.16  method_setup descending =
   14.17    {* Scan.succeed (fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.descend_tac ctxt []))) *}
   14.18 -  {* decends theorems to the raw level *}
   14.19 +  {* decend theorems to the raw level *}
   14.20  
   14.21  method_setup descending_setup =
   14.22    {* Scan.succeed (fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.descend_procedure_tac ctxt []))) *}
   14.23 -  {* sets up the three goals for the decending theorems *}
   14.24 +  {* set up the three goals for the decending theorems *}
   14.25  
   14.26  method_setup regularize =
   14.27    {* Scan.succeed (fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.regularize_tac ctxt))) *}
   14.28 -  {* proves the regularization goals from the quotient lifting procedure *}
   14.29 +  {* prove the regularization goals from the quotient lifting procedure *}
   14.30  
   14.31  method_setup injection =
   14.32    {* Scan.succeed (fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.all_injection_tac ctxt))) *}
   14.33 -  {* proves the rep/abs injection goals from the quotient lifting procedure *}
   14.34 +  {* prove the rep/abs injection goals from the quotient lifting procedure *}
   14.35  
   14.36  method_setup cleaning =
   14.37    {* Scan.succeed (fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.clean_tac ctxt))) *}
   14.38 -  {* proves the cleaning goals from the quotient lifting procedure *}
   14.39 +  {* prove the cleaning goals from the quotient lifting procedure *}
   14.40  
   14.41  attribute_setup quot_lifted =
   14.42    {* Scan.succeed Quotient_Tacs.lifted_attrib *}
   14.43 -  {* lifts theorems to quotient types *}
   14.44 +  {* lift theorems to quotient types *}
   14.45  
   14.46  no_notation
   14.47    rel_conj (infixr "OOO" 75) and
    15.1 --- a/src/HOL/SET_Protocol/Cardholder_Registration.thy	Sun May 15 17:06:35 2011 +0200
    15.2 +++ b/src/HOL/SET_Protocol/Cardholder_Registration.thy	Sun May 15 17:45:53 2011 +0200
    15.3 @@ -541,7 +541,7 @@
    15.4        EVERY [ftac @{thm Gets_certificate_valid} i,
    15.5               assume_tac i,
    15.6               etac conjE i, REPEAT (hyp_subst_tac i)])))
    15.7 -*} ""
    15.8 +*}
    15.9  
   15.10  text{*The @{text "(no_asm)"} attribute is essential, since it retains
   15.11    the quantifier and allows the simprule's condition to itself be simplified.*}
    16.1 --- a/src/HOL/SET_Protocol/Purchase.thy	Sun May 15 17:06:35 2011 +0200
    16.2 +++ b/src/HOL/SET_Protocol/Purchase.thy	Sun May 15 17:45:53 2011 +0200
    16.3 @@ -484,7 +484,7 @@
    16.4      K (SIMPLE_METHOD'' quant (fn i =>
    16.5        EVERY [ftac @{thm Gets_certificate_valid} i,
    16.6               assume_tac i, REPEAT (hyp_subst_tac i)])))
    16.7 -*} ""
    16.8 +*}
    16.9  
   16.10  
   16.11  subsection{*Proofs on Symmetric Keys*}
    17.1 --- a/src/HOL/TLA/Action.thy	Sun May 15 17:06:35 2011 +0200
    17.2 +++ b/src/HOL/TLA/Action.thy	Sun May 15 17:45:53 2011 +0200
    17.3 @@ -120,9 +120,9 @@
    17.4      | _ => th;
    17.5  *}
    17.6  
    17.7 -attribute_setup action_unlift = {* Scan.succeed (Thm.rule_attribute (K action_unlift)) *} ""
    17.8 -attribute_setup action_rewrite = {* Scan.succeed (Thm.rule_attribute (K action_rewrite)) *} ""
    17.9 -attribute_setup action_use = {* Scan.succeed (Thm.rule_attribute (K action_use)) *} ""
   17.10 +attribute_setup action_unlift = {* Scan.succeed (Thm.rule_attribute (K action_unlift)) *}
   17.11 +attribute_setup action_rewrite = {* Scan.succeed (Thm.rule_attribute (K action_rewrite)) *}
   17.12 +attribute_setup action_use = {* Scan.succeed (Thm.rule_attribute (K action_use)) *}
   17.13  
   17.14  
   17.15  (* =========================== square / angle brackets =========================== *)
   17.16 @@ -283,7 +283,7 @@
   17.17  
   17.18  method_setup enabled = {*
   17.19    Attrib.thm >> (fn th => fn ctxt => SIMPLE_METHOD' (enabled_tac ctxt th))
   17.20 -*} ""
   17.21 +*}
   17.22  
   17.23  (* Example *)
   17.24  
    18.1 --- a/src/HOL/TLA/Intensional.thy	Sun May 15 17:06:35 2011 +0200
    18.2 +++ b/src/HOL/TLA/Intensional.thy	Sun May 15 17:45:53 2011 +0200
    18.3 @@ -289,10 +289,10 @@
    18.4      | _ => th
    18.5  *}
    18.6  
    18.7 -attribute_setup int_unlift = {* Scan.succeed (Thm.rule_attribute (K int_unlift)) *} ""
    18.8 -attribute_setup int_rewrite = {* Scan.succeed (Thm.rule_attribute (K int_rewrite)) *} ""
    18.9 -attribute_setup flatten = {* Scan.succeed (Thm.rule_attribute (K flatten)) *} ""
   18.10 -attribute_setup int_use = {* Scan.succeed (Thm.rule_attribute (K int_use)) *} ""
   18.11 +attribute_setup int_unlift = {* Scan.succeed (Thm.rule_attribute (K int_unlift)) *}
   18.12 +attribute_setup int_rewrite = {* Scan.succeed (Thm.rule_attribute (K int_rewrite)) *}
   18.13 +attribute_setup flatten = {* Scan.succeed (Thm.rule_attribute (K flatten)) *}
   18.14 +attribute_setup int_use = {* Scan.succeed (Thm.rule_attribute (K int_use)) *}
   18.15  
   18.16  lemma Not_Rall: "|- (~(! x. F x)) = (? x. ~F x)"
   18.17    by (simp add: Valid_def)
    19.1 --- a/src/HOL/TLA/Memory/MemoryImplementation.thy	Sun May 15 17:06:35 2011 +0200
    19.2 +++ b/src/HOL/TLA/Memory/MemoryImplementation.thy	Sun May 15 17:45:53 2011 +0200
    19.3 @@ -803,7 +803,7 @@
    19.4  method_setup split_idle = {*
    19.5    Method.sections (Simplifier.simp_modifiers @ Splitter.split_modifiers)
    19.6      >> (K (SIMPLE_METHOD' o split_idle_tac))
    19.7 -*} ""
    19.8 +*}
    19.9  
   19.10  (* ----------------------------------------------------------------------
   19.11     Combine steps 1.2 and 1.4 to prove that the implementation satisfies
    20.1 --- a/src/HOL/TLA/TLA.thy	Sun May 15 17:06:35 2011 +0200
    20.2 +++ b/src/HOL/TLA/TLA.thy	Sun May 15 17:45:53 2011 +0200
    20.3 @@ -128,10 +128,10 @@
    20.4  fun try_rewrite th = temp_rewrite th handle THM _ => temp_use th;
    20.5  *}
    20.6  
    20.7 -attribute_setup temp_unlift = {* Scan.succeed (Thm.rule_attribute (K temp_unlift)) *} ""
    20.8 -attribute_setup temp_rewrite = {* Scan.succeed (Thm.rule_attribute (K temp_rewrite)) *} ""
    20.9 -attribute_setup temp_use = {* Scan.succeed (Thm.rule_attribute (K temp_use)) *} ""
   20.10 -attribute_setup try_rewrite = {* Scan.succeed (Thm.rule_attribute (K try_rewrite)) *} ""
   20.11 +attribute_setup temp_unlift = {* Scan.succeed (Thm.rule_attribute (K temp_unlift)) *}
   20.12 +attribute_setup temp_rewrite = {* Scan.succeed (Thm.rule_attribute (K temp_rewrite)) *}
   20.13 +attribute_setup temp_use = {* Scan.succeed (Thm.rule_attribute (K temp_use)) *}
   20.14 +attribute_setup try_rewrite = {* Scan.succeed (Thm.rule_attribute (K try_rewrite)) *}
   20.15  
   20.16  
   20.17  (* Update classical reasoner---will be updated once more below! *)
   20.18 @@ -310,10 +310,10 @@
   20.19                           eres_inst_tac ctxt [(("'a", 0), "state * state")] @{thm box_thin} i])
   20.20  *}
   20.21  
   20.22 -method_setup merge_box = {* Scan.succeed (K (SIMPLE_METHOD' merge_box_tac)) *} ""
   20.23 -method_setup merge_temp_box = {* Scan.succeed (SIMPLE_METHOD' o merge_temp_box_tac) *} ""
   20.24 -method_setup merge_stp_box = {* Scan.succeed (SIMPLE_METHOD' o merge_stp_box_tac) *} ""
   20.25 -method_setup merge_act_box = {* Scan.succeed (SIMPLE_METHOD' o merge_act_box_tac) *} ""
   20.26 +method_setup merge_box = {* Scan.succeed (K (SIMPLE_METHOD' merge_box_tac)) *}
   20.27 +method_setup merge_temp_box = {* Scan.succeed (SIMPLE_METHOD' o merge_temp_box_tac) *}
   20.28 +method_setup merge_stp_box = {* Scan.succeed (SIMPLE_METHOD' o merge_stp_box_tac) *}
   20.29 +method_setup merge_act_box = {* Scan.succeed (SIMPLE_METHOD' o merge_act_box_tac) *}
   20.30  
   20.31  (* rewrite rule to push universal quantification through box:
   20.32        (sigma |= [](! x. F x)) = (! x. (sigma |= []F x))
   20.33 @@ -606,11 +606,11 @@
   20.34  
   20.35  method_setup invariant = {*
   20.36    Method.sections Clasimp.clasimp_modifiers >> (K (SIMPLE_METHOD' o inv_tac))
   20.37 -*} ""
   20.38 +*}
   20.39  
   20.40  method_setup auto_invariant = {*
   20.41    Method.sections Clasimp.clasimp_modifiers >> (K (SIMPLE_METHOD' o auto_inv_tac))
   20.42 -*} ""
   20.43 +*}
   20.44  
   20.45  lemma unless: "|- []($P --> P` | Q`) --> (stable P) | <>Q"
   20.46    apply (unfold dmd_def)
    21.1 --- a/src/HOL/UNITY/Comp/Alloc.thy	Sun May 15 17:06:35 2011 +0200
    21.2 +++ b/src/HOL/UNITY/Comp/Alloc.thy	Sun May 15 17:45:53 2011 +0200
    21.3 @@ -326,7 +326,7 @@
    21.4  in
    21.5    Scan.succeed (Thm.rule_attribute (K normalized))
    21.6  end
    21.7 -*} ""
    21.8 +*}
    21.9  
   21.10  (*** bijectivity of sysOfAlloc [MUST BE AUTOMATED] ***)
   21.11  ML {*
   21.12 @@ -342,9 +342,7 @@
   21.13  
   21.14  *}
   21.15  
   21.16 -method_setup record_auto = {*
   21.17 -  Scan.succeed (SIMPLE_METHOD o record_auto_tac)
   21.18 -*} ""
   21.19 +method_setup record_auto = {* Scan.succeed (SIMPLE_METHOD o record_auto_tac) *}
   21.20  
   21.21  lemma inj_sysOfAlloc [iff]: "inj sysOfAlloc"
   21.22    apply (unfold sysOfAlloc_def Let_def)
   21.23 @@ -737,7 +735,7 @@
   21.24  method_setup rename_client_map = {*
   21.25    Scan.succeed (fn ctxt =>
   21.26      SIMPLE_METHOD (rename_client_map_tac (simpset_of ctxt)))
   21.27 -*} ""
   21.28 +*}
   21.29  
   21.30  text{*Lifting @{text Client_Increasing} to @{term systemState}*}
   21.31  lemma rename_Client_Increasing: "i : I
    22.1 --- a/src/HOL/ex/Binary.thy	Sun May 15 17:06:35 2011 +0200
    22.2 +++ b/src/HOL/ex/Binary.thy	Sun May 15 17:45:53 2011 +0200
    22.3 @@ -180,7 +180,7 @@
    22.4            @{simproc binary_nat_diff},
    22.5            @{simproc binary_nat_div},
    22.6            @{simproc binary_nat_mod}]))))
    22.7 -*} "binary simplification"
    22.8 +*}
    22.9  
   22.10  
   22.11  subsection {* Concrete syntax *}
    23.1 --- a/src/HOL/ex/Iff_Oracle.thy	Sun May 15 17:06:35 2011 +0200
    23.2 +++ b/src/HOL/ex/Iff_Oracle.thy	Sun May 15 17:45:53 2011 +0200
    23.3 @@ -56,7 +56,7 @@
    23.4      SIMPLE_METHOD
    23.5        (HEADGOAL (rtac (iff_oracle (Proof_Context.theory_of ctxt, n)))
    23.6          handle Fail _ => no_tac))
    23.7 -*} "iff oracle"
    23.8 +*}
    23.9  
   23.10  
   23.11  lemma "A <-> A"
    24.1 --- a/src/Sequents/ILL.thy	Sun May 15 17:06:35 2011 +0200
    24.2 +++ b/src/Sequents/ILL.thy	Sun May 15 17:45:53 2011 +0200
    24.3 @@ -274,10 +274,10 @@
    24.4  
    24.5  
    24.6  method_setup best_safe =
    24.7 -  {* Scan.succeed (K (SIMPLE_METHOD' (best_tac safe_cs))) *} ""
    24.8 +  {* Scan.succeed (K (SIMPLE_METHOD' (best_tac safe_cs))) *}
    24.9  
   24.10  method_setup best_power =
   24.11 -  {* Scan.succeed (K (SIMPLE_METHOD' (best_tac power_cs))) *} ""
   24.12 +  {* Scan.succeed (K (SIMPLE_METHOD' (best_tac power_cs))) *}
   24.13  
   24.14  
   24.15  (* Some examples from Troelstra and van Dalen *)
    25.1 --- a/src/Sequents/LK0.thy	Sun May 15 17:06:35 2011 +0200
    25.2 +++ b/src/Sequents/LK0.thy	Sun May 15 17:45:53 2011 +0200
    25.3 @@ -225,25 +225,11 @@
    25.4      rtac (@{thm thinR} RS @{thm cut}) i THEN REPEAT (rtac @{thm thinL} i) THEN rtac th i;
    25.5  *}
    25.6  
    25.7 -method_setup fast_prop =
    25.8 -  {* Scan.succeed (K (SIMPLE_METHOD' (fast_tac prop_pack))) *}
    25.9 -  "propositional reasoning"
   25.10 -
   25.11 -method_setup fast =
   25.12 -  {* Scan.succeed (K (SIMPLE_METHOD' (fast_tac LK_pack))) *}
   25.13 -  "classical reasoning"
   25.14 -
   25.15 -method_setup fast_dup =
   25.16 -  {* Scan.succeed (K (SIMPLE_METHOD' (fast_tac LK_dup_pack))) *}
   25.17 -  "classical reasoning"
   25.18 -
   25.19 -method_setup best =
   25.20 -  {* Scan.succeed (K (SIMPLE_METHOD' (best_tac LK_pack))) *}
   25.21 -  "classical reasoning"
   25.22 -
   25.23 -method_setup best_dup =
   25.24 -  {* Scan.succeed (K (SIMPLE_METHOD' (best_tac LK_dup_pack))) *}
   25.25 -  "classical reasoning"
   25.26 +method_setup fast_prop = {* Scan.succeed (K (SIMPLE_METHOD' (fast_tac prop_pack))) *}
   25.27 +method_setup fast = {* Scan.succeed (K (SIMPLE_METHOD' (fast_tac LK_pack))) *}
   25.28 +method_setup fast_dup = {* Scan.succeed (K (SIMPLE_METHOD' (fast_tac LK_dup_pack))) *}
   25.29 +method_setup best = {* Scan.succeed (K (SIMPLE_METHOD' (best_tac LK_pack))) *}
   25.30 +method_setup best_dup = {* Scan.succeed (K (SIMPLE_METHOD' (best_tac LK_dup_pack))) *}
   25.31  
   25.32  
   25.33  lemma mp_R:
    26.1 --- a/src/Sequents/S4.thy	Sun May 15 17:06:35 2011 +0200
    26.2 +++ b/src/Sequents/S4.thy	Sun May 15 17:45:53 2011 +0200
    26.3 @@ -43,8 +43,7 @@
    26.4  )
    26.5  *}
    26.6  
    26.7 -method_setup S4_solve =
    26.8 -  {* Scan.succeed (K (SIMPLE_METHOD (S4_Prover.solve_tac 2))) *} "S4 solver"
    26.9 +method_setup S4_solve = {* Scan.succeed (K (SIMPLE_METHOD (S4_Prover.solve_tac 2))) *}
   26.10  
   26.11  
   26.12  (* Theorems of system T from Hughes and Cresswell and Hailpern, LNCS 129 *)
    27.1 --- a/src/Sequents/S43.thy	Sun May 15 17:06:35 2011 +0200
    27.2 +++ b/src/Sequents/S43.thy	Sun May 15 17:45:53 2011 +0200
    27.3 @@ -92,7 +92,7 @@
    27.4  method_setup S43_solve = {*
    27.5    Scan.succeed (K (SIMPLE_METHOD
    27.6      (S43_Prover.solve_tac 2 ORELSE S43_Prover.solve_tac 3)))
    27.7 -*} "S4 solver"
    27.8 +*}
    27.9  
   27.10  
   27.11  (* Theorems of system T from Hughes and Cresswell and Hailpern, LNCS 129 *)
    28.1 --- a/src/Sequents/T.thy	Sun May 15 17:06:35 2011 +0200
    28.2 +++ b/src/Sequents/T.thy	Sun May 15 17:45:53 2011 +0200
    28.3 @@ -42,8 +42,7 @@
    28.4  )
    28.5  *}
    28.6  
    28.7 -method_setup T_solve =
    28.8 -  {* Scan.succeed (K (SIMPLE_METHOD (T_Prover.solve_tac 2))) *} "T solver"
    28.9 +method_setup T_solve = {* Scan.succeed (K (SIMPLE_METHOD (T_Prover.solve_tac 2))) *}
   28.10  
   28.11  
   28.12  (* Theorems of system T from Hughes and Cresswell and Hailpern, LNCS 129 *)
    29.1 --- a/src/ZF/UNITY/Mutex.thy	Sun May 15 17:06:35 2011 +0200
    29.2 +++ b/src/ZF/UNITY/Mutex.thy	Sun May 15 17:45:53 2011 +0200
    29.3 @@ -207,18 +207,18 @@
    29.4  
    29.5  lemma U_F1:
    29.6       "Mutex \<in> {s \<in> state. s`m=#1} LeadsTo {s \<in> state. s`p = s`v & s`m = #2}"
    29.7 -by (unfold Mutex_def, ensures_tac U1)
    29.8 +by (unfold Mutex_def, ensures U1)
    29.9  
   29.10  lemma U_F2: "Mutex \<in> {s \<in> state. s`p =0 & s`m = #2} LeadsTo {s \<in> state. s`m = #3}"
   29.11  apply (cut_tac IU)
   29.12 -apply (unfold Mutex_def, ensures_tac U2)
   29.13 +apply (unfold Mutex_def, ensures U2)
   29.14  done
   29.15  
   29.16  lemma U_F3: "Mutex \<in> {s \<in> state. s`m = #3} LeadsTo {s \<in> state. s`p=1}"
   29.17  apply (rule_tac B = "{s \<in> state. s`m = #4}" in LeadsTo_Trans)
   29.18   apply (unfold Mutex_def)
   29.19 - apply (ensures_tac U3)
   29.20 -apply (ensures_tac U4)
   29.21 + apply (ensures U3)
   29.22 +apply (ensures U4)
   29.23  done
   29.24  
   29.25  
   29.26 @@ -258,18 +258,18 @@
   29.27  by (unfold op_Unless_def Mutex_def, safety)
   29.28  
   29.29  lemma V_F1: "Mutex \<in> {s \<in> state. s`n=#1} LeadsTo {s \<in> state. s`p = not(s`u) & s`n = #2}"
   29.30 -by (unfold Mutex_def, ensures_tac "V1")
   29.31 +by (unfold Mutex_def, ensures "V1")
   29.32  
   29.33  lemma V_F2: "Mutex \<in> {s \<in> state. s`p=1 & s`n = #2} LeadsTo {s \<in> state. s`n = #3}"
   29.34  apply (cut_tac IV)
   29.35 -apply (unfold Mutex_def, ensures_tac "V2")
   29.36 +apply (unfold Mutex_def, ensures "V2")
   29.37  done
   29.38  
   29.39  lemma V_F3: "Mutex \<in> {s \<in> state. s`n = #3} LeadsTo {s \<in> state. s`p=0}"
   29.40  apply (rule_tac B = "{s \<in> state. s`n = #4}" in LeadsTo_Trans)
   29.41   apply (unfold Mutex_def)
   29.42 - apply (ensures_tac V3)
   29.43 -apply (ensures_tac V4)
   29.44 + apply (ensures V3)
   29.45 +apply (ensures V4)
   29.46  done
   29.47  
   29.48  lemma V_lemma2: "Mutex \<in> {s \<in> state. s`n = #2} LeadsTo {s \<in> state. s`p=0}"
    30.1 --- a/src/ZF/UNITY/SubstAx.thy	Sun May 15 17:06:35 2011 +0200
    30.2 +++ b/src/ZF/UNITY/SubstAx.thy	Sun May 15 17:45:53 2011 +0200
    30.3 @@ -376,7 +376,7 @@
    30.4    end;
    30.5  *}
    30.6  
    30.7 -method_setup ensures_tac = {*
    30.8 +method_setup ensures = {*
    30.9      Args.goal_spec -- Scan.lift Args.name_source >>
   30.10      (fn (quant, s) => fn ctxt => SIMPLE_METHOD'' quant (ensures_tac ctxt s))
   30.11  *} "for proving progress properties"