--- a/doc-src/LaTeXsugar/Sugar/Sugar.thy Thu Jan 19 15:45:10 2006 +0100
+++ b/doc-src/LaTeXsugar/Sugar/Sugar.thy Thu Jan 19 21:22:08 2006 +0100
@@ -389,7 +389,7 @@
setup {*
let
fun my_concl ctxt = Logic.strip_imp_concl
- in [TermStyle.add_style "my_concl" my_concl]
+ in TermStyle.add_style "my_concl" my_concl
end;
*}
(*>*)
@@ -399,7 +399,7 @@
\verb!setup {!\verb!*!\\
\verb!let!\\
\verb! fun my_concl ctxt = Logic.strip_imp_concl!\\
- \verb! in [TermStyle.add_style "my_concl" my_concl]!\\
+ \verb! in TermStyle.add_style "my_concl" my_concl!\\
\verb!end;!\\
\verb!*!\verb!}!\\
\end{quote}
--- a/src/FOL/IFOL.thy Thu Jan 19 15:45:10 2006 +0100
+++ b/src/FOL/IFOL.thy Thu Jan 19 21:22:08 2006 +0100
@@ -194,9 +194,7 @@
and [Pure.elim 2] = allE notE' impE'
and [Pure.intro] = exI disjI2 disjI1
-setup {*
- [ContextRules.addSWrapper (fn tac => hyp_subst_tac ORELSE' tac)]
-*}
+setup {* ContextRules.addSWrapper (fn tac => hyp_subst_tac ORELSE' tac) *}
lemma iff_not_sym: "~ (Q <-> P) ==> ~ (P <-> Q)"
--- a/src/FOL/cladata.ML Thu Jan 19 15:45:10 2006 +0100
+++ b/src/FOL/cladata.ML Thu Jan 19 21:22:08 2006 +0100
@@ -42,9 +42,9 @@
val FOL_cs = prop_cs addSIs [allI,ex_ex1I] addIs [exI]
addSEs [exE,alt_ex1E] addEs [allE];
-val cla_setup = [fn thy => (change_claset_of thy (fn _ => FOL_cs); thy)];
+val cla_setup = (fn thy => (change_claset_of thy (fn _ => FOL_cs); thy));
val case_setup =
- [Method.add_methods
+ (Method.add_methods
[("case_tac", Method.goal_args Args.name case_tac,
- "case_tac emulation (dynamic instantiation!)")]];
+ "case_tac emulation (dynamic instantiation!)")]);
--- a/src/FOL/simpdata.ML Thu Jan 19 15:45:10 2006 +0100
+++ b/src/FOL/simpdata.ML Thu Jan 19 21:22:08 2006 +0100
@@ -361,7 +361,7 @@
(*classical simprules too*)
val FOL_ss = IFOL_ss addsimps (cla_simps @ cla_ex_simps @ cla_all_simps);
-val simpsetup = [fn thy => (change_simpset_of thy (fn _ => FOL_ss); thy)];
+val simpsetup = (fn thy => (change_simpset_of thy (fn _ => FOL_ss); thy));
(*** integration of simplifier with classical reasoner ***)
--- a/src/HOL/Extraction.thy Thu Jan 19 15:45:10 2006 +0100
+++ b/src/HOL/Extraction.thy Thu Jan 19 21:22:08 2006 +0100
@@ -35,16 +35,16 @@
incr_boundvars 1 r $ (Const ("op :", elT --> setT --> HOLogic.boolT) $
Bound 0 $ incr_boundvars 1 s));
in
- [Extraction.add_types
+ Extraction.add_types
[("bool", ([], NONE)),
- ("set", ([realizes_set_proc], SOME mk_realizes_set))],
- Extraction.set_preprocessor (fn thy =>
+ ("set", ([realizes_set_proc], SOME mk_realizes_set))] #>
+ Extraction.set_preprocessor (fn thy =>
Proofterm.rewrite_proof_notypes
([], ("HOL/elim_cong", RewriteHOLProof.elim_cong) ::
ProofRewriteRules.rprocs true) o
Proofterm.rewrite_proof thy
(RewriteHOLProof.rews, ProofRewriteRules.rprocs true) o
- ProofRewriteRules.elim_vars (curry Const "arbitrary"))]
+ ProofRewriteRules.elim_vars (curry Const "arbitrary"))
end
*}
--- a/src/HOL/HOL.thy Thu Jan 19 15:45:10 2006 +0100
+++ b/src/HOL/HOL.thy Thu Jan 19 21:22:08 2006 +0100
@@ -911,9 +911,7 @@
use "cladata.ML"
setup hypsubst_setup
-setup {*
- [ContextRules.addSWrapper (fn tac => hyp_subst_tac' ORELSE' tac)]
-*}
+setup {* ContextRules.addSWrapper (fn tac => hyp_subst_tac' ORELSE' tac) *}
setup Classical.setup
setup clasetup
@@ -1233,7 +1231,7 @@
in
-val eq_codegen_setup = [Codegen.add_codegen "eq_codegen" eq_codegen];
+val eq_codegen_setup = Codegen.add_codegen "eq_codegen" eq_codegen;
end;
*}
--- a/src/HOL/Hyperreal/StarDef.thy Thu Jan 19 15:45:10 2006 +0100
+++ b/src/HOL/Hyperreal/StarDef.thy Thu Jan 19 21:22:08 2006 +0100
@@ -161,7 +161,7 @@
"star_of x \<equiv> star_n (\<lambda>n. x)"
text {* Transfer tactic should remove occurrences of @{term star_of} *}
-setup {* [Transfer.add_const "StarDef.star_of"] *}
+setup {* Transfer.add_const "StarDef.star_of" *}
declare star_of_def [transfer_intro]
lemma star_of_inject: "(star_of x = star_of y) = (x = y)"
@@ -184,7 +184,7 @@
UN_equiv_class2 [OF equiv_starrel equiv_starrel Ifun_congruent2])
text {* Transfer tactic should remove occurrences of @{term Ifun} *}
-setup {* [Transfer.add_const "StarDef.Ifun"] *}
+setup {* Transfer.add_const "StarDef.Ifun" *}
lemma transfer_Ifun [transfer_intro]:
"\<lbrakk>f \<equiv> star_n F; x \<equiv> star_n X\<rbrakk> \<Longrightarrow> f \<star> x \<equiv> star_n (\<lambda>n. F n (X n))"
@@ -234,7 +234,7 @@
by (simp add: unstar_def star_of_inject)
text {* Transfer tactic should remove occurrences of @{term unstar} *}
-setup {* [Transfer.add_const "StarDef.unstar"] *}
+setup {* Transfer.add_const "StarDef.unstar" *}
lemma transfer_unstar [transfer_intro]:
"p \<equiv> star_n P \<Longrightarrow> unstar p \<equiv> {n. P n} \<in> \<U>"
@@ -277,7 +277,7 @@
by (simp add: Iset_def starP2_star_n)
text {* Transfer tactic should remove occurrences of @{term Iset} *}
-setup {* [Transfer.add_const "StarDef.Iset"] *}
+setup {* Transfer.add_const "StarDef.Iset" *}
lemma transfer_mem [transfer_intro]:
"\<lbrakk>x \<equiv> star_n X; a \<equiv> Iset (star_n A)\<rbrakk>
--- a/src/HOL/Hyperreal/hypreal_arith.ML Thu Jan 19 15:45:10 2006 +0100
+++ b/src/HOL/Hyperreal/hypreal_arith.ML Thu Jan 19 21:22:08 2006 +0100
@@ -28,15 +28,15 @@
Fast_Arith.lin_arith_prover;
val hypreal_arith_setup =
- [Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
+ Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
{add_mono_thms = add_mono_thms,
mult_mono_thms = mult_mono_thms,
inj_thms = inj_thms @ real_inj_thms,
lessD = lessD, (*Can't change LA_Data_Ref.lessD: the hypreals are dense!*)
neqE = neqE,
- simpset = simpset}),
- arith_inj_const ("StarDef.star_of", HOLogic.realT --> hyprealT),
- fn thy => (change_simpset_of thy (fn ss => ss addsimprocs [fast_hypreal_arith_simproc]); thy)];
+ simpset = simpset}) #>
+ arith_inj_const ("StarDef.star_of", HOLogic.realT --> hyprealT) #>
+ (fn thy => (change_simpset_of thy (fn ss => ss addsimprocs [fast_hypreal_arith_simproc]); thy));
end;
--- a/src/HOL/Hyperreal/transfer.ML Thu Jan 19 15:45:10 2006 +0100
+++ b/src/HOL/Hyperreal/transfer.ML Thu Jan 19 21:22:08 2006 +0100
@@ -9,7 +9,7 @@
sig
val transfer_tac: thm list -> int -> tactic
val add_const: string -> theory -> theory
- val setup: (theory -> theory) list
+ val setup: theory -> theory
end;
structure Transfer: TRANSFER_TAC =
@@ -127,17 +127,15 @@
val transfer_method = Method.SIMPLE_METHOD' HEADGOAL o transfer_tac;
val setup =
- [ TransferData.init,
- Attrib.add_attributes
- [ ("transfer_intro", intro_attr,
- "declaration of transfer introduction rule"),
- ("transfer_unfold", unfold_attr,
- "declaration of transfer unfolding rule"),
- ("transfer_refold", refold_attr,
- "declaration of transfer refolding rule")
- ],
- Method.add_method
- ("transfer", Method.thms_args transfer_method, "transfer principle")
- ];
+ TransferData.init #>
+ Attrib.add_attributes
+ [("transfer_intro", intro_attr,
+ "declaration of transfer introduction rule"),
+ ("transfer_unfold", unfold_attr,
+ "declaration of transfer unfolding rule"),
+ ("transfer_refold", refold_attr,
+ "declaration of transfer refolding rule")] #>
+ Method.add_method
+ ("transfer", Method.thms_args transfer_method, "transfer principle");
end;
--- a/src/HOL/Import/hol4rews.ML Thu Jan 19 15:45:10 2006 +0100
+++ b/src/HOL/Import/hol4rews.ML Thu Jan 19 21:22:08 2006 +0100
@@ -758,24 +758,25 @@
|> add_hol4_const_mapping "min" "@" false "Hilbert_Choice.Eps"
in
val hol4_setup =
- [HOL4Rewrites.init,
- HOL4Maps.init,
- HOL4UNames.init,
- HOL4DefMaps.init,
- HOL4Moves.init,
- HOL4CMoves.init,
- HOL4ConstMaps.init,
- HOL4Rename.init,
- HOL4TypeMaps.init,
- HOL4Pending.init,
- HOL4Thms.init,
- HOL4Dump.init,
- HOL4DefThy.init,
- HOL4Imports.init,
- ImportSegment.init,
- initial_maps,
- Attrib.add_attributes [("hol4rew",
- (Attrib.no_args add_hol4_rewrite,
- Attrib.no_args Attrib.undef_local_attribute),
- "HOL4 rewrite rule")]]
+ HOL4Rewrites.init #>
+ HOL4Maps.init #>
+ HOL4UNames.init #>
+ HOL4DefMaps.init #>
+ HOL4Moves.init #>
+ HOL4CMoves.init #>
+ HOL4ConstMaps.init #>
+ HOL4Rename.init #>
+ HOL4TypeMaps.init #>
+ HOL4Pending.init #>
+ HOL4Thms.init #>
+ HOL4Dump.init #>
+ HOL4DefThy.init #>
+ HOL4Imports.init #>
+ ImportSegment.init #>
+ initial_maps #>
+ Attrib.add_attributes
+ [("hol4rew",
+ (Attrib.no_args add_hol4_rewrite,
+ Attrib.no_args Attrib.undef_local_attribute),
+ "HOL4 rewrite rule")]
end
--- a/src/HOL/Import/import_package.ML Thu Jan 19 15:45:10 2006 +0100
+++ b/src/HOL/Import/import_package.ML Thu Jan 19 21:22:08 2006 +0100
@@ -6,7 +6,7 @@
signature IMPORT_PACKAGE =
sig
val import_meth: Method.src -> Proof.context -> Proof.method
- val setup : (theory -> theory) list
+ val setup : theory -> theory
val debug : bool ref
end
@@ -80,6 +80,6 @@
Method.SIMPLE_METHOD (import_tac arg thy)
end)
-val setup = [Method.add_method("import",import_meth,"Import HOL4 theorem"),ImportData.init]
+val setup = Method.add_method("import",import_meth,"Import HOL4 theorem") #> ImportData.init
end
--- a/src/HOL/Import/shuffler.ML Thu Jan 19 15:45:10 2006 +0100
+++ b/src/HOL/Import/shuffler.ML Thu Jan 19 21:22:08 2006 +0100
@@ -26,7 +26,7 @@
val add_shuffle_rule: thm -> theory -> theory
val shuffle_attr: theory attribute
- val setup : (theory -> theory) list
+ val setup : theory -> theory
end
structure Shuffler :> Shuffler =
@@ -684,13 +684,15 @@
fun shuffle_attr (thy,thm) = (add_shuffle_rule thm thy,thm)
-val setup = [Method.add_method ("shuffle_tac",Method.thms_ctxt_args shuffle_meth,"solve goal by shuffling terms around"),
- Method.add_method ("search_tac",Method.ctxt_args search_meth,"search for suitable theorems"),
- ShuffleData.init,
- add_shuffle_rule weaken,
- add_shuffle_rule equiv_comm,
- add_shuffle_rule imp_comm,
- add_shuffle_rule Drule.norm_hhf_eq,
- add_shuffle_rule Drule.triv_forall_equality,
- Attrib.add_attributes [("shuffle_rule",(Attrib.no_args shuffle_attr,K Attrib.undef_local_attribute),"tell the shuffler about the theorem")]]
+val setup =
+ Method.add_method ("shuffle_tac",Method.thms_ctxt_args shuffle_meth,"solve goal by shuffling terms around") #>
+ Method.add_method ("search_tac",Method.ctxt_args search_meth,"search for suitable theorems") #>
+ ShuffleData.init #>
+ add_shuffle_rule weaken #>
+ add_shuffle_rule equiv_comm #>
+ add_shuffle_rule imp_comm #>
+ add_shuffle_rule Drule.norm_hhf_eq #>
+ add_shuffle_rule Drule.triv_forall_equality #>
+ Attrib.add_attributes [("shuffle_rule", (Attrib.no_args shuffle_attr,K Attrib.undef_local_attribute),"tell the shuffler about the theorem")]
+
end
--- a/src/HOL/Integ/IntDef.thy Thu Jan 19 15:45:10 2006 +0100
+++ b/src/HOL/Integ/IntDef.thy Thu Jan 19 21:22:08 2006 +0100
@@ -948,12 +948,12 @@
*}
-setup {*[
- Codegen.add_codegen "number_of_codegen" number_of_codegen,
+setup {*
+ Codegen.add_codegen "number_of_codegen" number_of_codegen #>
CodegenPackage.add_appconst
- ("Numeral.number_of", ((1, 1), CodegenPackage.appgen_number_of mk_int_to_nat bin_to_int "IntDef.int" "nat")),
+ ("Numeral.number_of", ((1, 1), CodegenPackage.appgen_number_of mk_int_to_nat bin_to_int "IntDef.int" "nat")) #>
CodegenPackage.set_int_tyco "IntDef.int"
-]*}
+*}
quickcheck_params [default_type = int]
--- a/src/HOL/Integ/NatBin.thy Thu Jan 19 15:45:10 2006 +0100
+++ b/src/HOL/Integ/NatBin.thy Thu Jan 19 21:22:08 2006 +0100
@@ -591,14 +591,14 @@
val numeral_ss = simpset() addsimps numerals;
val nat_bin_arith_setup =
- [Fast_Arith.map_data
+ Fast_Arith.map_data
(fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
{add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms,
inj_thms = inj_thms,
lessD = lessD, neqE = neqE,
simpset = simpset addsimps [Suc_nat_number_of, int_nat_number_of,
not_neg_number_of_Pls,
- neg_number_of_Min,neg_number_of_BIT]})]
+ neg_number_of_Min,neg_number_of_BIT]})
*}
setup nat_bin_arith_setup
--- a/src/HOL/Integ/int_arith1.ML Thu Jan 19 15:45:10 2006 +0100
+++ b/src/HOL/Integ/int_arith1.ML Thu Jan 19 21:22:08 2006 +0100
@@ -521,7 +521,7 @@
in
val int_arith_setup =
- [Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
+ Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
{add_mono_thms = add_mono_thms,
mult_mono_thms = [mult_strict_left_mono,mult_left_mono] @ mult_mono_thms,
inj_thms = [zle_int RS iffD2,int_int_eq RS iffD2] @ inj_thms,
@@ -529,10 +529,10 @@
neqE = thm "linorder_neqE_int" :: neqE,
simpset = simpset addsimps add_rules
addsimprocs simprocs
- addcongs [if_weak_cong]}),
- arith_inj_const ("IntDef.of_nat", HOLogic.natT --> HOLogic.intT),
- arith_inj_const ("IntDef.int", HOLogic.natT --> HOLogic.intT),
- arith_discrete "IntDef.int"];
+ addcongs [if_weak_cong]}) #>
+ arith_inj_const ("IntDef.of_nat", HOLogic.natT --> HOLogic.intT) #>
+ arith_inj_const ("IntDef.int", HOLogic.natT --> HOLogic.intT) #>
+ arith_discrete "IntDef.int";
end;
--- a/src/HOL/Integ/nat_simprocs.ML Thu Jan 19 15:45:10 2006 +0100
+++ b/src/HOL/Integ/nat_simprocs.ML Thu Jan 19 21:22:08 2006 +0100
@@ -554,10 +554,10 @@
in
val nat_simprocs_setup =
- [Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
+ Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
{add_mono_thms = add_mono_thms, mult_mono_thms = mult_mono_thms,
inj_thms = inj_thms, lessD = lessD, neqE = neqE,
simpset = simpset addsimps add_rules
- addsimprocs simprocs})];
+ addsimprocs simprocs});
end;
--- a/src/HOL/Integ/presburger.ML Thu Jan 19 15:45:10 2006 +0100
+++ b/src/HOL/Integ/presburger.ML Thu Jan 19 21:22:08 2006 +0100
@@ -14,7 +14,7 @@
sig
val presburger_tac : bool -> bool -> int -> tactic
val presburger_method : bool -> bool -> int -> Proof.method
- val setup : (theory -> theory) list
+ val setup : theory -> theory
val trace : bool ref
end;
@@ -364,12 +364,12 @@
Method.insert_tac facts 1 THEN presburger_tac q a i)
val setup =
- [Method.add_method ("presburger",
- presburger_args presburger_method,
- "decision procedure for Presburger arithmetic"),
- ArithTheoryData.map (fn {splits, inj_consts, discrete, presburger} =>
- {splits = splits, inj_consts = inj_consts, discrete = discrete,
- presburger = SOME (presburger_tac true true)})];
+ Method.add_method ("presburger",
+ presburger_args presburger_method,
+ "decision procedure for Presburger arithmetic") #>
+ ArithTheoryData.map (fn {splits, inj_consts, discrete, presburger} =>
+ {splits = splits, inj_consts = inj_consts, discrete = discrete,
+ presburger = SOME (presburger_tac true true)});
end;
--- a/src/HOL/Library/Commutative_Ring.thy Thu Jan 19 15:45:10 2006 +0100
+++ b/src/HOL/Library/Commutative_Ring.thy Thu Jan 19 21:22:08 2006 +0100
@@ -322,6 +322,6 @@
generate_code ("ring.ML") test = "norm"*)
use "comm_ring.ML"
-setup "CommRing.setup"
+setup CommRing.setup
end
--- a/src/HOL/Library/EfficientNat.thy Thu Jan 19 15:45:10 2006 +0100
+++ b/src/HOL/Library/EfficientNat.thy Thu Jan 19 21:22:08 2006 +0100
@@ -222,8 +222,8 @@
end;
val suc_preproc_setup =
- [Codegen.add_preprocessor eqn_suc_preproc,
- Codegen.add_preprocessor clause_suc_preproc];
+ Codegen.add_preprocessor eqn_suc_preproc #>
+ Codegen.add_preprocessor clause_suc_preproc;
*}
setup suc_preproc_setup
--- a/src/HOL/Library/comm_ring.ML Thu Jan 19 15:45:10 2006 +0100
+++ b/src/HOL/Library/comm_ring.ML Thu Jan 19 21:22:08 2006 +0100
@@ -9,7 +9,7 @@
val comm_ring_tac : int -> tactic
val comm_ring_method: int -> Proof.method
val algebra_method: int -> Proof.method
- val setup : (theory -> theory) list
+ val setup : theory -> theory
end
structure CommRing: COMM_RING =
@@ -132,11 +132,11 @@
val algebra_method = comm_ring_method;
val setup =
- [Method.add_method ("comm_ring",
+ Method.add_method ("comm_ring",
Method.no_args (comm_ring_method 1),
- "reflective decision procedure for equalities over commutative rings"),
- Method.add_method ("algebra",
+ "reflective decision procedure for equalities over commutative rings") #>
+ Method.add_method ("algebra",
Method.no_args (algebra_method 1),
- "Method for proving algebraic properties: for now only comm_ring")];
+ "Method for proving algebraic properties: for now only comm_ring");
end;
--- a/src/HOL/Library/word_setup.ML Thu Jan 19 15:45:10 2006 +0100
+++ b/src/HOL/Library/word_setup.ML Thu Jan 19 21:22:08 2006 +0100
@@ -42,5 +42,5 @@
thy
end
in
-val setup_word = [add_word]
+val setup_word = add_word
end
--- a/src/HOL/List.thy Thu Jan 19 15:45:10 2006 +0100
+++ b/src/HOL/List.thy Thu Jan 19 21:22:08 2006 +0100
@@ -2652,14 +2652,12 @@
in
-val list_codegen_setup = [
- Codegen.add_codegen "list_codegen" list_codegen,
- Codegen.add_codegen "char_codegen" char_codegen,
+val list_codegen_setup =
+ Codegen.add_codegen "list_codegen" list_codegen #>
+ Codegen.add_codegen "char_codegen" char_codegen #>
fold (CodegenPackage.add_pretty_list "Nil" "Cons") [
("ml", (7, "::")),
- ("haskell", (5, ":"))
- ]
-];
+ ("haskell", (5, ":"))];
end;
*}
@@ -2705,6 +2703,6 @@
setup list_codegen_setup
-setup "[CodegenPackage.rename_inconsistent]"
+setup CodegenPackage.rename_inconsistent
end
--- a/src/HOL/Product_Type.thy Thu Jan 19 15:45:10 2006 +0100
+++ b/src/HOL/Product_Type.thy Thu Jan 19 21:22:08 2006 +0100
@@ -885,14 +885,13 @@
in
-val prod_codegen_setup = [
- Codegen.add_codegen "let_codegen" let_codegen,
- Codegen.add_codegen "split_codegen" split_codegen,
+val prod_codegen_setup =
+ Codegen.add_codegen "let_codegen" let_codegen #>
+ Codegen.add_codegen "split_codegen" split_codegen #>
CodegenPackage.add_appconst
- ("Let", ((2, 2), CodegenPackage.appgen_let strip_abs)),
+ ("Let", ((2, 2), CodegenPackage.appgen_let strip_abs)) #>
CodegenPackage.add_appconst
- ("split", ((1, 1), CodegenPackage.appgen_split strip_abs))
-];
+ ("split", ((1, 1), CodegenPackage.appgen_split strip_abs));
end;
*}
--- a/src/HOL/Real/rat_arith.ML Thu Jan 19 15:45:10 2006 +0100
+++ b/src/HOL/Real/rat_arith.ML Thu Jan 19 21:22:08 2006 +0100
@@ -38,17 +38,16 @@
val ratT = Type("Rational.rat", []);
val rat_arith_setup =
- [Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD,
- neqE, simpset} =>
+ Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
{add_mono_thms = add_mono_thms,
mult_mono_thms = mult_mono_thms,
inj_thms = int_inj_thms @ inj_thms,
lessD = lessD, (*Can't change LA_Data_Ref.lessD: the rats are dense!*)
neqE = neqE,
simpset = simpset addsimps simps
- addsimprocs simprocs}),
- arith_inj_const("IntDef.of_nat", HOLogic.natT --> ratT),
- arith_inj_const("IntDef.of_int", HOLogic.intT --> ratT),
- fn thy => (change_simpset_of thy (fn ss => ss addsimprocs [fast_rat_arith_simproc]); thy)];
+ addsimprocs simprocs}) #>
+ arith_inj_const("IntDef.of_nat", HOLogic.natT --> ratT) #>
+ arith_inj_const("IntDef.of_int", HOLogic.intT --> ratT) #>
+ (fn thy => (change_simpset_of thy (fn ss => ss addsimprocs [fast_rat_arith_simproc]); thy));
end;
--- a/src/HOL/Real/real_arith.ML Thu Jan 19 15:45:10 2006 +0100
+++ b/src/HOL/Real/real_arith.ML Thu Jan 19 21:22:08 2006 +0100
@@ -118,16 +118,16 @@
Fast_Arith.lin_arith_prover;
val real_arith_setup =
- [Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
+ Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, neqE, simpset} =>
{add_mono_thms = add_mono_thms,
mult_mono_thms = mult_mono_thms,
inj_thms = int_inj_thms @ nat_inj_thms @ inj_thms,
lessD = lessD, (*Can't change LA_Data_Ref.lessD: the reals are dense!*)
neqE = neqE,
- simpset = simpset addsimps simps}),
- arith_inj_const ("RealDef.real", HOLogic.natT --> HOLogic.realT),
- arith_inj_const ("RealDef.real", HOLogic.intT --> HOLogic.realT),
- fn thy => (change_simpset_of thy (fn ss => ss addsimprocs [fast_real_arith_simproc]); thy)];
+ simpset = simpset addsimps simps}) #>
+ arith_inj_const ("RealDef.real", HOLogic.natT --> HOLogic.realT) #>
+ arith_inj_const ("RealDef.real", HOLogic.intT --> HOLogic.realT) #>
+ (fn thy => (change_simpset_of thy (fn ss => ss addsimprocs [fast_real_arith_simproc]); thy));
(* some thms for injection nat => real:
real_of_nat_zero
--- a/src/HOL/Tools/Presburger/presburger.ML Thu Jan 19 15:45:10 2006 +0100
+++ b/src/HOL/Tools/Presburger/presburger.ML Thu Jan 19 21:22:08 2006 +0100
@@ -14,7 +14,7 @@
sig
val presburger_tac : bool -> bool -> int -> tactic
val presburger_method : bool -> bool -> int -> Proof.method
- val setup : (theory -> theory) list
+ val setup : theory -> theory
val trace : bool ref
end;
@@ -364,12 +364,12 @@
Method.insert_tac facts 1 THEN presburger_tac q a i)
val setup =
- [Method.add_method ("presburger",
- presburger_args presburger_method,
- "decision procedure for Presburger arithmetic"),
- ArithTheoryData.map (fn {splits, inj_consts, discrete, presburger} =>
- {splits = splits, inj_consts = inj_consts, discrete = discrete,
- presburger = SOME (presburger_tac true true)})];
+ Method.add_method ("presburger",
+ presburger_args presburger_method,
+ "decision procedure for Presburger arithmetic") #>
+ ArithTheoryData.map (fn {splits, inj_consts, discrete, presburger} =>
+ {splits = splits, inj_consts = inj_consts, discrete = discrete,
+ presburger = SOME (presburger_tac true true)});
end;
--- a/src/HOL/Tools/datatype_codegen.ML Thu Jan 19 15:45:10 2006 +0100
+++ b/src/HOL/Tools/datatype_codegen.ML Thu Jan 19 21:22:08 2006 +0100
@@ -7,7 +7,7 @@
signature DATATYPE_CODEGEN =
sig
- val setup: (theory -> theory) list
+ val setup: theory -> theory
end;
structure DatatypeCodegen : DATATYPE_CODEGEN =
@@ -297,18 +297,17 @@
| datatype_tycodegen _ _ _ _ _ _ _ = NONE;
-val setup = [
- add_codegen "datatype" datatype_codegen,
- add_tycodegen "datatype" datatype_tycodegen,
+val setup =
+ add_codegen "datatype" datatype_codegen #>
+ add_tycodegen "datatype" datatype_tycodegen #>
CodegenPackage.set_is_datatype
- DatatypePackage.is_datatype,
+ DatatypePackage.is_datatype #>
CodegenPackage.set_get_all_datatype_cons
- DatatypePackage.get_all_datatype_cons,
+ DatatypePackage.get_all_datatype_cons #>
CodegenPackage.add_defgen
- ("datatype", CodegenPackage.defgen_datatype DatatypePackage.get_datatype DatatypePackage.get_datatype_cons),
+ ("datatype", CodegenPackage.defgen_datatype DatatypePackage.get_datatype DatatypePackage.get_datatype_cons) #>
CodegenPackage.ensure_datatype_case_consts
DatatypePackage.get_datatype_case_consts
- DatatypePackage.get_case_const_data
-];
+ DatatypePackage.get_case_const_data;
end;
--- a/src/HOL/Tools/datatype_package.ML Thu Jan 19 15:45:10 2006 +0100
+++ b/src/HOL/Tools/datatype_package.ML Thu Jan 19 21:22:08 2006 +0100
@@ -75,7 +75,7 @@
val constrs_of : theory -> string -> term list option
val case_const_of : theory -> string -> term option
val weak_case_congs_of : theory -> thm list
- val setup: (theory -> theory) list
+ val setup: theory -> theory
end;
structure DatatypePackage : DATATYPE_PACKAGE =
@@ -433,8 +433,8 @@
val dist_ss = HOL_ss addsimprocs [distinct_simproc];
val simproc_setup =
- [Theory.add_oracle (distinctN, fn (_, ConstrDistinct t) => t),
- fn thy => ((change_simpset_of thy) (fn ss => ss addsimprocs [distinct_simproc]); thy)];
+ Theory.add_oracle (distinctN, fn (_, ConstrDistinct t) => t) #>
+ (fn thy => ((change_simpset_of thy) (fn ss => ss addsimprocs [distinct_simproc]); thy));
(**** translation rules for case ****)
@@ -545,7 +545,7 @@
(NameSpace.accesses' case_name)) (descr ~~ case_names));
val trfun_setup =
- [Theory.add_advanced_trfuns ([], [("_case_syntax", case_tr)], [], [])];
+ Theory.add_advanced_trfuns ([], [("_case_syntax", case_tr)], [], []);
(* prepare types *)
@@ -1019,7 +1019,8 @@
(* setup theory *)
-val setup = [DatatypesData.init, Method.add_methods tactic_emulations] @ simproc_setup @ trfun_setup;
+val setup =
+ DatatypesData.init #> Method.add_methods tactic_emulations #> simproc_setup #> trfun_setup;
(* outer syntax *)
--- a/src/HOL/Tools/inductive_codegen.ML Thu Jan 19 15:45:10 2006 +0100
+++ b/src/HOL/Tools/inductive_codegen.ML Thu Jan 19 21:22:08 2006 +0100
@@ -8,7 +8,7 @@
signature INDUCTIVE_CODEGEN =
sig
val add : string option -> theory attribute
- val setup : (theory -> theory) list
+ val setup : theory -> theory
end;
structure InductiveCodegen : INDUCTIVE_CODEGEN =
@@ -732,10 +732,9 @@
| _ => NONE);
val setup =
- [add_codegen "inductive" inductive_codegen,
- CodegenData.init,
- add_attribute "ind"
- (Scan.option (Args.$$$ "target" |-- Args.colon |-- Args.name) >> add)];
+ add_codegen "inductive" inductive_codegen #>
+ CodegenData.init #>
+ add_attribute "ind" (Scan.option (Args.$$$ "target" |-- Args.colon |-- Args.name) >> add);
end;
--- a/src/HOL/Tools/inductive_package.ML Thu Jan 19 15:45:10 2006 +0100
+++ b/src/HOL/Tools/inductive_package.ML Thu Jan 19 21:22:08 2006 +0100
@@ -55,7 +55,7 @@
theory -> theory *
{defs: thm list, elims: thm list, raw_induct: thm, induct: thm,
intrs: thm list, mk_cases: string -> thm, mono: thm, unfold: thm}
- val setup: (theory -> theory) list
+ val setup: theory -> theory
end;
structure InductivePackage: INDUCTIVE_PACKAGE =
@@ -868,10 +868,10 @@
(* setup theory *)
val setup =
- [InductiveData.init,
+ InductiveData.init #>
Method.add_methods [("ind_cases", mk_cases_meth oo mk_cases_args,
- "dynamic case analysis on sets")],
- Attrib.add_attributes [("mono", mono_attr, "declaration of monotonicity rule")]];
+ "dynamic case analysis on sets")] #>
+ Attrib.add_attributes [("mono", mono_attr, "declaration of monotonicity rule")];
(* outer syntax *)
--- a/src/HOL/Tools/inductive_realizer.ML Thu Jan 19 15:45:10 2006 +0100
+++ b/src/HOL/Tools/inductive_realizer.ML Thu Jan 19 21:22:08 2006 +0100
@@ -9,7 +9,7 @@
signature INDUCTIVE_REALIZER =
sig
val add_ind_realizers: string -> string list -> theory -> theory
- val setup: (theory -> theory) list
+ val setup: theory -> theory
end;
structure InductiveRealizer : INDUCTIVE_REALIZER =
@@ -487,9 +487,10 @@
Scan.option (Scan.lift (Args.colon) |--
Scan.repeat1 Args.global_const))) >> rlz_attrib);
-val setup = [Attrib.add_attributes [("ind_realizer",
- (rlz_attrib_global, K Attrib.undef_local_attribute),
- "add realizers for inductive set")]];
+val setup =
+ Attrib.add_attributes [("ind_realizer",
+ (rlz_attrib_global, K Attrib.undef_local_attribute),
+ "add realizers for inductive set")];
end;
--- a/src/HOL/Tools/meson.ML Thu Jan 19 15:45:10 2006 +0100
+++ b/src/HOL/Tools/meson.ML Thu Jan 19 21:22:08 2006 +0100
@@ -590,11 +590,11 @@
val make_clauses_meth = Method.SIMPLE_METHOD' HEADGOAL make_clauses_tac;
val skolemize_setup =
- [Method.add_methods
- [("skolemize", Method.no_args skolemize_meth,
- "Skolemization into existential quantifiers"),
- ("make_clauses", Method.no_args make_clauses_meth,
- "Conversion to !!-quantified meta-level clauses")]];
+ Method.add_methods
+ [("skolemize", Method.no_args skolemize_meth,
+ "Skolemization into existential quantifiers"),
+ ("make_clauses", Method.no_args make_clauses_meth,
+ "Conversion to !!-quantified meta-level clauses")];
end;
--- a/src/HOL/Tools/numeral_syntax.ML Thu Jan 19 15:45:10 2006 +0100
+++ b/src/HOL/Tools/numeral_syntax.ML Thu Jan 19 21:22:08 2006 +0100
@@ -8,7 +8,7 @@
signature NUMERAL_SYNTAX =
sig
- val setup: (theory -> theory) list
+ val setup: theory -> theory
end;
structure NumeralSyntax: NUMERAL_SYNTAX =
@@ -55,9 +55,9 @@
(* theory setup *)
val setup =
- [Theory.hide_consts_i false ["Numeral.Pls", "Numeral.Min"],
- Theory.hide_consts_i false ["Numeral.bit.B0", "Numeral.bit.B1"],
- Theory.add_trfuns ([], [("_Numeral", numeral_tr)], [], []),
- Theory.add_trfunsT [("number_of", numeral_tr'), ("Numeral.number_of", numeral_tr')]];
+ Theory.hide_consts_i false ["Numeral.Pls", "Numeral.Min"] #>
+ Theory.hide_consts_i false ["Numeral.bit.B0", "Numeral.bit.B1"] #>
+ Theory.add_trfuns ([], [("_Numeral", numeral_tr)], [], []) #>
+ Theory.add_trfunsT [("number_of", numeral_tr'), ("Numeral.number_of", numeral_tr')];
end;
--- a/src/HOL/Tools/recdef_package.ML Thu Jan 19 15:45:10 2006 +0100
+++ b/src/HOL/Tools/recdef_package.ML Thu Jan 19 21:22:08 2006 +0100
@@ -29,7 +29,7 @@
val recdef_tc: bstring * Attrib.src list -> xstring -> int option -> theory -> Proof.state
val recdef_tc_i: bstring * theory attribute list -> string -> int option
-> theory -> Proof.state
- val setup: (theory -> theory) list
+ val setup: theory -> theory
end;
structure RecdefPackage: RECDEF_PACKAGE =
@@ -294,14 +294,15 @@
(* setup theory *)
val setup =
- [GlobalRecdefData.init, LocalRecdefData.init,
+ GlobalRecdefData.init #>
+ LocalRecdefData.init #>
Attrib.add_attributes
[(recdef_simpN, Attrib.common (Attrib.add_del_args simp_add simp_del),
"declaration of recdef simp rule"),
(recdef_congN, Attrib.common (Attrib.add_del_args cong_add cong_del),
"declaration of recdef cong rule"),
(recdef_wfN, Attrib.common (Attrib.add_del_args wf_add wf_del),
- "declaration of recdef wf rule")]];
+ "declaration of recdef wf rule")];
(* outer syntax *)
--- a/src/HOL/Tools/recfun_codegen.ML Thu Jan 19 15:45:10 2006 +0100
+++ b/src/HOL/Tools/recfun_codegen.ML Thu Jan 19 21:22:08 2006 +0100
@@ -11,7 +11,7 @@
val del: theory attribute
val get_rec_equations: theory -> string * typ -> (term list * term) list * typ
val get_thm_equations: theory -> string * typ -> (thm list * typ) option
- val setup: (theory -> theory) list
+ val setup: theory -> theory
end;
structure RecfunCodegen : RECFUN_CODEGEN =
@@ -191,14 +191,13 @@
| _ => NONE);
-val setup = [
- CodegenData.init,
- add_codegen "recfun" recfun_codegen,
+val setup =
+ CodegenData.init #>
+ add_codegen "recfun" recfun_codegen #>
add_attribute ""
( Args.del |-- Scan.succeed del
- || Scan.option (Args.$$$ "target" |-- Args.colon |-- Args.name) >> add),
+ || Scan.option (Args.$$$ "target" |-- Args.colon |-- Args.name) >> add) #>
CodegenPackage.add_eqextr
- ("rec", fn thy => fn _ => get_thm_equations thy)
-];
+ ("rec", fn thy => fn _ => get_thm_equations thy);
end;
--- a/src/HOL/Tools/reconstruction.ML Thu Jan 19 15:45:10 2006 +0100
+++ b/src/HOL/Tools/reconstruction.ML Thu Jan 19 21:22:08 2006 +0100
@@ -132,12 +132,12 @@
(** theory setup **)
val setup =
- [Attrib.add_attributes
- [("binary", (binary_global, binary_local), "binary resolution"),
- ("paramod", (paramod_global, paramod_local), "paramodulation"),
- ("demod", (demod_global, demod_local), "demodulation"),
- ("factor", (factor, factor), "factoring"),
- ("clausify", (clausify, clausify), "conversion to clauses")]];
+ Attrib.add_attributes
+ [("binary", (binary_global, binary_local), "binary resolution"),
+ ("paramod", (paramod_global, paramod_local), "paramodulation"),
+ ("demod", (demod_global, demod_local), "demodulation"),
+ ("factor", (factor, factor), "factoring"),
+ ("clausify", (clausify, clausify), "conversion to clauses")];
end
end
--- a/src/HOL/Tools/record_package.ML Thu Jan 19 15:45:10 2006 +0100
+++ b/src/HOL/Tools/record_package.ML Thu Jan 19 21:22:08 2006 +0100
@@ -39,7 +39,7 @@
-> theory -> theory
val add_record_i: string list * string -> (typ list * string) option
-> (string * typ * mixfix) list -> theory -> theory
- val setup: (theory -> theory) list
+ val setup: theory -> theory
end;
@@ -2098,11 +2098,11 @@
(* setup theory *)
val setup =
- [RecordsData.init,
- Theory.add_trfuns ([], parse_translation, [], []),
- Theory.add_advanced_trfuns ([], adv_parse_translation, [], []),
+ RecordsData.init #>
+ Theory.add_trfuns ([], parse_translation, [], []) #>
+ Theory.add_advanced_trfuns ([], adv_parse_translation, [], []) #>
(fn thy => (Simplifier.change_simpset_of thy
- (fn ss => ss addsimprocs [record_simproc, record_upd_simproc, record_eq_simproc]); thy))];
+ (fn ss => ss addsimprocs [record_simproc, record_upd_simproc, record_eq_simproc]); thy));
(* outer syntax *)
--- a/src/HOL/Tools/refute.ML Thu Jan 19 15:45:10 2006 +0100
+++ b/src/HOL/Tools/refute.ML Thu Jan 19 21:22:08 2006 +0100
@@ -50,7 +50,7 @@
val refute_term : theory -> (string * string) list -> Term.term -> unit (* tries to find a model that refutes a formula *)
val refute_subgoal : theory -> (string * string) list -> Thm.thm -> int -> unit
- val setup : (theory -> theory) list
+ val setup : theory -> theory
end;
structure Refute : REFUTE =
@@ -2605,25 +2605,25 @@
(* (theory -> theory) list *)
val setup =
- [RefuteData.init,
- 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.Finites" Finite_Set_Finites_interpreter,
- add_interpreter "Nat.op <" Nat_less_interpreter,
- add_interpreter "Nat.op +" Nat_plus_interpreter,
- add_interpreter "Nat.op -" Nat_minus_interpreter,
- add_interpreter "Nat.op *" Nat_mult_interpreter,
- add_interpreter "List.op @" List_append_interpreter,
- add_interpreter "Lfp.lfp" Lfp_lfp_interpreter,
- add_interpreter "Gfp.gfp" Gfp_gfp_interpreter,
- add_printer "stlc" stlc_printer,
- add_printer "set" set_printer,
- add_printer "IDT" IDT_printer];
+ RefuteData.init #>
+ 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.Finites" Finite_Set_Finites_interpreter #>
+ add_interpreter "Nat.op <" Nat_less_interpreter #>
+ add_interpreter "Nat.op +" Nat_plus_interpreter #>
+ add_interpreter "Nat.op -" Nat_minus_interpreter #>
+ add_interpreter "Nat.op *" Nat_mult_interpreter #>
+ add_interpreter "List.op @" List_append_interpreter #>
+ add_interpreter "Lfp.lfp" Lfp_lfp_interpreter #>
+ add_interpreter "Gfp.gfp" Gfp_gfp_interpreter #>
+ add_printer "stlc" stlc_printer #>
+ add_printer "set" set_printer #>
+ add_printer "IDT" IDT_printer;
end
--- a/src/HOL/Tools/res_atp_methods.ML Thu Jan 19 15:45:10 2006 +0100
+++ b/src/HOL/Tools/res_atp_methods.ML Thu Jan 19 21:22:08 2006 +0100
@@ -46,16 +46,13 @@
val eproverH_tac = res_atp_tac eprover_oracle ResAtpSetup.Hol (!eprover_time);
-val ResAtps_setup = [Method.add_methods
- [("vampireF", ResAtpSetup.atp_method vampireF_tac, "A Vampire method for FOL problems"),
- ("eproverF", ResAtpSetup.atp_method eproverF_tac, "A E prover method for FOL problems"),
- ("vampireH",ResAtpSetup.atp_method vampireH_tac, "A Vampire method for HOL problems"),
- ("eproverH",ResAtpSetup.atp_method eproverH_tac,"A E prover method for HOL problems"),
- ("eprover",ResAtpSetup.atp_method eprover_tac,"A E prover method for FOL and HOL problems"),
- ("vampire",ResAtpSetup.atp_method vampire_tac,"A Vampire method for FOL and HOL problems")
-]];
-
-
-
+val ResAtps_setup =
+ Method.add_methods
+ [("vampireF", ResAtpSetup.atp_method vampireF_tac, "Vampire for FOL problems"),
+ ("eproverF", ResAtpSetup.atp_method eproverF_tac, "E prover for FOL problems"),
+ ("vampireH", ResAtpSetup.atp_method vampireH_tac, "Vampire for HOL problems"),
+ ("eproverH", ResAtpSetup.atp_method eproverH_tac, "E prover for HOL problems"),
+ ("eprover", ResAtpSetup.atp_method eprover_tac, "E prover for FOL and HOL problems"),
+ ("vampire", ResAtpSetup.atp_method vampire_tac, "Vampire for FOL and HOL problems")];
end
--- a/src/HOL/Tools/res_axioms.ML Thu Jan 19 15:45:10 2006 +0100
+++ b/src/HOL/Tools/res_axioms.ML Thu Jan 19 21:22:08 2006 +0100
@@ -27,8 +27,8 @@
val cnf_rules1 : (string * thm) list -> string list -> (string * thm list) list * string list
val cnf_rules2 : (string * thm) list -> string list -> (string * term list) list * string list
- val meson_method_setup : (theory -> theory) list (*Reconstruction.thy*)
- val setup : (theory -> theory) list (*Main.thy*)
+ val meson_method_setup : theory -> theory
+ val setup : theory -> theory
end;
structure ResAxioms : RES_AXIOMS =
@@ -471,9 +471,9 @@
(CHANGED_PROP o Meson.meson_claset_tac (cnf_rules_of_ths ths) (local_claset_of ctxt));
val meson_method_setup =
- [Method.add_methods
- [("meson", Method.thms_ctxt_args meson_meth,
- "The MESON resolution proof procedure")]];
+ Method.add_methods
+ [("meson", Method.thms_ctxt_args meson_meth,
+ "The MESON resolution proof procedure")];
@@ -497,6 +497,6 @@
[("skolem", (skolem_global, skolem_local),
"skolemization of a theorem")];
-val setup = [clause_cache_setup, setup_attrs];
+val setup = clause_cache_setup #> setup_attrs;
end;
--- a/src/HOL/Tools/split_rule.ML Thu Jan 19 15:45:10 2006 +0100
+++ b/src/HOL/Tools/split_rule.ML Thu Jan 19 21:22:08 2006 +0100
@@ -16,7 +16,7 @@
include BASIC_SPLIT_RULE
val split_rule_var: term * thm -> thm
val split_rule_goal: string list list -> thm -> thm
- val setup: (theory -> theory) list
+ val setup: theory -> theory
end;
structure SplitRule: SPLIT_RULE =
@@ -141,9 +141,9 @@
>> (fn xss => Attrib.rule (K (split_rule_goal xss)))) x;
val setup =
- [Attrib.add_attributes
- [("split_format", (split_format, split_format),
- "split pair-typed subterms in premises, or function arguments")]];
+ Attrib.add_attributes
+ [("split_format", (split_format, split_format),
+ "split pair-typed subterms in premises, or function arguments")];
end;
--- a/src/HOL/Tools/typedef_package.ML Thu Jan 19 15:45:10 2006 +0100
+++ b/src/HOL/Tools/typedef_package.ML Thu Jan 19 21:22:08 2006 +0100
@@ -23,7 +23,7 @@
* (string * string) option -> theory -> Proof.state
val typedef_i: (bool * string) * (bstring * string list * mixfix) * term
* (string * string) option -> theory -> Proof.state
- val setup: (theory -> theory) list
+ val setup: theory -> theory
end;
structure TypedefPackage: TYPEDEF_PACKAGE =
@@ -360,9 +360,9 @@
| typedef_tycodegen thy defs gr dep module brack _ = NONE;
val setup =
- [TypedefData.init,
- Codegen.add_codegen "typedef" typedef_codegen,
- Codegen.add_tycodegen "typedef" typedef_tycodegen];
+ TypedefData.init #>
+ Codegen.add_codegen "typedef" typedef_codegen #>
+ Codegen.add_tycodegen "typedef" typedef_tycodegen;
--- a/src/HOL/antisym_setup.ML Thu Jan 19 15:45:10 2006 +0100
+++ b/src/HOL/antisym_setup.ML Thu Jan 19 21:22:08 2006 +0100
@@ -48,7 +48,7 @@
in
val antisym_setup =
- [fn thy => (Simplifier.change_simpset_of thy
- (fn ss => ss addsimprocs [antisym_le, antisym_less]); thy)]
+ (fn thy => (Simplifier.change_simpset_of thy
+ (fn ss => ss addsimprocs [antisym_le, antisym_less]); thy));
end
--- a/src/HOL/arith_data.ML Thu Jan 19 15:45:10 2006 +0100
+++ b/src/HOL/arith_data.ML Thu Jan 19 21:22:08 2006 +0100
@@ -420,8 +420,8 @@
in
val init_lin_arith_data =
- Fast_Arith.setup @
- [Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, ...} =>
+ Fast_Arith.setup #>
+ Fast_Arith.map_data (fn {add_mono_thms, mult_mono_thms, inj_thms, lessD, ...} =>
{add_mono_thms = add_mono_thms @
add_mono_thms_ordered_semiring @ add_mono_thms_ordered_field,
mult_mono_thms = mult_mono_thms,
@@ -433,8 +433,9 @@
addsimprocs [ab_group_add_cancel.sum_conv,
ab_group_add_cancel.rel_conv]
(*abel_cancel helps it work in abstract algebraic domains*)
- addsimprocs nat_cancel_sums_add}),
- ArithTheoryData.init, arith_discrete "nat"];
+ addsimprocs nat_cancel_sums_add}) #>
+ ArithTheoryData.init #>
+ arith_discrete "nat";
end;
@@ -576,14 +577,14 @@
(* theory setup *)
val arith_setup =
- init_lin_arith_data @
- [fn thy => (Simplifier.change_simpset_of thy (fn ss => ss
+ init_lin_arith_data #>
+ (fn thy => (Simplifier.change_simpset_of thy (fn ss => ss
addsimprocs (nat_cancel_sums @ [fast_nat_arith_simproc])
- addSolver (mk_solver' "lin. arith." Fast_Arith.cut_lin_arith_tac)); thy),
+ addSolver (mk_solver' "lin. arith." Fast_Arith.cut_lin_arith_tac)); thy)) #>
Method.add_methods
[("arith", (arith_method o #2) oo Method.syntax Args.bang_facts,
- "decide linear arithmethic")],
+ "decide linear arithmethic")] #>
Attrib.add_attributes [("arith_split",
(Attrib.no_args arith_split_add,
Attrib.no_args Attrib.undef_local_attribute),
- "declaration of split rules for arithmetic procedure")]];
+ "declaration of split rules for arithmetic procedure")];
--- a/src/HOL/cladata.ML Thu Jan 19 15:45:10 2006 +0100
+++ b/src/HOL/cladata.ML Thu Jan 19 21:22:08 2006 +0100
@@ -62,4 +62,4 @@
val HOL_cs = prop_cs addSIs [allI,ex_ex1I] addIs [exI, the_equality]
addSEs [exE] addEs [allE];
-val clasetup = [fn thy => (change_claset_of thy (fn _ => HOL_cs); thy)];
+val clasetup = (fn thy => (change_claset_of thy (fn _ => HOL_cs); thy));
--- a/src/HOL/simpdata.ML Thu Jan 19 15:45:10 2006 +0100
+++ b/src/HOL/simpdata.ML Thu Jan 19 21:22:08 2006 +0100
@@ -425,7 +425,7 @@
(* default simpset *)
val simpsetup =
- [fn thy => (change_simpset_of thy (fn _ => HOL_ss addcongs [if_weak_cong]); thy)];
+ (fn thy => (change_simpset_of thy (fn _ => HOL_ss addcongs [if_weak_cong]); thy));
(*** integration of simplifier with classical reasoner ***)
--- a/src/HOLCF/cont_proc.ML Thu Jan 19 15:45:10 2006 +0100
+++ b/src/HOLCF/cont_proc.ML Thu Jan 19 21:22:08 2006 +0100
@@ -10,7 +10,7 @@
val all_cont_thms: term -> thm list
val cont_tac: int -> tactic
val cont_proc: theory -> simproc
- val setup: (theory -> theory) list
+ val setup: theory -> theory
end;
structure ContProc: CONT_PROC =
@@ -110,6 +110,6 @@
end;
val setup =
- [fn thy => (Simplifier.change_simpset_of thy (fn ss => ss addsimprocs [cont_proc thy]); thy)];
+ (fn thy => (Simplifier.change_simpset_of thy (fn ss => ss addsimprocs [cont_proc thy]); thy));
end;
--- a/src/Provers/Arith/fast_lin_arith.ML Thu Jan 19 15:45:10 2006 +0100
+++ b/src/Provers/Arith/fast_lin_arith.ML Thu Jan 19 21:22:08 2006 +0100
@@ -70,7 +70,7 @@
signature FAST_LIN_ARITH =
sig
- val setup: (theory -> theory) list
+ val setup: theory -> theory
val map_data: ({add_mono_thms: thm list, mult_mono_thms: thm list, inj_thms: thm list,
lessD: thm list, neqE: thm list, simpset: Simplifier.simpset}
-> {add_mono_thms: thm list, mult_mono_thms: thm list, inj_thms: thm list,
@@ -119,7 +119,7 @@
end);
val map_data = Data.map;
-val setup = [Data.init];
+val setup = Data.init;
--- a/src/Provers/blast.ML Thu Jan 19 15:45:10 2006 +0100
+++ b/src/Provers/blast.ML Thu Jan 19 21:22:08 2006 +0100
@@ -79,7 +79,7 @@
val depth_limit : int ref
val blast_tac : claset -> int -> tactic
val Blast_tac : int -> tactic
- val setup : (theory -> theory) list
+ val setup : theory -> theory
(*debugging tools*)
val stats : bool ref
val trace : bool ref
@@ -1329,7 +1329,7 @@
| blast_meth (SOME lim) = Data.cla_meth' (fn cs => depth_tac cs lim);
val setup =
- [Method.add_methods [("blast", blast_args blast_meth, "tableau prover")]];
+ Method.add_methods [("blast", blast_args blast_meth, "tableau prover")];
end;
--- a/src/Provers/clasimp.ML Thu Jan 19 15:45:10 2006 +0100
+++ b/src/Provers/clasimp.ML Thu Jan 19 21:22:08 2006 +0100
@@ -64,7 +64,7 @@
val iff_del: Context.generic attribute
val iff_modifiers: (Args.T list -> (Method.modifier * Args.T list)) list
val clasimp_modifiers: (Args.T list -> (Method.modifier * Args.T list)) list
- val setup: (theory -> theory) list
+ val setup: theory -> theory
end;
functor ClasimpFun(Data: CLASIMP_DATA): CLASIMP =
@@ -327,14 +327,14 @@
(* theory setup *)
val setup =
- [Attrib.add_attributes
- [("iff", Attrib.common iff_att, "declaration of Simplifier / Classical rules")],
+ (Attrib.add_attributes
+ [("iff", Attrib.common iff_att, "declaration of Simplifier / Classical rules")] #>
Method.add_methods
[("fastsimp", clasimp_method' fast_simp_tac, "combined fast and simp"),
("slowsimp", clasimp_method' slow_simp_tac, "combined slow and simp"),
("bestsimp", clasimp_method' best_simp_tac, "combined best and simp"),
("force", clasimp_method' force_tac, "force"),
("auto", auto_args auto_meth, "auto"),
- ("clarsimp", clasimp_method' (CHANGED_PROP oo clarsimp_tac), "clarify simplified goal")]];
+ ("clarsimp", clasimp_method' (CHANGED_PROP oo clarsimp_tac), "clarify simplified goal")]);
end;
--- a/src/Provers/classical.ML Thu Jan 19 15:45:10 2006 +0100
+++ b/src/Provers/classical.ML Thu Jan 19 21:22:08 2006 +0100
@@ -155,7 +155,7 @@
val cla_meth': (claset -> int -> tactic) -> thm list -> Proof.context -> Proof.method
val cla_method: (claset -> tactic) -> Method.src -> Proof.context -> Proof.method
val cla_method': (claset -> int -> tactic) -> Method.src -> Proof.context -> Proof.method
- val setup: (theory -> theory) list
+ val setup: theory -> theory
end;
@@ -1080,7 +1080,7 @@
(** theory setup **)
-val setup = [GlobalClaset.init, LocalClaset.init, setup_attrs, setup_methods];
+val setup = GlobalClaset.init #> LocalClaset.init #> setup_attrs #> setup_methods;
--- a/src/Provers/eqsubst.ML Thu Jan 19 15:45:10 2006 +0100
+++ b/src/Provers/eqsubst.ML Thu Jan 19 21:22:08 2006 +0100
@@ -7,7 +7,7 @@
signature EQSUBST =
sig
- val setup : (Theory.theory -> Theory.theory) list
+ val setup : theory -> theory
end;
structure EqSubst: EQSUBST =
@@ -337,6 +337,6 @@
val setup =
- [Method.add_method ("subst", subst_meth, "substiution with an equation")];
+ Method.add_method ("subst", subst_meth, "substiution with an equation");
end;
--- a/src/Provers/hypsubst.ML Thu Jan 19 15:45:10 2006 +0100
+++ b/src/Provers/hypsubst.ML Thu Jan 19 21:22:08 2006 +0100
@@ -58,7 +58,7 @@
val inspect_pair : bool -> bool -> term * term * typ -> bool
val mk_eqs : bool -> thm -> thm list
val stac : thm -> int -> tactic
- val hypsubst_setup : (theory -> theory) list
+ val hypsubst_setup : theory -> theory
end;
@@ -242,8 +242,8 @@
(* theory setup *)
val hypsubst_setup =
- [Method.add_methods
- [("hypsubst", hyp_subst_meth, "substitution using an assumption (improper)"),
- ("simplesubst", subst_meth, "simple substitution")]];
+ Method.add_methods
+ [("hypsubst", hyp_subst_meth, "substitution using an assumption (improper)"),
+ ("simplesubst", subst_meth, "simple substitution")];
end;
--- a/src/Provers/induct_method.ML Thu Jan 19 15:45:10 2006 +0100
+++ b/src/Provers/induct_method.ML Thu Jan 19 21:22:08 2006 +0100
@@ -32,7 +32,7 @@
cases_tactic
val coinduct_tac: Proof.context -> bool -> term option list -> term option list ->
thm option -> thm list -> int -> cases_tactic
- val setup: (theory -> theory) list
+ val setup: theory -> theory
end;
functor InductMethodFun(Data: INDUCT_METHOD_DATA): INDUCT_METHOD =
@@ -556,9 +556,9 @@
(** theory setup **)
val setup =
- [Method.add_methods
+ Method.add_methods
[(InductAttrib.casesN, cases_meth, "case analysis on types or sets"),
(InductAttrib.inductN, induct_meth, "induction on types or sets"),
- (InductAttrib.coinductN, coinduct_meth, "coinduction on types or sets")]];
+ (InductAttrib.coinductN, coinduct_meth, "coinduction on types or sets")];
end;
--- a/src/Provers/splitter.ML Thu Jan 19 15:45:10 2006 +0100
+++ b/src/Provers/splitter.ML Thu Jan 19 21:22:08 2006 +0100
@@ -35,7 +35,7 @@
val split_add: Context.generic attribute
val split_del: Context.generic attribute
val split_modifiers : (Args.T list -> (Method.modifier * Args.T list)) list
- val setup: (theory -> theory) list
+ val setup: theory -> theory
end;
functor SplitterFun(Data: SPLITTER_DATA): SPLITTER =
@@ -455,9 +455,9 @@
(* theory setup *)
val setup =
- [Attrib.add_attributes
+ (Attrib.add_attributes
[(splitN, Attrib.common (Attrib.add_del_args split_add split_del),
- "declaration of case split rule")],
- Method.add_methods [(splitN, split_meth, "apply case split rule")]];
+ "declaration of case split rule")] #>
+ Method.add_methods [(splitN, split_meth, "apply case split rule")]);
end;
--- a/src/Pure/Isar/attrib.ML Thu Jan 19 15:45:10 2006 +0100
+++ b/src/Pure/Isar/attrib.ML Thu Jan 19 21:22:08 2006 +0100
@@ -114,7 +114,7 @@
end;
end);
-val _ = Context.add_setup [AttributesData.init];
+val _ = Context.add_setup AttributesData.init;
val print_attributes = AttributesData.print;
@@ -487,7 +487,7 @@
(* theory setup *)
val _ = Context.add_setup
- [add_attributes
+ (add_attributes
[("tagged", common tagged, "tagged theorem"),
("untagged", common untagged, "untagged theorem"),
("COMP", common COMP_att, "direct composition with rules (no lifting)"),
@@ -511,7 +511,7 @@
("rulify", (no_args ObjectLogic.declare_rulify, no_args undef_local_attribute),
"declaration of rulify rule"),
("rule_format", common rule_format_att, "result put into standard rule format"),
- ("attribute", common internal_att, "internal attribute")]];
+ ("attribute", common internal_att, "internal attribute")]);
end;
--- a/src/Pure/Isar/calculation.ML Thu Jan 19 15:45:10 2006 +0100
+++ b/src/Pure/Isar/calculation.ML Thu Jan 19 21:22:08 2006 +0100
@@ -46,7 +46,7 @@
end;
);
-val _ = Context.add_setup [CalculationData.init];
+val _ = Context.add_setup CalculationData.init;
val print_rules = CalculationData.print;
@@ -97,13 +97,13 @@
val sym_att = Attrib.add_del_args sym_add sym_del;
val _ = Context.add_setup
- [Attrib.add_attributes
+ (Attrib.add_attributes
[("trans", Attrib.common trans_att, "declaration of transitivity rule"),
("sym", Attrib.common sym_att, "declaration of symmetry rule"),
- ("symmetric", Attrib.common (Attrib.no_args symmetric), "resolution with symmetry rule")],
- snd o PureThy.add_thms
+ ("symmetric", Attrib.common (Attrib.no_args symmetric), "resolution with symmetry rule")] #>
+ PureThy.add_thms
[(("", transitive_thm), [Attrib.theory trans_add]),
- (("", symmetric_thm), [Attrib.theory sym_add])]];
+ (("", symmetric_thm), [Attrib.theory sym_add])] #> snd);
--- a/src/Pure/Isar/context_rules.ML Thu Jan 19 15:45:10 2006 +0100
+++ b/src/Pure/Isar/context_rules.ML Thu Jan 19 21:22:08 2006 +0100
@@ -123,7 +123,7 @@
in Pretty.writeln (Pretty.chunks (map prt_kind rule_kinds)) end;
);
-val _ = Context.add_setup [Rules.init];
+val _ = Context.add_setup Rules.init;
val print_rules = Rules.print;
@@ -203,7 +203,7 @@
val dest_query = rule_add elim_queryK Tactic.make_elim;
val _ = Context.add_setup
- [snd o PureThy.add_thms [(("", Drule.equal_intr_rule), [Attrib.theory (intro_query NONE)])]];
+ (snd o PureThy.add_thms [(("", Drule.equal_intr_rule), [Attrib.theory (intro_query NONE)])]);
(* concrete syntax *)
@@ -222,6 +222,6 @@
("rule", Attrib.common (Attrib.syntax (Scan.lift Args.del >> K rule_del)),
"remove declaration of intro/elim/dest rule")];
-val _ = Context.add_setup [Attrib.add_attributes rule_atts];
+val _ = Context.add_setup (Attrib.add_attributes rule_atts);
end;
--- a/src/Pure/Isar/induct_attrib.ML Thu Jan 19 15:45:10 2006 +0100
+++ b/src/Pure/Isar/induct_attrib.ML Thu Jan 19 21:22:08 2006 +0100
@@ -134,7 +134,7 @@
end
);
-val _ = Context.add_setup [Induct.init];
+val _ = Context.add_setup Induct.init;
val print_rules = Induct.print;
val dest_rules = dest o Induct.get;
@@ -224,9 +224,9 @@
end;
val _ = Context.add_setup
- [Attrib.add_attributes
+ (Attrib.add_attributes
[(casesN, Attrib.common cases_att, "declaration of cases rule for type or set"),
(inductN, Attrib.common induct_att, "declaration of induction rule for type or set"),
- (coinductN, Attrib.common coinduct_att, "declaration of coinduction rule for type or set")]];
+ (coinductN, Attrib.common coinduct_att, "declaration of coinduction rule for type or set")]);
end;
--- a/src/Pure/Isar/locale.ML Thu Jan 19 15:45:10 2006 +0100
+++ b/src/Pure/Isar/locale.ML Thu Jan 19 21:22:08 2006 +0100
@@ -278,7 +278,7 @@
|> Pretty.writeln;
end);
-val _ = Context.add_setup [GlobalLocalesData.init];
+val _ = Context.add_setup GlobalLocalesData.init;
@@ -293,7 +293,7 @@
fun print _ _ = ();
end);
-val _ = Context.add_setup [LocalLocalesData.init];
+val _ = Context.add_setup LocalLocalesData.init;
(* access locales *)
@@ -1718,8 +1718,8 @@
end;
val _ = Context.add_setup
- [add_locale_i true "var" empty [Fixes [(Syntax.internal "x", NONE, NoSyn)]],
- add_locale_i true "struct" empty [Fixes [(Syntax.internal "S", NONE, Structure)]]];
+ (add_locale_i true "var" empty [Fixes [(Syntax.internal "x", NONE, NoSyn)]] #>
+ add_locale_i true "struct" empty [Fixes [(Syntax.internal "S", NONE, Structure)]]);
--- a/src/Pure/Isar/method.ML Thu Jan 19 15:45:10 2006 +0100
+++ b/src/Pure/Isar/method.ML Thu Jan 19 21:22:08 2006 +0100
@@ -544,7 +544,7 @@
end;
end);
-val _ = Context.add_setup [MethodsData.init];
+val _ = Context.add_setup MethodsData.init;
val print_methods = MethodsData.print;
@@ -721,9 +721,9 @@
val rotate_meth = goal_args (Scan.optional Args.int 1) Tactic.rotate_tac;
-(* pure_methods *)
+(* theory setup *)
-val pure_methods =
+val _ = Context.add_setup (add_methods
[("fail", no_args fail, "force failure"),
("succeed", no_args succeed, "succeed"),
("-", no_args insert_facts, "do nothing (insert current facts only)"),
@@ -751,9 +751,7 @@
("thin_tac", thin_meth, "remove premise (dynamic instantiation)"),
("rename_tac", rename_meth, "rename parameters of goal (dynamic instantiation)"),
("rotate_tac", rotate_meth, "rotate assumptions of goal"),
- ("tactic", simple_args Args.name tactic, "ML tactic as proof method")];
-
-val _ = Context.add_setup [add_methods pure_methods];
+ ("tactic", simple_args Args.name tactic, "ML tactic as proof method")]);
(*final declarations of this structure!*)
--- a/src/Pure/Isar/object_logic.ML Thu Jan 19 15:45:10 2006 +0100
+++ b/src/Pure/Isar/object_logic.ML Thu Jan 19 21:22:08 2006 +0100
@@ -56,7 +56,7 @@
fun print _ _ = ();
end);
-val _ = Context.add_setup [ObjectLogicData.init];
+val _ = Context.add_setup ObjectLogicData.init;
--- a/src/Pure/Isar/proof_context.ML Thu Jan 19 15:45:10 2006 +0100
+++ b/src/Pure/Isar/proof_context.ML Thu Jan 19 21:22:08 2006 +0100
@@ -204,7 +204,7 @@
fun print _ _ = ();
);
-val _ = Context.add_setup [ContextData.init];
+val _ = Context.add_setup ContextData.init;
fun rep_context ctxt = ContextData.get ctxt |> (fn Ctxt args => args);
--- a/src/Pure/Isar/skip_proof.ML Thu Jan 19 15:45:10 2006 +0100
+++ b/src/Pure/Isar/skip_proof.ML Thu Jan 19 21:22:08 2006 +0100
@@ -23,7 +23,7 @@
if ! quick_and_dirty then prop
else error "Proof may be skipped in quick_and_dirty mode only!";
-val _ = Context.add_setup [Theory.add_oracle ("skip_proof", skip_proof)];
+val _ = Context.add_setup (Theory.add_oracle ("skip_proof", skip_proof));
(* basic cheating *)
--- a/src/Pure/Isar/term_style.ML Thu Jan 19 15:45:10 2006 +0100
+++ b/src/Pure/Isar/term_style.ML Thu Jan 19 21:22:08 2006 +0100
@@ -33,7 +33,7 @@
fun print _ tab = Pretty.writeln (Pretty.strs ("antiquote styles:" :: Symtab.keys tab));
end);
-val _ = Context.add_setup [StyleData.init];
+val _ = Context.add_setup StyleData.init;
val print_styles = StyleData.print;
@@ -68,26 +68,27 @@
end;
val _ = Context.add_setup
- [add_style "lhs" (fst oo style_binargs),
- add_style "rhs" (snd oo style_binargs),
- add_style "prem1" (style_parm_premise 1),
- add_style "prem2" (style_parm_premise 2),
- add_style "prem3" (style_parm_premise 3),
- add_style "prem4" (style_parm_premise 4),
- add_style "prem5" (style_parm_premise 5),
- add_style "prem6" (style_parm_premise 6),
- add_style "prem7" (style_parm_premise 7),
- add_style "prem8" (style_parm_premise 8),
- add_style "prem9" (style_parm_premise 9),
- add_style "prem10" (style_parm_premise 10),
- add_style "prem11" (style_parm_premise 11),
- add_style "prem12" (style_parm_premise 12),
- add_style "prem13" (style_parm_premise 13),
- add_style "prem14" (style_parm_premise 14),
- add_style "prem15" (style_parm_premise 15),
- add_style "prem16" (style_parm_premise 16),
- add_style "prem17" (style_parm_premise 17),
- add_style "prem18" (style_parm_premise 18),
- add_style "prem19" (style_parm_premise 19),
- add_style "concl" (K Logic.strip_imp_concl)];
+ (add_style "lhs" (fst oo style_binargs) #>
+ add_style "rhs" (snd oo style_binargs) #>
+ add_style "prem1" (style_parm_premise 1) #>
+ add_style "prem2" (style_parm_premise 2) #>
+ add_style "prem3" (style_parm_premise 3) #>
+ add_style "prem4" (style_parm_premise 4) #>
+ add_style "prem5" (style_parm_premise 5) #>
+ add_style "prem6" (style_parm_premise 6) #>
+ add_style "prem7" (style_parm_premise 7) #>
+ add_style "prem8" (style_parm_premise 8) #>
+ add_style "prem9" (style_parm_premise 9) #>
+ add_style "prem10" (style_parm_premise 10) #>
+ add_style "prem11" (style_parm_premise 11) #>
+ add_style "prem12" (style_parm_premise 12) #>
+ add_style "prem13" (style_parm_premise 13) #>
+ add_style "prem14" (style_parm_premise 14) #>
+ add_style "prem15" (style_parm_premise 15) #>
+ add_style "prem16" (style_parm_premise 16) #>
+ add_style "prem17" (style_parm_premise 17) #>
+ add_style "prem18" (style_parm_premise 18) #>
+ add_style "prem19" (style_parm_premise 19) #>
+ add_style "concl" (K Logic.strip_imp_concl));
+
end;
--- a/src/Pure/Proof/extraction.ML Thu Jan 19 15:45:10 2006 +0100
+++ b/src/Pure/Proof/extraction.ML Thu Jan 19 21:22:08 2006 +0100
@@ -214,7 +214,7 @@
fun print _ _ = ();
end);
-val _ = Context.add_setup [ExtractionData.init];
+val _ = Context.add_setup ExtractionData.init;
fun read_condeq thy =
let val thy' = add_syntax thy
@@ -401,7 +401,7 @@
(** Pure setup **)
val _ = Context.add_setup
- [add_types [("prop", ([], NONE))],
+ (add_types [("prop", ([], NONE))] #>
add_typeof_eqns
["(typeof (PROP P)) == (Type (TYPE(Null))) ==> \
@@ -422,7 +422,7 @@
\ (typeof (!!x::'a. PROP P (x))) == (Type (TYPE('a => 'P)))",
"(%x. typeof (f (x))) == (%x. Type (TYPE('f))) ==> \
- \ (typeof (f)) == (Type (TYPE('f)))"],
+ \ (typeof (f)) == (Type (TYPE('f)))"] #>
add_realizes_eqns
["(typeof (PROP P)) == (Type (TYPE(Null))) ==> \
@@ -442,12 +442,12 @@
\ (!!x. PROP realizes (Null) (PROP P (x)))",
"(realizes (r) (!!x. PROP P (x))) == \
- \ (!!x. PROP realizes (r (x)) (PROP P (x)))"],
+ \ (!!x. PROP realizes (r (x)) (PROP P (x)))"] #>
Attrib.add_attributes
[("extraction_expand",
(Attrib.no_args add_expand_thm, K Attrib.undef_local_attribute),
- "specify theorems / definitions to be expanded during extraction")]];
+ "specify theorems / definitions to be expanded during extraction")]);
(**** extract program ****)
--- a/src/Pure/Proof/proof_rewrite_rules.ML Thu Jan 19 15:45:10 2006 +0100
+++ b/src/Pure/Proof/proof_rewrite_rules.ML Thu Jan 19 21:22:08 2006 +0100
@@ -181,7 +181,7 @@
in rew' end;
fun rprocs b = [("Pure/meta_equality", rew b)];
-val _ = Context.add_setup [Proofterm.add_prf_rprocs (rprocs false)];
+val _ = Context.add_setup (Proofterm.add_prf_rprocs (rprocs false));
(**** apply rewriting function to all terms in proof ****)
--- a/src/Pure/Thy/html.ML Thu Jan 19 15:45:10 2006 +0100
+++ b/src/Pure/Thy/html.ML Thu Jan 19 21:22:08 2006 +0100
@@ -253,7 +253,7 @@
("var", style "var"),
("xstr", style "xstr")];
-val _ = Context.add_setup [Theory.add_mode_tokentrfuns htmlN html_trans];
+val _ = Context.add_setup (Theory.add_mode_tokentrfuns htmlN html_trans);
--- a/src/Pure/Thy/present.ML Thu Jan 19 15:45:10 2006 +0100
+++ b/src/Pure/Thy/present.ML Thu Jan 19 21:22:08 2006 +0100
@@ -83,7 +83,7 @@
fun print _ _ = ();
end);
-val _ = Context.add_setup [BrowserInfoData.init];
+val _ = Context.add_setup BrowserInfoData.init;
fun get_info thy =
if Context.theory_name thy mem_string [Context.ProtoPureN, Context.PureN, Context.CPureN]
--- a/src/Pure/Tools/class_package.ML Thu Jan 19 15:45:10 2006 +0100
+++ b/src/Pure/Tools/class_package.ML Thu Jan 19 21:22:08 2006 +0100
@@ -39,7 +39,7 @@
struct
-(* data kind 'Pure/classes' *)
+(* theory data *)
type class_data = {
superclasses: class list,
@@ -87,6 +87,7 @@
end
);
+val _ = Context.add_setup ClassData.init;
val print_classes = ClassData.print;
val lookup_class_data = Symtab.lookup o fst o ClassData.get;
@@ -451,9 +452,4 @@
end; (* local *)
-
-(* setup *)
-
-val _ = Context.add_setup [ClassData.init];
-
end; (* struct *)
--- a/src/Pure/Tools/codegen_package.ML Thu Jan 19 15:45:10 2006 +0100
+++ b/src/Pure/Tools/codegen_package.ML Thu Jan 19 21:22:08 2006 +0100
@@ -304,9 +304,11 @@
target_data = Symtab.join (K (merge_target_data #> SOME))
(target_data1, target_data2)
};
- fun print thy _ = writeln "sorry, this stuff is too complicated...";
+ fun print _ _ = ();
end);
+val _ = Context.add_setup CodegenData.init;
+
fun map_codegen_data f thy =
case CodegenData.get thy
of { modl, gens, target_data, logic_data } =>
@@ -1311,18 +1313,17 @@
-(** setup **)
+(** theory setup **)
-val _ = Context.add_setup [
- CodegenData.init,
-(* add_appconst_i ("op =", ((2, 2), appgen_eq)), *)
- add_eqextr ("defs", eqextr_defs),
- add_defgen ("clsdecl", defgen_clsdecl),
- add_defgen ("funs", defgen_funs),
- add_defgen ("clsmem", defgen_clsmem),
- add_defgen ("datatypecons", defgen_datatypecons)(*,
- add_defgen ("clsinst", defgen_clsinst) *)
-];
+val _ = Context.add_setup
+ (add_eqextr ("defs", eqextr_defs) #>
+ add_defgen ("clsdecl", defgen_clsdecl) #>
+ add_defgen ("funs", defgen_funs) #>
+ add_defgen ("clsmem", defgen_clsmem) #>
+ add_defgen ("datatypecons", defgen_datatypecons));
+
+(* add_appconst_i ("op =", ((2, 2), appgen_eq)) *)
+(* add_defgen ("clsinst", defgen_clsinst) *)
end; (* local *)
--- a/src/Pure/Tools/compute.ML Thu Jan 19 15:45:10 2006 +0100
+++ b/src/Pure/Tools/compute.ML Thu Jan 19 21:22:08 2006 +0100
@@ -277,7 +277,9 @@
fun rewrite r ct = rewrite_param r default_naming ct
-(* setup of the Pure.compute oracle *)
+
+(* theory setup *)
+
fun compute_oracle (thy, Param (r, naming, ct)) =
let
val _ = Theory.assert_super (theory_of r) thy
@@ -286,6 +288,6 @@
Logic.mk_equals (term_of ct, t')
end
-val _ = Context.add_setup [Theory.add_oracle ("compute", compute_oracle)]
+val _ = Context.add_setup (Theory.add_oracle ("compute", compute_oracle))
end
--- a/src/Pure/axclass.ML Thu Jan 19 15:45:10 2006 +0100
+++ b/src/Pure/axclass.ML Thu Jan 19 21:22:08 2006 +0100
@@ -136,7 +136,7 @@
in Pretty.writeln (Pretty.chunks (map pretty_axclass (Symtab.dest tab))) end;
end);
-val _ = Context.add_setup [AxclassesData.init];
+val _ = Context.add_setup AxclassesData.init;
val print_axclasses = AxclassesData.print;
@@ -334,10 +334,10 @@
HEADGOAL (Method.some_rule_tac rules ctxt facts) ORELSE
default_intro_classes_tac facts;
-val _ = Context.add_setup [Method.add_methods
+val _ = Context.add_setup (Method.add_methods
[("intro_classes", Method.no_args (Method.METHOD intro_classes_tac),
- "back-chain introduction rules of axiomatic type classes"),
- ("default", Method.thms_ctxt_args (Method.METHOD oo default_tac), "apply some intro/elim rule")]];
+ "back-chain introduction rules of axiomatic type classes"),
+ ("default", Method.thms_ctxt_args (Method.METHOD oo default_tac), "apply some intro/elim rule")]);
--- a/src/Pure/codegen.ML Thu Jan 19 15:45:10 2006 +0100
+++ b/src/Pure/codegen.ML Thu Jan 19 21:22:08 2006 +0100
@@ -240,7 +240,7 @@
Pretty.strs ("type code generators:" :: map fst tycodegens)]);
end);
-val _ = Context.add_setup [CodegenData.init];
+val _ = Context.add_setup CodegenData.init;
val print_codegens = CodegenData.print;
@@ -316,9 +316,9 @@
(#attrs (CodegenData.get thy)))));
val _ = Context.add_setup
- [Attrib.add_attributes
+ (Attrib.add_attributes
[("code", (code_attr, K Attrib.undef_local_attribute),
- "declare theorems for code generation")]];
+ "declare theorems for code generation")]);
(**** preprocessors ****)
@@ -361,7 +361,7 @@
end)
in (add_preprocessor prep thy, eqn) end;
-val _ = Context.add_setup [add_attribute "unfold" (Scan.succeed unfold_attr)];
+val _ = Context.add_setup (add_attribute "unfold" (Scan.succeed unfold_attr));
(**** associate constants with target language code ****)
@@ -834,8 +834,8 @@
end);
val _ = Context.add_setup
- [add_codegen "default" default_codegen,
- add_tycodegen "default" default_tycodegen];
+ (add_codegen "default" default_codegen #>
+ add_tycodegen "default" default_tycodegen);
fun mk_struct name s = "structure " ^ name ^ " =\nstruct\n\n" ^ s ^ "end;\n";
@@ -1086,7 +1086,7 @@
| _ => error ("Malformed annotation: " ^ quote s));
val _ = Context.add_setup
- [assoc_types [("fun", (parse_mixfix (K dummyT) "(_ ->/ _)",
+ (assoc_types [("fun", (parse_mixfix (K dummyT) "(_ ->/ _)",
[("term_of",
"fun term_of_fun_type _ T _ U _ = Free (\"<function>\", T --> U);\n"),
("test",
@@ -1098,7 +1098,7 @@
\ val y = G i;\n\
\ val f' = !f\n\
\ in (f := (fn x' => if x = x' then y else f' x'); y) end))\n\
- \ in (fn x => !f x) end;\n")]))]];
+ \ in (fn x => !f x) end;\n")]))]);
structure P = OuterParse and K = OuterKeyword;
--- a/src/Pure/proof_general.ML Thu Jan 19 15:45:10 2006 +0100
+++ b/src/Pure/proof_general.ML Thu Jan 19 21:22:08 2006 +0100
@@ -148,7 +148,7 @@
in
-val _ = Context.add_setup [Theory.add_tokentrfuns proof_general_trans];
+val _ = Context.add_setup (Theory.add_tokentrfuns proof_general_trans);
end;
--- a/src/Pure/simplifier.ML Thu Jan 19 15:45:10 2006 +0100
+++ b/src/Pure/simplifier.ML Thu Jan 19 21:22:08 2006 +0100
@@ -73,8 +73,8 @@
val simp_modifiers': (Args.T list -> (Method.modifier * Args.T list)) list
val simp_modifiers: (Args.T list -> (Method.modifier * Args.T list)) list
val method_setup: (Args.T list -> (Method.modifier * Args.T list)) list
- -> (theory -> theory) list
- val easy_setup: thm -> thm list -> (theory -> theory) list
+ -> theory -> theory
+ val easy_setup: thm -> thm list -> theory -> theory
end;
structure Simplifier: SIMPLIFIER =
@@ -96,7 +96,7 @@
fun print _ (ref ss) = print_ss ss;
end);
-val _ = Context.add_setup [GlobalSimpset.init];
+val _ = Context.add_setup GlobalSimpset.init;
val print_simpset = GlobalSimpset.print;
val get_simpset = ! o GlobalSimpset.get;
@@ -128,7 +128,7 @@
fun print _ ss = print_ss ss;
end);
-val _ = Context.add_setup [LocalSimpset.init];
+val _ = Context.add_setup LocalSimpset.init;
val print_local_simpset = LocalSimpset.print;
val get_local_simpset = LocalSimpset.get;
val put_local_simpset = LocalSimpset.put;
@@ -260,12 +260,12 @@
(* setup attributes *)
val _ = Context.add_setup
- [Attrib.add_attributes
+ (Attrib.add_attributes
[(simpN, Attrib.common (Attrib.add_del_args simp_add simp_del),
"declaration of Simplifier rule"),
(congN, Attrib.common (Attrib.add_del_args cong_add cong_del),
"declaration of Simplifier congruence rule"),
- ("simplified", Attrib.common simplified, "simplified rule")]];
+ ("simplified", Attrib.common simplified, "simplified rule")]);
@@ -318,18 +318,14 @@
((FLAGS o CHANGED_PROP) oo tac) (local_simpset_of ctxt)));
-(* setup methods *)
-fun setup_methods more_mods = Method.add_methods
+(** setup **)
+
+fun method_setup more_mods = Method.add_methods
[(simpN, simp_args more_mods simp_method', "simplification"),
("simp_all", simp_args more_mods simp_method, "simplification (all goals)")];
-fun method_setup mods = [setup_methods mods];
-
-
-(** easy_setup **)
-
-fun easy_setup reflect trivs =
+fun easy_setup reflect trivs = method_setup [] #> (fn thy =>
let
val trivialities = Drule.reflexive_thm :: trivs;
@@ -345,14 +341,14 @@
else [thm RS reflect] handle THM _ => [];
fun mksimps thm = mk_eq (Drule.forall_elim_vars (#maxidx (Thm.rep_thm thm) + 1) thm);
-
- fun init_ss thy =
- (GlobalSimpset.get thy :=
- empty_ss setsubgoaler asm_simp_tac
- setSSolver safe_solver
- setSolver unsafe_solver
- setmksimps mksimps; thy);
- in method_setup [] @ [init_ss] end;
+ in
+ GlobalSimpset.get thy :=
+ empty_ss setsubgoaler asm_simp_tac
+ setSSolver safe_solver
+ setSolver unsafe_solver
+ setmksimps mksimps;
+ thy
+ end);
open MetaSimplifier;
--- a/src/Sequents/prover.ML Thu Jan 19 15:45:10 2006 +0100
+++ b/src/Sequents/prover.ML Thu Jan 19 21:22:08 2006 +0100
@@ -179,7 +179,7 @@
fun print _ (ref pack) = print_pack pack;
end);
-val prover_setup = [ProverData.init];
+val prover_setup = ProverData.init;
val print_pack = ProverData.print;
val pack_ref_of = ProverData.get;
--- a/src/ZF/Tools/ind_cases.ML Thu Jan 19 15:45:10 2006 +0100
+++ b/src/ZF/Tools/ind_cases.ML Thu Jan 19 21:22:08 2006 +0100
@@ -9,7 +9,7 @@
sig
val declare: string -> (simpset -> cterm -> thm) -> theory -> theory
val inductive_cases: ((bstring * Attrib.src list) * string list) list -> theory -> theory
- val setup: (theory -> theory) list
+ val setup: theory -> theory
end;
structure IndCases: IND_CASES =
@@ -72,9 +72,9 @@
(* package setup *)
val setup =
- [IndCasesData.init,
+ (IndCasesData.init #>
Method.add_methods [("ind_cases", mk_cases_meth oo mk_cases_args,
- "dynamic case analysis on sets")]];
+ "dynamic case analysis on sets")]);
(* outer syntax *)
--- a/src/ZF/Tools/induct_tacs.ML Thu Jan 19 15:45:10 2006 +0100
+++ b/src/ZF/Tools/induct_tacs.ML Thu Jan 19 21:22:08 2006 +0100
@@ -15,7 +15,7 @@
val rep_datatype_i: thm -> thm -> thm list -> thm list -> theory -> theory
val rep_datatype: thmref * Attrib.src list -> thmref * Attrib.src list ->
(thmref * Attrib.src list) list -> (thmref * Attrib.src list) list -> theory -> theory
- val setup: (theory -> theory) list
+ val setup: theory -> theory
end;
@@ -185,13 +185,13 @@
(* theory setup *)
val setup =
- [DatatypesData.init,
- ConstructorsData.init,
+ (DatatypesData.init #>
+ ConstructorsData.init #>
Method.add_methods
[("induct_tac", Method.goal_args Args.name induct_tac,
"induct_tac emulation (dynamic instantiation!)"),
("case_tac", Method.goal_args Args.name exhaust_tac,
- "datatype case_tac emulation (dynamic instantiation!)")]];
+ "datatype case_tac emulation (dynamic instantiation!)")]);
(* outer syntax *)
--- a/src/ZF/Tools/numeral_syntax.ML Thu Jan 19 15:45:10 2006 +0100
+++ b/src/ZF/Tools/numeral_syntax.ML Thu Jan 19 21:22:08 2006 +0100
@@ -12,7 +12,7 @@
val mk_bin : IntInf.int -> term
val int_tr : term list -> term
val int_tr' : bool -> typ -> term list -> term
- val setup : (theory -> theory) list
+ val setup : theory -> theory
end;
structure NumeralSyntax: NUMERAL_SYNTAX =
@@ -100,7 +100,7 @@
val setup =
- [Theory.add_trfuns ([], [("_Int", int_tr)], [], []),
- Theory.add_trfunsT [("integ_of", int_tr'), ("Bin.integ_of", int_tr')]];
+ (Theory.add_trfuns ([], [("_Int", int_tr)], [], []) #>
+ Theory.add_trfunsT [("integ_of", int_tr'), ("Bin.integ_of", int_tr')]);
end;
--- a/src/ZF/Tools/typechk.ML Thu Jan 19 15:45:10 2006 +0100
+++ b/src/ZF/Tools/typechk.ML Thu Jan 19 21:22:08 2006 +0100
@@ -37,7 +37,7 @@
signature TYPE_CHECK =
sig
include BASIC_TYPE_CHECK
- val setup: (theory -> theory) list
+ val setup: theory -> theory
end;
structure TypeCheck: TYPE_CHECK =
@@ -210,10 +210,11 @@
(** theory setup **)
val setup =
- [TypecheckingData.init, LocalTypecheckingData.init,
- fn thy => (change_simpset_of thy (fn ss => ss addSolver type_solver); thy),
- Attrib.add_attributes [("TC", TC_attr, "declaration of typecheck rule")],
- Method.add_methods [("typecheck", TC_args typecheck, "ZF typecheck")]];
+ (TypecheckingData.init #>
+ LocalTypecheckingData.init #>
+ (fn thy => (change_simpset_of thy (fn ss => ss addSolver type_solver); thy)) #>
+ Attrib.add_attributes [("TC", TC_attr, "declaration of typecheck rule")] #>
+ Method.add_methods [("typecheck", TC_args typecheck, "ZF typecheck")]);
(** outer syntax **)