--- a/src/HOL/Library/Old_Recdef.thy Wed Oct 29 15:28:27 2014 +0100
+++ b/src/HOL/Library/Old_Recdef.thy Wed Oct 29 17:01:44 2014 +0100
@@ -68,7 +68,7 @@
ML_file "~~/src/HOL/Tools/TFL/tfl.ML"
ML_file "~~/src/HOL/Tools/TFL/post.ML"
ML_file "~~/src/HOL/Tools/recdef.ML"
-setup Recdef.setup
+
subsection {* Rule setup *}
--- a/src/HOL/Library/Old_SMT.thy Wed Oct 29 15:28:27 2014 +0100
+++ b/src/HOL/Library/Old_SMT.thy Wed Oct 29 17:01:44 2014 +0100
@@ -420,10 +420,7 @@
by auto
ML_file "Old_SMT/old_smt_real.ML"
-setup Old_SMT_Real.setup
-
ML_file "Old_SMT/old_smt_word.ML"
-setup Old_SMT_Word.setup
hide_type (open) pattern
hide_const fun_app term_true term_false z3div z3mod
--- a/src/HOL/Library/Old_SMT/old_smt_real.ML Wed Oct 29 15:28:27 2014 +0100
+++ b/src/HOL/Library/Old_SMT/old_smt_real.ML Wed Oct 29 17:01:44 2014 +0100
@@ -4,12 +4,7 @@
SMT setup for reals.
*)
-signature OLD_SMT_REAL =
-sig
- val setup: theory -> theory
-end
-
-structure Old_SMT_Real: OLD_SMT_REAL =
+structure Old_SMT_Real: sig end =
struct
@@ -125,12 +120,13 @@
(* setup *)
-val setup =
- Context.theory_map (
- Old_SMTLIB_Interface.add_logic (10, smtlib_logic) #>
- setup_builtins #>
- Old_Z3_Interface.add_mk_builtins z3_mk_builtins #>
- fold Old_Z3_Proof_Reconstruction.add_z3_rule real_rules #>
- Old_Z3_Proof_Tools.add_simproc real_linarith_proc)
+val _ =
+ Theory.setup
+ (Context.theory_map (
+ Old_SMTLIB_Interface.add_logic (10, smtlib_logic) #>
+ setup_builtins #>
+ Old_Z3_Interface.add_mk_builtins z3_mk_builtins #>
+ fold Old_Z3_Proof_Reconstruction.add_z3_rule real_rules #>
+ Old_Z3_Proof_Tools.add_simproc real_linarith_proc))
end
--- a/src/HOL/Library/Old_SMT/old_smt_word.ML Wed Oct 29 15:28:27 2014 +0100
+++ b/src/HOL/Library/Old_SMT/old_smt_word.ML Wed Oct 29 17:01:44 2014 +0100
@@ -4,12 +4,7 @@
SMT setup for words.
*)
-signature OLD_SMT_WORD =
-sig
- val setup: theory -> theory
-end
-
-structure Old_SMT_Word: OLD_SMT_WORD =
+structure Old_SMT_Word: sig end =
struct
open Word_Lib
@@ -143,9 +138,9 @@
(* setup *)
-val setup =
- Context.theory_map (
- Old_SMTLIB_Interface.add_logic (20, smtlib_logic) #>
- setup_builtins)
+val _ =
+ Theory.setup
+ (Context.theory_map
+ (Old_SMTLIB_Interface.add_logic (20, smtlib_logic) #> setup_builtins))
end
--- a/src/HOL/Library/Refute.thy Wed Oct 29 15:28:27 2014 +0100
+++ b/src/HOL/Library/Refute.thy Wed Oct 29 17:01:44 2014 +0100
@@ -13,7 +13,6 @@
begin
ML_file "refute.ML"
-setup Refute.setup
refute_params
[itself = 1,
--- a/src/HOL/Library/refute.ML Wed Oct 29 15:28:27 2014 +0100
+++ b/src/HOL/Library/refute.ML Wed Oct 29 17:01:44 2014 +0100
@@ -52,8 +52,6 @@
val refute_goal :
Proof.context -> (string * string) list -> thm -> int -> string
- val setup : theory -> theory
-
(* ------------------------------------------------------------------------- *)
(* Additional functions used by Nitpick (to be factored out) *)
(* ------------------------------------------------------------------------- *)
@@ -2926,37 +2924,33 @@
(* ------------------------------------------------------------------------- *)
-(* use 'setup Refute.setup' in an Isabelle theory to initialize the 'Refute' *)
-(* structure *)
-(* ------------------------------------------------------------------------- *)
-
-(* ------------------------------------------------------------------------- *)
(* Note: the interpreters and printers are used in reverse order; however, *)
(* an interpreter that can handle non-atomic terms ends up being *)
(* applied before the 'stlc_interpreter' breaks the term apart into *)
(* subterms that are then passed to other interpreters! *)
(* ------------------------------------------------------------------------- *)
(* FIXME formal @{const_name} for some entries (!??) *)
-val setup =
- add_interpreter "stlc" stlc_interpreter #>
- add_interpreter "Pure" Pure_interpreter #>
- add_interpreter "HOLogic" HOLogic_interpreter #>
- add_interpreter "set" set_interpreter #>
- add_interpreter "IDT" IDT_interpreter #>
- add_interpreter "IDT_constructor" IDT_constructor_interpreter #>
- add_interpreter "IDT_recursion" IDT_recursion_interpreter #>
- add_interpreter "Finite_Set.card" Finite_Set_card_interpreter #>
- add_interpreter "Finite_Set.finite" Finite_Set_finite_interpreter #>
- add_interpreter "Nat_Orderings.less" Nat_less_interpreter #>
- add_interpreter "Nat_HOL.plus" Nat_plus_interpreter #>
- add_interpreter "Nat_HOL.minus" Nat_minus_interpreter #>
- add_interpreter "Nat_HOL.times" Nat_times_interpreter #>
- add_interpreter "List.append" List_append_interpreter #>
- add_interpreter "Product_Type.prod.fst" Product_Type_fst_interpreter #>
- add_interpreter "Product_Type.prod.snd" Product_Type_snd_interpreter #>
- add_printer "stlc" stlc_printer #>
- add_printer "set" set_printer #>
- add_printer "IDT" IDT_printer;
+val _ =
+ Theory.setup
+ (add_interpreter "stlc" stlc_interpreter #>
+ add_interpreter "Pure" Pure_interpreter #>
+ add_interpreter "HOLogic" HOLogic_interpreter #>
+ add_interpreter "set" set_interpreter #>
+ add_interpreter "IDT" IDT_interpreter #>
+ add_interpreter "IDT_constructor" IDT_constructor_interpreter #>
+ add_interpreter "IDT_recursion" IDT_recursion_interpreter #>
+ add_interpreter "Finite_Set.card" Finite_Set_card_interpreter #>
+ add_interpreter "Finite_Set.finite" Finite_Set_finite_interpreter #>
+ add_interpreter "Nat_Orderings.less" Nat_less_interpreter #>
+ add_interpreter "Nat_HOL.plus" Nat_plus_interpreter #>
+ add_interpreter "Nat_HOL.minus" Nat_minus_interpreter #>
+ add_interpreter "Nat_HOL.times" Nat_times_interpreter #>
+ add_interpreter "List.append" List_append_interpreter #>
+ add_interpreter "Product_Type.prod.fst" Product_Type_fst_interpreter #>
+ add_interpreter "Product_Type.prod.snd" Product_Type_snd_interpreter #>
+ add_printer "stlc" stlc_printer #>
+ add_printer "set" set_printer #>
+ add_printer "IDT" IDT_printer);
--- a/src/HOL/NSA/StarDef.thy Wed Oct 29 15:28:27 2014 +0100
+++ b/src/HOL/NSA/StarDef.thy Wed Oct 29 17:01:44 2014 +0100
@@ -88,7 +88,6 @@
text {*Initialize transfer tactic.*}
ML_file "transfer.ML"
-setup Transfer_Principle.setup
method_setup transfer = {*
Attrib.thms >> (fn ths => fn ctxt =>
--- a/src/HOL/NSA/transfer.ML Wed Oct 29 15:28:27 2014 +0100
+++ b/src/HOL/NSA/transfer.ML Wed Oct 29 17:01:44 2014 +0100
@@ -8,7 +8,6 @@
sig
val transfer_tac: Proof.context -> thm list -> int -> tactic
val add_const: string -> theory -> theory
- val setup: theory -> theory
end;
structure Transfer_Principle: TRANSFER_PRINCIPLE =
@@ -106,12 +105,13 @@
(fn {intros,unfolds,refolds,consts} =>
{intros=intros, unfolds=unfolds, refolds=refolds, consts=c::consts}))
-val setup =
- Attrib.setup @{binding transfer_intro} (Attrib.add_del intro_add intro_del)
- "declaration of transfer introduction rule" #>
- Attrib.setup @{binding transfer_unfold} (Attrib.add_del unfold_add unfold_del)
- "declaration of transfer unfolding rule" #>
- Attrib.setup @{binding transfer_refold} (Attrib.add_del refold_add refold_del)
- "declaration of transfer refolding rule"
+val _ =
+ Theory.setup
+ (Attrib.setup @{binding transfer_intro} (Attrib.add_del intro_add intro_del)
+ "declaration of transfer introduction rule" #>
+ Attrib.setup @{binding transfer_unfold} (Attrib.add_del unfold_add unfold_del)
+ "declaration of transfer unfolding rule" #>
+ Attrib.setup @{binding transfer_refold} (Attrib.add_del refold_add refold_del)
+ "declaration of transfer refolding rule")
end;
--- a/src/HOL/Statespace/StateSpaceLocale.thy Wed Oct 29 15:28:27 2014 +0100
+++ b/src/HOL/Statespace/StateSpaceLocale.thy Wed Oct 29 17:01:44 2014 +0100
@@ -10,7 +10,6 @@
ML_file "state_space.ML"
ML_file "state_fun.ML"
-setup StateFun.setup
text {* For every type that is to be stored in a state space, an
instance of this locale is imported in order convert the abstract and
--- a/src/HOL/Statespace/state_fun.ML Wed Oct 29 15:28:27 2014 +0100
+++ b/src/HOL/Statespace/state_fun.ML Wed Oct 29 17:01:44 2014 +0100
@@ -16,8 +16,6 @@
val ex_lookup_ss : simpset
val lazy_conj_simproc : simproc
val string_eq_simp_tac : Proof.context -> int -> tactic
-
- val setup : theory -> theory
end;
structure StateFun: STATE_FUN =
@@ -107,8 +105,7 @@
(merge_ss (ss1, ss2), merge_ss (ex_ss1, ex_ss2), b1 orelse b2);
);
-val init_state_fun_data =
- Context.theory_map (Data.put (lookup_ss, ex_lookup_ss, false));
+val _ = Theory.setup (Context.theory_map (Data.put (lookup_ss, ex_lookup_ss, false)));
val lookup_simproc =
Simplifier.simproc_global @{theory} "lookup_simp" ["lookup d n (update d' c m v s)"]
@@ -370,29 +367,27 @@
val mk_constr = gen_constr_destr (fn a => fn b => Syntax.const @{const_name Fun.comp} $ a $ b) "";
val mk_destr = gen_constr_destr (fn a => fn b => Syntax.const @{const_name Fun.comp} $ b $ a) "the_";
-
-val statefun_simp_attr = Thm.declaration_attribute (fn thm => fn context =>
- let
- val ctxt = Context.proof_of context;
- val (lookup_ss, ex_lookup_ss, simprocs_active) = Data.get context;
- val (lookup_ss', ex_lookup_ss') =
- (case concl_of thm of
- (_ $ ((Const (@{const_name Ex}, _) $ _))) =>
- (lookup_ss, simpset_map ctxt (Simplifier.add_simp thm) ex_lookup_ss)
- | _ =>
- (simpset_map ctxt (Simplifier.add_simp thm) lookup_ss, ex_lookup_ss));
- val activate_simprocs =
- if simprocs_active then I
- else Simplifier.map_ss (fn ctxt => ctxt addsimprocs [lookup_simproc, update_simproc]);
- in
- context
- |> activate_simprocs
- |> Data.put (lookup_ss', ex_lookup_ss', true)
- end);
-
-val setup =
- init_state_fun_data #>
- Attrib.setup @{binding statefun_simp} (Scan.succeed statefun_simp_attr)
- "simplification in statespaces";
+val _ =
+ Theory.setup
+ (Attrib.setup @{binding statefun_simp}
+ (Scan.succeed (Thm.declaration_attribute (fn thm => fn context =>
+ let
+ val ctxt = Context.proof_of context;
+ val (lookup_ss, ex_lookup_ss, simprocs_active) = Data.get context;
+ val (lookup_ss', ex_lookup_ss') =
+ (case concl_of thm of
+ (_ $ ((Const (@{const_name Ex}, _) $ _))) =>
+ (lookup_ss, simpset_map ctxt (Simplifier.add_simp thm) ex_lookup_ss)
+ | _ =>
+ (simpset_map ctxt (Simplifier.add_simp thm) lookup_ss, ex_lookup_ss));
+ val activate_simprocs =
+ if simprocs_active then I
+ else Simplifier.map_ss (fn ctxt => ctxt addsimprocs [lookup_simproc, update_simproc]);
+ in
+ context
+ |> activate_simprocs
+ |> Data.put (lookup_ss', ex_lookup_ss', true)
+ end)))
+ "simplification in statespaces");
end;
--- a/src/HOL/Tools/recdef.ML Wed Oct 29 15:28:27 2014 +0100
+++ b/src/HOL/Tools/recdef.ML Wed Oct 29 17:01:44 2014 +0100
@@ -27,7 +27,6 @@
local_theory -> Proof.state
val recdef_tc_i: bstring * Token.src list -> string -> int option -> bool ->
local_theory -> Proof.state
- val setup: theory -> theory
end;
structure Recdef: RECDEF =
@@ -278,13 +277,14 @@
(* setup theory *)
-val setup =
- Attrib.setup @{binding recdef_simp} (Attrib.add_del simp_add simp_del)
- "declaration of recdef simp rule" #>
- Attrib.setup @{binding recdef_cong} (Attrib.add_del cong_add cong_del)
- "declaration of recdef cong rule" #>
- Attrib.setup @{binding recdef_wf} (Attrib.add_del wf_add wf_del)
- "declaration of recdef wf rule";
+val _ =
+ Theory.setup
+ (Attrib.setup @{binding recdef_simp} (Attrib.add_del simp_add simp_del)
+ "declaration of recdef simp rule" #>
+ Attrib.setup @{binding recdef_cong} (Attrib.add_del cong_add cong_del)
+ "declaration of recdef cong rule" #>
+ Attrib.setup @{binding recdef_wf} (Attrib.add_del wf_add wf_del)
+ "declaration of recdef wf rule");
(* outer syntax *)