--- a/src/HOL/Nat.thy Wed Oct 29 14:14:36 2014 +0100
+++ b/src/HOL/Nat.thy Wed Oct 29 14:40:14 2014 +0100
@@ -1599,8 +1599,6 @@
shows "u = s"
using 2 1 by (rule trans)
-setup Arith_Data.setup
-
ML_file "Tools/nat_arith.ML"
simproc_setup nateq_cancel_sums
--- a/src/HOL/Presburger.thy Wed Oct 29 14:14:36 2014 +0100
+++ b/src/HOL/Presburger.thy Wed Oct 29 14:40:14 2014 +0100
@@ -390,7 +390,6 @@
by (simp cong: conj_cong)
ML_file "Tools/Qelim/cooper.ML"
-setup Cooper.setup
method_setup presburger = {*
let
--- a/src/HOL/Product_Type.thy Wed Oct 29 14:14:36 2014 +0100
+++ b/src/HOL/Product_Type.thy Wed Oct 29 14:40:14 2014 +0100
@@ -784,7 +784,6 @@
by (simp only: internal_split_def split_conv)
ML_file "Tools/split_rule.ML"
-setup Split_Rule.setup
hide_const internal_split
--- a/src/HOL/Tools/Qelim/cooper.ML Wed Oct 29 14:14:36 2014 +0100
+++ b/src/HOL/Tools/Qelim/cooper.ML Wed Oct 29 14:40:14 2014 +0100
@@ -13,7 +13,6 @@
exception COOPER of string
val conv: Proof.context -> conv
val tac: bool -> thm list -> thm list -> Proof.context -> int -> tactic
- val setup: theory -> theory
end;
structure Cooper: COOPER =
@@ -835,6 +834,7 @@
[@{thm "split_zdiv"}, @{thm "split_zmod"}, @{thm "split_div'"},
@{thm "split_min"}, @{thm "split_max"}, @{thm "abs_split"}])
in
+
fun nat_to_int_tac ctxt =
simp_tac (put_simpset ss1 ctxt) THEN_ALL_NEW
simp_tac (put_simpset ss2 ctxt) THEN_ALL_NEW
@@ -842,16 +842,17 @@
fun div_mod_tac ctxt = simp_tac (put_simpset div_mod_ss ctxt);
fun splits_tac ctxt = simp_tac (put_simpset splits_ss ctxt);
+
end;
fun core_tac ctxt = CSUBGOAL (fn (p, i) =>
let
- val cpth =
+ val cpth =
if Config.get ctxt quick_and_dirty
then oracle (ctxt, Envir.beta_norm (Envir.eta_long [] (term_of (Thm.dest_arg p))))
else Conv.arg_conv (conv ctxt) p
- val p' = Thm.rhs_of cpth
- val th = Thm.implies_intr p' (Thm.equal_elim (Thm.symmetric cpth) (Thm.assume p'))
+ val p' = Thm.rhs_of cpth
+ val th = Thm.implies_intr p' (Thm.equal_elim (Thm.symmetric cpth) (Thm.assume p'))
in rtac th i end
handle COOPER _ => no_tac);
@@ -881,7 +882,7 @@
end 1);
-(* theory setup *)
+(* attribute syntax *)
local
@@ -896,11 +897,12 @@
in
-val setup =
- Attrib.setup @{binding presburger}
- ((Scan.lift (Args.$$$ "del") |-- optional (keyword constsN |-- terms)) >> del ||
- optional (keyword constsN |-- terms) >> add) "data for Cooper's algorithm"
- #> Arith_Data.add_tactic "Presburger arithmetic" (K (tac true [] []));
+val _ =
+ Theory.setup
+ (Attrib.setup @{binding presburger}
+ ((Scan.lift (Args.$$$ "del") |-- optional (keyword constsN |-- terms)) >> del ||
+ optional (keyword constsN |-- terms) >> add) "data for Cooper's algorithm"
+ #> Arith_Data.add_tactic "Presburger arithmetic" (K (tac true [] [])));
end;
--- a/src/HOL/Tools/arith_data.ML Wed Oct 29 14:14:36 2014 +0100
+++ b/src/HOL/Tools/arith_data.ML Wed Oct 29 14:40:14 2014 +0100
@@ -20,8 +20,6 @@
val prove_conv2: tactic -> (Proof.context -> tactic) -> Proof.context -> term * term -> thm
val simp_all_tac: thm list -> Proof.context -> tactic
val simplify_meta_eq: thm list -> Proof.context -> thm -> thm
-
- val setup: theory -> theory
end;
structure Arith_Data: ARITH_DATA =
@@ -48,14 +46,15 @@
val arith_tac = gen_arith_tac false;
val verbose_arith_tac = gen_arith_tac true;
-val setup =
- Method.setup @{binding arith}
- (Scan.succeed (fn ctxt =>
- METHOD (fn facts =>
- HEADGOAL
- (Method.insert_tac (rev (Named_Theorems.get ctxt @{named_theorems arith}) @ facts)
- THEN' verbose_arith_tac ctxt))))
- "various arithmetic decision procedures";
+val _ =
+ Theory.setup
+ (Method.setup @{binding arith}
+ (Scan.succeed (fn ctxt =>
+ METHOD (fn facts =>
+ HEADGOAL
+ (Method.insert_tac (rev (Named_Theorems.get ctxt @{named_theorems arith}) @ facts)
+ THEN' verbose_arith_tac ctxt))))
+ "various arithmetic decision procedures");
(* some specialized syntactic operations *)
--- a/src/HOL/Tools/split_rule.ML Wed Oct 29 14:14:36 2014 +0100
+++ b/src/HOL/Tools/split_rule.ML Wed Oct 29 14:40:14 2014 +0100
@@ -9,7 +9,6 @@
val split_rule_var: Proof.context -> term -> thm -> thm
val split_rule: Proof.context -> thm -> thm
val complete_split_rule: Proof.context -> thm -> thm
- val setup: theory -> theory
end;
structure Split_Rule: SPLIT_RULE =
@@ -110,14 +109,15 @@
(* attribute syntax *)
-val setup =
- Attrib.setup @{binding split_format}
- (Scan.lift (Args.parens (Args.$$$ "complete")
- >> K (Thm.rule_attribute (complete_split_rule o Context.proof_of))))
- "split pair-typed subterms in premises, or function arguments" #>
- Attrib.setup @{binding split_rule}
- (Scan.succeed (Thm.rule_attribute (split_rule o Context.proof_of)))
- "curries ALL function variables occurring in a rule's conclusion";
+val _ =
+ Theory.setup
+ (Attrib.setup @{binding split_format}
+ (Scan.lift (Args.parens (Args.$$$ "complete")
+ >> K (Thm.rule_attribute (complete_split_rule o Context.proof_of))))
+ "split pair-typed subterms in premises, or function arguments" #>
+ Attrib.setup @{binding split_rule}
+ (Scan.succeed (Thm.rule_attribute (split_rule o Context.proof_of)))
+ "curries ALL function variables occurring in a rule's conclusion");
end;