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"