# HG changeset patch
# User wenzelm
# Date 1305474353 -7200
# Node ID 5af15f1e2ef60b0bf864250e238a906973f29c7a
# Parent  6c841fa92fa2699273ff06db2acb4e9fb94c5c41
simplified/unified method_setup/attribute_setup;

diff -r 6c841fa92fa2 -r 5af15f1e2ef6 src/CCL/CCL.thy
--- a/src/CCL/CCL.thy	Sun May 15 17:06:35 2011 +0200
+++ b/src/CCL/CCL.thy	Sun May 15 17:45:53 2011 +0200
@@ -205,7 +205,7 @@
 
 method_setup inj_rl = {*
   Attrib.thms >> (fn rews => fn ctxt => SIMPLE_METHOD' (inj_rl_tac ctxt rews))
-*} ""
+*}
 
 lemma ccl_injs:
   "<a,b> = <a',b'> <-> (a=a' & b=b')"
diff -r 6c841fa92fa2 -r 5af15f1e2ef6 src/CCL/Term.thy
--- a/src/CCL/Term.thy	Sun May 15 17:06:35 2011 +0200
+++ b/src/CCL/Term.thy	Sun May 15 17:45:53 2011 +0200
@@ -205,7 +205,7 @@
   Scan.succeed (fn ctxt =>
     SIMPLE_METHOD' (CHANGED o
       simp_tac (simpset_of ctxt addsimps @{thms rawBs} setloop (stac @{thm letrecB}))))
-*} ""
+*}
 
 lemma ifBtrue: "if true then t else u = t"
   and ifBfalse: "if false then t else u = u"
diff -r 6c841fa92fa2 -r 5af15f1e2ef6 src/CCL/Type.thy
--- a/src/CCL/Type.thy	Sun May 15 17:06:35 2011 +0200
+++ b/src/CCL/Type.thy	Sun May 15 17:45:53 2011 +0200
@@ -137,7 +137,7 @@
 
 method_setup ncanT = {*
   Scan.succeed (SIMPLE_METHOD' o mk_ncanT_tac @{thms case_rls} @{thms case_rls})
-*} ""
+*}
 
 lemma ifT:
   "[| b:Bool; b=true ==> t:A(true); b=false ==> u:A(false) |] ==>
@@ -278,7 +278,7 @@
 
 method_setup incanT = {*
   Scan.succeed (SIMPLE_METHOD' o mk_ncanT_tac @{thms icase_rls} @{thms case_rls})
-*} ""
+*}
 
 lemma ncaseT:
   "[| n:Nat; n=zero ==> b:C(zero); !!x.[| x:Nat;  n=succ(x) |] ==> c(x):C(succ(x)) |]
@@ -400,9 +400,7 @@
     fast_tac (ctxt addIs (mono RS @{thm coinduct3_mono_lemma} RS @{thm lfpI}) :: prems) 1);
 *}
 
-method_setup coinduct3 = {*
-  Scan.succeed (SIMPLE_METHOD' o coinduct3_tac)
-*} ""
+method_setup coinduct3 = {* Scan.succeed (SIMPLE_METHOD' o coinduct3_tac) *}
 
 lemma ci3_RI: "[| mono(Agen);  a : R |] ==> a : lfp(%x. Agen(x) Un R Un A)"
   by coinduct3
@@ -423,9 +421,9 @@
 *}
 
 method_setup genIs = {*
-  Attrib.thm -- Attrib.thm >> (fn (genXH, gen_mono) => fn ctxt =>
-    SIMPLE_METHOD' (genIs_tac ctxt genXH gen_mono))
-*} ""
+  Attrib.thm -- Attrib.thm >>
+    (fn (genXH, gen_mono) => fn ctxt => SIMPLE_METHOD' (genIs_tac ctxt genXH gen_mono))
+*}
 
 
 subsection {* POgen *}
diff -r 6c841fa92fa2 -r 5af15f1e2ef6 src/Cube/Example.thy
--- a/src/Cube/Example.thy	Sun May 15 17:06:35 2011 +0200
+++ b/src/Cube/Example.thy	Sun May 15 17:45:53 2011 +0200
@@ -13,19 +13,19 @@
 
 method_setup depth_solve = {*
   Attrib.thms >> (fn thms => K (METHOD (fn facts =>
-  (DEPTH_SOLVE (HEADGOAL (ares_tac (facts @ thms)))))))
-*} ""
+    (DEPTH_SOLVE (HEADGOAL (ares_tac (facts @ thms)))))))
+*}
 
 method_setup depth_solve1 = {*
   Attrib.thms >> (fn thms => K (METHOD (fn facts =>
-  (DEPTH_SOLVE_1 (HEADGOAL (ares_tac (facts @ thms)))))))
-*} ""
+    (DEPTH_SOLVE_1 (HEADGOAL (ares_tac (facts @ thms)))))))
+*}
 
 method_setup strip_asms =  {*
   Attrib.thms >> (fn thms => K (METHOD (fn facts =>
     REPEAT (resolve_tac [@{thm strip_b}, @{thm strip_s}] 1 THEN
     DEPTH_SOLVE_1 (ares_tac (facts @ thms) 1)))))
-*} ""
+*}
 
 
 subsection {* Simple types *}
diff -r 6c841fa92fa2 -r 5af15f1e2ef6 src/FOL/FOL.thy
--- a/src/FOL/FOL.thy	Sun May 15 17:06:35 2011 +0200
+++ b/src/FOL/FOL.thy	Sun May 15 17:45:53 2011 +0200
@@ -73,7 +73,7 @@
 
 method_setup case_tac = {*
   Args.goal_spec -- Scan.lift Args.name_source >>
-  (fn (quant, s) => fn ctxt => SIMPLE_METHOD'' quant (case_tac ctxt s))
+    (fn (quant, s) => fn ctxt => SIMPLE_METHOD'' quant (case_tac ctxt s))
 *} "case_tac emulation (dynamic instantiation!)"
 
 
diff -r 6c841fa92fa2 -r 5af15f1e2ef6 src/HOL/Algebra/abstract/Ring2.thy
--- a/src/HOL/Algebra/abstract/Ring2.thy	Sun May 15 17:06:35 2011 +0200
+++ b/src/HOL/Algebra/abstract/Ring2.thy	Sun May 15 17:45:53 2011 +0200
@@ -218,9 +218,9 @@
    @{thm r_distr}, @{thm l_null}, @{thm r_null}, @{thm l_minus}, @{thm r_minus}];
 *}   (* Note: r_one is not necessary in ring_ss *)
 
-method_setup ring =
-  {* Scan.succeed (K (SIMPLE_METHOD' (full_simp_tac ring_ss))) *}
-  {* computes distributive normal form in rings *}
+method_setup ring = {*
+  Scan.succeed (K (SIMPLE_METHOD' (full_simp_tac ring_ss)))
+*} "compute distributive normal form in rings"
 
 
 subsection {* Rings and the summation operator *}
diff -r 6c841fa92fa2 -r 5af15f1e2ef6 src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
--- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Sun May 15 17:06:35 2011 +0200
+++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Sun May 15 17:45:53 2011 +0200
@@ -3044,7 +3044,7 @@
  (keyword typN |-- typ) -- (keyword parsN |-- terms) >>
   (fn (T,ps) => fn ctxt => SIMPLE_METHOD' (FRParTac.frpar_tac T ps ctxt))
 end
-*} "Parametric QE for linear Arithmetic over fields, Version 1"
+*} "parametric QE for linear Arithmetic over fields, Version 1"
 
 method_setup frpar2 = {*
 let
@@ -3061,7 +3061,7 @@
  (keyword typN |-- typ) -- (keyword parsN |-- terms) >>
   (fn (T,ps) => fn ctxt => SIMPLE_METHOD' (FRParTac.frpar2_tac T ps ctxt))
 end
-*} "Parametric QE for linear Arithmetic over fields, Version 2"
+*} "parametric QE for linear Arithmetic over fields, Version 2"
 
 
 lemma "\<exists>(x::'a::{linordered_field_inverse_zero, number_ring}). y \<noteq> -1 \<longrightarrow> (y + 1)*x < 0"
diff -r 6c841fa92fa2 -r 5af15f1e2ef6 src/HOL/HOLCF/IOA/meta_theory/Abstraction.thy
--- a/src/HOL/HOLCF/IOA/meta_theory/Abstraction.thy	Sun May 15 17:06:35 2011 +0200
+++ b/src/HOL/HOLCF/IOA/meta_theory/Abstraction.thy	Sun May 15 17:45:53 2011 +0200
@@ -610,6 +610,6 @@
         ss addsimps [@{thm state_strengthening_def}, @{thm state_weakening_def}])))
 *}
 
-method_setup abstraction = {* Scan.succeed (SIMPLE_METHOD' o abstraction_tac) *} ""
+method_setup abstraction = {* Scan.succeed (SIMPLE_METHOD' o abstraction_tac) *}
 
 end
diff -r 6c841fa92fa2 -r 5af15f1e2ef6 src/HOL/HOLCF/Lift.thy
--- a/src/HOL/HOLCF/Lift.thy	Sun May 15 17:06:35 2011 +0200
+++ b/src/HOL/HOLCF/Lift.thy	Sun May 15 17:45:53 2011 +0200
@@ -47,7 +47,7 @@
 method_setup defined = {*
   Scan.succeed (fn ctxt => SIMPLE_METHOD'
     (etac @{thm lift_definedE} THEN' asm_simp_tac (simpset_of ctxt)))
-*} ""
+*}
 
 lemma DefE: "Def x = \<bottom> \<Longrightarrow> R"
   by simp
diff -r 6c841fa92fa2 -r 5af15f1e2ef6 src/HOL/Library/Reflection.thy
--- a/src/HOL/Library/Reflection.thy	Sun May 15 17:06:35 2011 +0200
+++ b/src/HOL/Library/Reflection.thy	Sun May 15 17:45:53 2011 +0200
@@ -41,6 +41,6 @@
       val raw_eqs = eqs@ceqs
     in SIMPLE_METHOD' (Reflection.reflection_tac ctxt corr_thms raw_eqs to) end)
 end
-*} "reflection"
+*}
 
 end
diff -r 6c841fa92fa2 -r 5af15f1e2ef6 src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Sun May 15 17:06:35 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Cartesian_Euclidean_Space.thy	Sun May 15 17:45:53 2011 +0200
@@ -108,7 +108,7 @@
  in
   Attrib.thms >> (fn ths => K (SIMPLE_METHOD' (vector_arith_tac ths)))
  end
-*} "Lifts trivial vector statements to real arith statements"
+*} "lift trivial vector statements to real arith statements"
 
 lemma vec_0[simp]: "vec 0 = 0" by (vector vector_zero_def)
 lemma vec_1[simp]: "vec 1 = 1" by (vector vector_one_def)
diff -r 6c841fa92fa2 -r 5af15f1e2ef6 src/HOL/Multivariate_Analysis/Euclidean_Space.thy
--- a/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Sun May 15 17:06:35 2011 +0200
+++ b/src/HOL/Multivariate_Analysis/Euclidean_Space.thy	Sun May 15 17:45:53 2011 +0200
@@ -321,7 +321,7 @@
 use "normarith.ML"
 
 method_setup norm = {* Scan.succeed (SIMPLE_METHOD' o NormArith.norm_arith_tac)
-*} "Proves simple linear statements about vector norms"
+*} "prove simple linear statements about vector norms"
 
 
 text{* Hence more metric properties. *}
diff -r 6c841fa92fa2 -r 5af15f1e2ef6 src/HOL/Prolog/HOHH.thy
--- a/src/HOL/Prolog/HOHH.thy	Sun May 15 17:06:35 2011 +0200
+++ b/src/HOL/Prolog/HOHH.thy	Sun May 15 17:45:53 2011 +0200
@@ -11,7 +11,7 @@
 
 method_setup ptac =
   {* Attrib.thms >> (fn thms => fn ctxt => SIMPLE_METHOD' (Prolog.ptac ctxt thms)) *}
-  "Basic Lambda Prolog interpreter"
+  "basic Lambda Prolog interpreter"
 
 method_setup prolog =
   {* Attrib.thms >> (fn thms => fn ctxt => SIMPLE_METHOD (Prolog.prolog_tac ctxt thms)) *}
diff -r 6c841fa92fa2 -r 5af15f1e2ef6 src/HOL/Quotient.thy
--- a/src/HOL/Quotient.thy	Sun May 15 17:06:35 2011 +0200
+++ b/src/HOL/Quotient.thy	Sun May 15 17:45:53 2011 +0200
@@ -728,36 +728,36 @@
 method_setup lifting =
   {* Attrib.thms >> (fn thms => fn ctxt => 
        SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.lift_tac ctxt [] thms))) *}
-  {* lifts theorems to quotient types *}
+  {* lift theorems to quotient types *}
 
 method_setup lifting_setup =
   {* Attrib.thm >> (fn thm => fn ctxt => 
        SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.lift_procedure_tac ctxt [] thm))) *}
-  {* sets up the three goals for the quotient lifting procedure *}
+  {* set up the three goals for the quotient lifting procedure *}
 
 method_setup descending =
   {* Scan.succeed (fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.descend_tac ctxt []))) *}
-  {* decends theorems to the raw level *}
+  {* decend theorems to the raw level *}
 
 method_setup descending_setup =
   {* Scan.succeed (fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.descend_procedure_tac ctxt []))) *}
-  {* sets up the three goals for the decending theorems *}
+  {* set up the three goals for the decending theorems *}
 
 method_setup regularize =
   {* Scan.succeed (fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.regularize_tac ctxt))) *}
-  {* proves the regularization goals from the quotient lifting procedure *}
+  {* prove the regularization goals from the quotient lifting procedure *}
 
 method_setup injection =
   {* Scan.succeed (fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.all_injection_tac ctxt))) *}
-  {* proves the rep/abs injection goals from the quotient lifting procedure *}
+  {* prove the rep/abs injection goals from the quotient lifting procedure *}
 
 method_setup cleaning =
   {* Scan.succeed (fn ctxt => SIMPLE_METHOD (HEADGOAL (Quotient_Tacs.clean_tac ctxt))) *}
-  {* proves the cleaning goals from the quotient lifting procedure *}
+  {* prove the cleaning goals from the quotient lifting procedure *}
 
 attribute_setup quot_lifted =
   {* Scan.succeed Quotient_Tacs.lifted_attrib *}
-  {* lifts theorems to quotient types *}
+  {* lift theorems to quotient types *}
 
 no_notation
   rel_conj (infixr "OOO" 75) and
diff -r 6c841fa92fa2 -r 5af15f1e2ef6 src/HOL/SET_Protocol/Cardholder_Registration.thy
--- a/src/HOL/SET_Protocol/Cardholder_Registration.thy	Sun May 15 17:06:35 2011 +0200
+++ b/src/HOL/SET_Protocol/Cardholder_Registration.thy	Sun May 15 17:45:53 2011 +0200
@@ -541,7 +541,7 @@
       EVERY [ftac @{thm Gets_certificate_valid} i,
              assume_tac i,
              etac conjE i, REPEAT (hyp_subst_tac i)])))
-*} ""
+*}
 
 text{*The @{text "(no_asm)"} attribute is essential, since it retains
   the quantifier and allows the simprule's condition to itself be simplified.*}
diff -r 6c841fa92fa2 -r 5af15f1e2ef6 src/HOL/SET_Protocol/Purchase.thy
--- a/src/HOL/SET_Protocol/Purchase.thy	Sun May 15 17:06:35 2011 +0200
+++ b/src/HOL/SET_Protocol/Purchase.thy	Sun May 15 17:45:53 2011 +0200
@@ -484,7 +484,7 @@
     K (SIMPLE_METHOD'' quant (fn i =>
       EVERY [ftac @{thm Gets_certificate_valid} i,
              assume_tac i, REPEAT (hyp_subst_tac i)])))
-*} ""
+*}
 
 
 subsection{*Proofs on Symmetric Keys*}
diff -r 6c841fa92fa2 -r 5af15f1e2ef6 src/HOL/TLA/Action.thy
--- a/src/HOL/TLA/Action.thy	Sun May 15 17:06:35 2011 +0200
+++ b/src/HOL/TLA/Action.thy	Sun May 15 17:45:53 2011 +0200
@@ -120,9 +120,9 @@
     | _ => th;
 *}
 
-attribute_setup action_unlift = {* Scan.succeed (Thm.rule_attribute (K action_unlift)) *} ""
-attribute_setup action_rewrite = {* Scan.succeed (Thm.rule_attribute (K action_rewrite)) *} ""
-attribute_setup action_use = {* Scan.succeed (Thm.rule_attribute (K action_use)) *} ""
+attribute_setup action_unlift = {* Scan.succeed (Thm.rule_attribute (K action_unlift)) *}
+attribute_setup action_rewrite = {* Scan.succeed (Thm.rule_attribute (K action_rewrite)) *}
+attribute_setup action_use = {* Scan.succeed (Thm.rule_attribute (K action_use)) *}
 
 
 (* =========================== square / angle brackets =========================== *)
@@ -283,7 +283,7 @@
 
 method_setup enabled = {*
   Attrib.thm >> (fn th => fn ctxt => SIMPLE_METHOD' (enabled_tac ctxt th))
-*} ""
+*}
 
 (* Example *)
 
diff -r 6c841fa92fa2 -r 5af15f1e2ef6 src/HOL/TLA/Intensional.thy
--- a/src/HOL/TLA/Intensional.thy	Sun May 15 17:06:35 2011 +0200
+++ b/src/HOL/TLA/Intensional.thy	Sun May 15 17:45:53 2011 +0200
@@ -289,10 +289,10 @@
     | _ => th
 *}
 
-attribute_setup int_unlift = {* Scan.succeed (Thm.rule_attribute (K int_unlift)) *} ""
-attribute_setup int_rewrite = {* Scan.succeed (Thm.rule_attribute (K int_rewrite)) *} ""
-attribute_setup flatten = {* Scan.succeed (Thm.rule_attribute (K flatten)) *} ""
-attribute_setup int_use = {* Scan.succeed (Thm.rule_attribute (K int_use)) *} ""
+attribute_setup int_unlift = {* Scan.succeed (Thm.rule_attribute (K int_unlift)) *}
+attribute_setup int_rewrite = {* Scan.succeed (Thm.rule_attribute (K int_rewrite)) *}
+attribute_setup flatten = {* Scan.succeed (Thm.rule_attribute (K flatten)) *}
+attribute_setup int_use = {* Scan.succeed (Thm.rule_attribute (K int_use)) *}
 
 lemma Not_Rall: "|- (~(! x. F x)) = (? x. ~F x)"
   by (simp add: Valid_def)
diff -r 6c841fa92fa2 -r 5af15f1e2ef6 src/HOL/TLA/Memory/MemoryImplementation.thy
--- a/src/HOL/TLA/Memory/MemoryImplementation.thy	Sun May 15 17:06:35 2011 +0200
+++ b/src/HOL/TLA/Memory/MemoryImplementation.thy	Sun May 15 17:45:53 2011 +0200
@@ -803,7 +803,7 @@
 method_setup split_idle = {*
   Method.sections (Simplifier.simp_modifiers @ Splitter.split_modifiers)
     >> (K (SIMPLE_METHOD' o split_idle_tac))
-*} ""
+*}
 
 (* ----------------------------------------------------------------------
    Combine steps 1.2 and 1.4 to prove that the implementation satisfies
diff -r 6c841fa92fa2 -r 5af15f1e2ef6 src/HOL/TLA/TLA.thy
--- a/src/HOL/TLA/TLA.thy	Sun May 15 17:06:35 2011 +0200
+++ b/src/HOL/TLA/TLA.thy	Sun May 15 17:45:53 2011 +0200
@@ -128,10 +128,10 @@
 fun try_rewrite th = temp_rewrite th handle THM _ => temp_use th;
 *}
 
-attribute_setup temp_unlift = {* Scan.succeed (Thm.rule_attribute (K temp_unlift)) *} ""
-attribute_setup temp_rewrite = {* Scan.succeed (Thm.rule_attribute (K temp_rewrite)) *} ""
-attribute_setup temp_use = {* Scan.succeed (Thm.rule_attribute (K temp_use)) *} ""
-attribute_setup try_rewrite = {* Scan.succeed (Thm.rule_attribute (K try_rewrite)) *} ""
+attribute_setup temp_unlift = {* Scan.succeed (Thm.rule_attribute (K temp_unlift)) *}
+attribute_setup temp_rewrite = {* Scan.succeed (Thm.rule_attribute (K temp_rewrite)) *}
+attribute_setup temp_use = {* Scan.succeed (Thm.rule_attribute (K temp_use)) *}
+attribute_setup try_rewrite = {* Scan.succeed (Thm.rule_attribute (K try_rewrite)) *}
 
 
 (* Update classical reasoner---will be updated once more below! *)
@@ -310,10 +310,10 @@
                          eres_inst_tac ctxt [(("'a", 0), "state * state")] @{thm box_thin} i])
 *}
 
-method_setup merge_box = {* Scan.succeed (K (SIMPLE_METHOD' merge_box_tac)) *} ""
-method_setup merge_temp_box = {* Scan.succeed (SIMPLE_METHOD' o merge_temp_box_tac) *} ""
-method_setup merge_stp_box = {* Scan.succeed (SIMPLE_METHOD' o merge_stp_box_tac) *} ""
-method_setup merge_act_box = {* Scan.succeed (SIMPLE_METHOD' o merge_act_box_tac) *} ""
+method_setup merge_box = {* Scan.succeed (K (SIMPLE_METHOD' merge_box_tac)) *}
+method_setup merge_temp_box = {* Scan.succeed (SIMPLE_METHOD' o merge_temp_box_tac) *}
+method_setup merge_stp_box = {* Scan.succeed (SIMPLE_METHOD' o merge_stp_box_tac) *}
+method_setup merge_act_box = {* Scan.succeed (SIMPLE_METHOD' o merge_act_box_tac) *}
 
 (* rewrite rule to push universal quantification through box:
       (sigma |= [](! x. F x)) = (! x. (sigma |= []F x))
@@ -606,11 +606,11 @@
 
 method_setup invariant = {*
   Method.sections Clasimp.clasimp_modifiers >> (K (SIMPLE_METHOD' o inv_tac))
-*} ""
+*}
 
 method_setup auto_invariant = {*
   Method.sections Clasimp.clasimp_modifiers >> (K (SIMPLE_METHOD' o auto_inv_tac))
-*} ""
+*}
 
 lemma unless: "|- []($P --> P` | Q`) --> (stable P) | <>Q"
   apply (unfold dmd_def)
diff -r 6c841fa92fa2 -r 5af15f1e2ef6 src/HOL/UNITY/Comp/Alloc.thy
--- a/src/HOL/UNITY/Comp/Alloc.thy	Sun May 15 17:06:35 2011 +0200
+++ b/src/HOL/UNITY/Comp/Alloc.thy	Sun May 15 17:45:53 2011 +0200
@@ -326,7 +326,7 @@
 in
   Scan.succeed (Thm.rule_attribute (K normalized))
 end
-*} ""
+*}
 
 (*** bijectivity of sysOfAlloc [MUST BE AUTOMATED] ***)
 ML {*
@@ -342,9 +342,7 @@
 
 *}
 
-method_setup record_auto = {*
-  Scan.succeed (SIMPLE_METHOD o record_auto_tac)
-*} ""
+method_setup record_auto = {* Scan.succeed (SIMPLE_METHOD o record_auto_tac) *}
 
 lemma inj_sysOfAlloc [iff]: "inj sysOfAlloc"
   apply (unfold sysOfAlloc_def Let_def)
@@ -737,7 +735,7 @@
 method_setup rename_client_map = {*
   Scan.succeed (fn ctxt =>
     SIMPLE_METHOD (rename_client_map_tac (simpset_of ctxt)))
-*} ""
+*}
 
 text{*Lifting @{text Client_Increasing} to @{term systemState}*}
 lemma rename_Client_Increasing: "i : I
diff -r 6c841fa92fa2 -r 5af15f1e2ef6 src/HOL/ex/Binary.thy
--- a/src/HOL/ex/Binary.thy	Sun May 15 17:06:35 2011 +0200
+++ b/src/HOL/ex/Binary.thy	Sun May 15 17:45:53 2011 +0200
@@ -180,7 +180,7 @@
           @{simproc binary_nat_diff},
           @{simproc binary_nat_div},
           @{simproc binary_nat_mod}]))))
-*} "binary simplification"
+*}
 
 
 subsection {* Concrete syntax *}
diff -r 6c841fa92fa2 -r 5af15f1e2ef6 src/HOL/ex/Iff_Oracle.thy
--- a/src/HOL/ex/Iff_Oracle.thy	Sun May 15 17:06:35 2011 +0200
+++ b/src/HOL/ex/Iff_Oracle.thy	Sun May 15 17:45:53 2011 +0200
@@ -56,7 +56,7 @@
     SIMPLE_METHOD
       (HEADGOAL (rtac (iff_oracle (Proof_Context.theory_of ctxt, n)))
         handle Fail _ => no_tac))
-*} "iff oracle"
+*}
 
 
 lemma "A <-> A"
diff -r 6c841fa92fa2 -r 5af15f1e2ef6 src/Sequents/ILL.thy
--- a/src/Sequents/ILL.thy	Sun May 15 17:06:35 2011 +0200
+++ b/src/Sequents/ILL.thy	Sun May 15 17:45:53 2011 +0200
@@ -274,10 +274,10 @@
 
 
 method_setup best_safe =
-  {* Scan.succeed (K (SIMPLE_METHOD' (best_tac safe_cs))) *} ""
+  {* Scan.succeed (K (SIMPLE_METHOD' (best_tac safe_cs))) *}
 
 method_setup best_power =
-  {* Scan.succeed (K (SIMPLE_METHOD' (best_tac power_cs))) *} ""
+  {* Scan.succeed (K (SIMPLE_METHOD' (best_tac power_cs))) *}
 
 
 (* Some examples from Troelstra and van Dalen *)
diff -r 6c841fa92fa2 -r 5af15f1e2ef6 src/Sequents/LK0.thy
--- a/src/Sequents/LK0.thy	Sun May 15 17:06:35 2011 +0200
+++ b/src/Sequents/LK0.thy	Sun May 15 17:45:53 2011 +0200
@@ -225,25 +225,11 @@
     rtac (@{thm thinR} RS @{thm cut}) i THEN REPEAT (rtac @{thm thinL} i) THEN rtac th i;
 *}
 
-method_setup fast_prop =
-  {* Scan.succeed (K (SIMPLE_METHOD' (fast_tac prop_pack))) *}
-  "propositional reasoning"
-
-method_setup fast =
-  {* Scan.succeed (K (SIMPLE_METHOD' (fast_tac LK_pack))) *}
-  "classical reasoning"
-
-method_setup fast_dup =
-  {* Scan.succeed (K (SIMPLE_METHOD' (fast_tac LK_dup_pack))) *}
-  "classical reasoning"
-
-method_setup best =
-  {* Scan.succeed (K (SIMPLE_METHOD' (best_tac LK_pack))) *}
-  "classical reasoning"
-
-method_setup best_dup =
-  {* Scan.succeed (K (SIMPLE_METHOD' (best_tac LK_dup_pack))) *}
-  "classical reasoning"
+method_setup fast_prop = {* Scan.succeed (K (SIMPLE_METHOD' (fast_tac prop_pack))) *}
+method_setup fast = {* Scan.succeed (K (SIMPLE_METHOD' (fast_tac LK_pack))) *}
+method_setup fast_dup = {* Scan.succeed (K (SIMPLE_METHOD' (fast_tac LK_dup_pack))) *}
+method_setup best = {* Scan.succeed (K (SIMPLE_METHOD' (best_tac LK_pack))) *}
+method_setup best_dup = {* Scan.succeed (K (SIMPLE_METHOD' (best_tac LK_dup_pack))) *}
 
 
 lemma mp_R:
diff -r 6c841fa92fa2 -r 5af15f1e2ef6 src/Sequents/S4.thy
--- a/src/Sequents/S4.thy	Sun May 15 17:06:35 2011 +0200
+++ b/src/Sequents/S4.thy	Sun May 15 17:45:53 2011 +0200
@@ -43,8 +43,7 @@
 )
 *}
 
-method_setup S4_solve =
-  {* Scan.succeed (K (SIMPLE_METHOD (S4_Prover.solve_tac 2))) *} "S4 solver"
+method_setup S4_solve = {* Scan.succeed (K (SIMPLE_METHOD (S4_Prover.solve_tac 2))) *}
 
 
 (* Theorems of system T from Hughes and Cresswell and Hailpern, LNCS 129 *)
diff -r 6c841fa92fa2 -r 5af15f1e2ef6 src/Sequents/S43.thy
--- a/src/Sequents/S43.thy	Sun May 15 17:06:35 2011 +0200
+++ b/src/Sequents/S43.thy	Sun May 15 17:45:53 2011 +0200
@@ -92,7 +92,7 @@
 method_setup S43_solve = {*
   Scan.succeed (K (SIMPLE_METHOD
     (S43_Prover.solve_tac 2 ORELSE S43_Prover.solve_tac 3)))
-*} "S4 solver"
+*}
 
 
 (* Theorems of system T from Hughes and Cresswell and Hailpern, LNCS 129 *)
diff -r 6c841fa92fa2 -r 5af15f1e2ef6 src/Sequents/T.thy
--- a/src/Sequents/T.thy	Sun May 15 17:06:35 2011 +0200
+++ b/src/Sequents/T.thy	Sun May 15 17:45:53 2011 +0200
@@ -42,8 +42,7 @@
 )
 *}
 
-method_setup T_solve =
-  {* Scan.succeed (K (SIMPLE_METHOD (T_Prover.solve_tac 2))) *} "T solver"
+method_setup T_solve = {* Scan.succeed (K (SIMPLE_METHOD (T_Prover.solve_tac 2))) *}
 
 
 (* Theorems of system T from Hughes and Cresswell and Hailpern, LNCS 129 *)
diff -r 6c841fa92fa2 -r 5af15f1e2ef6 src/ZF/UNITY/Mutex.thy
--- a/src/ZF/UNITY/Mutex.thy	Sun May 15 17:06:35 2011 +0200
+++ b/src/ZF/UNITY/Mutex.thy	Sun May 15 17:45:53 2011 +0200
@@ -207,18 +207,18 @@
 
 lemma U_F1:
      "Mutex \<in> {s \<in> state. s`m=#1} LeadsTo {s \<in> state. s`p = s`v & s`m = #2}"
-by (unfold Mutex_def, ensures_tac U1)
+by (unfold Mutex_def, ensures U1)
 
 lemma U_F2: "Mutex \<in> {s \<in> state. s`p =0 & s`m = #2} LeadsTo {s \<in> state. s`m = #3}"
 apply (cut_tac IU)
-apply (unfold Mutex_def, ensures_tac U2)
+apply (unfold Mutex_def, ensures U2)
 done
 
 lemma U_F3: "Mutex \<in> {s \<in> state. s`m = #3} LeadsTo {s \<in> state. s`p=1}"
 apply (rule_tac B = "{s \<in> state. s`m = #4}" in LeadsTo_Trans)
  apply (unfold Mutex_def)
- apply (ensures_tac U3)
-apply (ensures_tac U4)
+ apply (ensures U3)
+apply (ensures U4)
 done
 
 
@@ -258,18 +258,18 @@
 by (unfold op_Unless_def Mutex_def, safety)
 
 lemma V_F1: "Mutex \<in> {s \<in> state. s`n=#1} LeadsTo {s \<in> state. s`p = not(s`u) & s`n = #2}"
-by (unfold Mutex_def, ensures_tac "V1")
+by (unfold Mutex_def, ensures "V1")
 
 lemma V_F2: "Mutex \<in> {s \<in> state. s`p=1 & s`n = #2} LeadsTo {s \<in> state. s`n = #3}"
 apply (cut_tac IV)
-apply (unfold Mutex_def, ensures_tac "V2")
+apply (unfold Mutex_def, ensures "V2")
 done
 
 lemma V_F3: "Mutex \<in> {s \<in> state. s`n = #3} LeadsTo {s \<in> state. s`p=0}"
 apply (rule_tac B = "{s \<in> state. s`n = #4}" in LeadsTo_Trans)
  apply (unfold Mutex_def)
- apply (ensures_tac V3)
-apply (ensures_tac V4)
+ apply (ensures V3)
+apply (ensures V4)
 done
 
 lemma V_lemma2: "Mutex \<in> {s \<in> state. s`n = #2} LeadsTo {s \<in> state. s`p=0}"
diff -r 6c841fa92fa2 -r 5af15f1e2ef6 src/ZF/UNITY/SubstAx.thy
--- a/src/ZF/UNITY/SubstAx.thy	Sun May 15 17:06:35 2011 +0200
+++ b/src/ZF/UNITY/SubstAx.thy	Sun May 15 17:45:53 2011 +0200
@@ -376,7 +376,7 @@
   end;
 *}
 
-method_setup ensures_tac = {*
+method_setup ensures = {*
     Args.goal_spec -- Scan.lift Args.name_source >>
     (fn (quant, s) => fn ctxt => SIMPLE_METHOD'' quant (ensures_tac ctxt s))
 *} "for proving progress properties"