--- 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')"
--- 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"
--- 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 *}
--- 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 *}
--- 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!)"
--- 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 *}
--- 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"
--- 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
--- 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
--- 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
--- 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)
--- 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. *}
--- 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)) *}
--- 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
--- 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.*}
--- 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*}
--- 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 *)
--- 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)
--- 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
--- 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)
--- 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
--- 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 *}
--- 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"
--- 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 *)
--- 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:
--- 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 *)
--- 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 *)
--- 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 *)
--- 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}"
--- 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"