# HG changeset patch # User wenzelm # Date 1137702128 -3600 # Node ID 4b3dadb4fe33d2c8361a5e62d1d4a861db7eeb6e # Parent 9d6154f76476a884d72036ce95291cb9cbd7665c setup: theory -> theory; diff -r 9d6154f76476 -r 4b3dadb4fe33 doc-src/LaTeXsugar/Sugar/Sugar.thy --- 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} diff -r 9d6154f76476 -r 4b3dadb4fe33 src/FOL/IFOL.thy --- 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)" diff -r 9d6154f76476 -r 4b3dadb4fe33 src/FOL/cladata.ML --- 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!)")]); diff -r 9d6154f76476 -r 4b3dadb4fe33 src/FOL/simpdata.ML --- 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 ***) diff -r 9d6154f76476 -r 4b3dadb4fe33 src/HOL/Extraction.thy --- 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 *} diff -r 9d6154f76476 -r 4b3dadb4fe33 src/HOL/HOL.thy --- 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; *} diff -r 9d6154f76476 -r 4b3dadb4fe33 src/HOL/Hyperreal/StarDef.thy --- 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 \ star_n (\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]: "\f \ star_n F; x \ star_n X\ \ f \ x \ star_n (\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 \ star_n P \ unstar p \ {n. P n} \ \" @@ -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]: "\x \ star_n X; a \ Iset (star_n A)\ diff -r 9d6154f76476 -r 4b3dadb4fe33 src/HOL/Hyperreal/hypreal_arith.ML --- 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; diff -r 9d6154f76476 -r 4b3dadb4fe33 src/HOL/Hyperreal/transfer.ML --- 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; diff -r 9d6154f76476 -r 4b3dadb4fe33 src/HOL/Import/hol4rews.ML --- 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 diff -r 9d6154f76476 -r 4b3dadb4fe33 src/HOL/Import/import_package.ML --- 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 diff -r 9d6154f76476 -r 4b3dadb4fe33 src/HOL/Import/shuffler.ML --- 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 diff -r 9d6154f76476 -r 4b3dadb4fe33 src/HOL/Integ/IntDef.thy --- 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] diff -r 9d6154f76476 -r 4b3dadb4fe33 src/HOL/Integ/NatBin.thy --- 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 diff -r 9d6154f76476 -r 4b3dadb4fe33 src/HOL/Integ/int_arith1.ML --- 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; diff -r 9d6154f76476 -r 4b3dadb4fe33 src/HOL/Integ/nat_simprocs.ML --- 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; diff -r 9d6154f76476 -r 4b3dadb4fe33 src/HOL/Integ/presburger.ML --- 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; diff -r 9d6154f76476 -r 4b3dadb4fe33 src/HOL/Library/Commutative_Ring.thy --- 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 diff -r 9d6154f76476 -r 4b3dadb4fe33 src/HOL/Library/EfficientNat.thy --- 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 diff -r 9d6154f76476 -r 4b3dadb4fe33 src/HOL/Library/comm_ring.ML --- 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; diff -r 9d6154f76476 -r 4b3dadb4fe33 src/HOL/Library/word_setup.ML --- 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 diff -r 9d6154f76476 -r 4b3dadb4fe33 src/HOL/List.thy --- 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 diff -r 9d6154f76476 -r 4b3dadb4fe33 src/HOL/Product_Type.thy --- 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; *} diff -r 9d6154f76476 -r 4b3dadb4fe33 src/HOL/Real/rat_arith.ML --- 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; diff -r 9d6154f76476 -r 4b3dadb4fe33 src/HOL/Real/real_arith.ML --- 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 diff -r 9d6154f76476 -r 4b3dadb4fe33 src/HOL/Tools/Presburger/presburger.ML --- 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; diff -r 9d6154f76476 -r 4b3dadb4fe33 src/HOL/Tools/datatype_codegen.ML --- 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; diff -r 9d6154f76476 -r 4b3dadb4fe33 src/HOL/Tools/datatype_package.ML --- 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 *) diff -r 9d6154f76476 -r 4b3dadb4fe33 src/HOL/Tools/inductive_codegen.ML --- 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; diff -r 9d6154f76476 -r 4b3dadb4fe33 src/HOL/Tools/inductive_package.ML --- 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 *) diff -r 9d6154f76476 -r 4b3dadb4fe33 src/HOL/Tools/inductive_realizer.ML --- 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; diff -r 9d6154f76476 -r 4b3dadb4fe33 src/HOL/Tools/meson.ML --- 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; diff -r 9d6154f76476 -r 4b3dadb4fe33 src/HOL/Tools/numeral_syntax.ML --- 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; diff -r 9d6154f76476 -r 4b3dadb4fe33 src/HOL/Tools/recdef_package.ML --- 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 *) diff -r 9d6154f76476 -r 4b3dadb4fe33 src/HOL/Tools/recfun_codegen.ML --- 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; diff -r 9d6154f76476 -r 4b3dadb4fe33 src/HOL/Tools/reconstruction.ML --- 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 diff -r 9d6154f76476 -r 4b3dadb4fe33 src/HOL/Tools/record_package.ML --- 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 *) diff -r 9d6154f76476 -r 4b3dadb4fe33 src/HOL/Tools/refute.ML --- 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 diff -r 9d6154f76476 -r 4b3dadb4fe33 src/HOL/Tools/res_atp_methods.ML --- 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 diff -r 9d6154f76476 -r 4b3dadb4fe33 src/HOL/Tools/res_axioms.ML --- 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; diff -r 9d6154f76476 -r 4b3dadb4fe33 src/HOL/Tools/split_rule.ML --- 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; diff -r 9d6154f76476 -r 4b3dadb4fe33 src/HOL/Tools/typedef_package.ML --- 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; diff -r 9d6154f76476 -r 4b3dadb4fe33 src/HOL/antisym_setup.ML --- 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 diff -r 9d6154f76476 -r 4b3dadb4fe33 src/HOL/arith_data.ML --- 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")]; diff -r 9d6154f76476 -r 4b3dadb4fe33 src/HOL/cladata.ML --- 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)); diff -r 9d6154f76476 -r 4b3dadb4fe33 src/HOL/simpdata.ML --- 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 ***) diff -r 9d6154f76476 -r 4b3dadb4fe33 src/HOLCF/cont_proc.ML --- 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; diff -r 9d6154f76476 -r 4b3dadb4fe33 src/Provers/Arith/fast_lin_arith.ML --- 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; diff -r 9d6154f76476 -r 4b3dadb4fe33 src/Provers/blast.ML --- 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; diff -r 9d6154f76476 -r 4b3dadb4fe33 src/Provers/clasimp.ML --- 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; diff -r 9d6154f76476 -r 4b3dadb4fe33 src/Provers/classical.ML --- 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; diff -r 9d6154f76476 -r 4b3dadb4fe33 src/Provers/eqsubst.ML --- 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; diff -r 9d6154f76476 -r 4b3dadb4fe33 src/Provers/hypsubst.ML --- 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; diff -r 9d6154f76476 -r 4b3dadb4fe33 src/Provers/induct_method.ML --- 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; diff -r 9d6154f76476 -r 4b3dadb4fe33 src/Provers/splitter.ML --- 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; diff -r 9d6154f76476 -r 4b3dadb4fe33 src/Pure/Isar/attrib.ML --- 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; diff -r 9d6154f76476 -r 4b3dadb4fe33 src/Pure/Isar/calculation.ML --- 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); diff -r 9d6154f76476 -r 4b3dadb4fe33 src/Pure/Isar/context_rules.ML --- 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; diff -r 9d6154f76476 -r 4b3dadb4fe33 src/Pure/Isar/induct_attrib.ML --- 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; diff -r 9d6154f76476 -r 4b3dadb4fe33 src/Pure/Isar/locale.ML --- 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)]]); diff -r 9d6154f76476 -r 4b3dadb4fe33 src/Pure/Isar/method.ML --- 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!*) diff -r 9d6154f76476 -r 4b3dadb4fe33 src/Pure/Isar/object_logic.ML --- 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; diff -r 9d6154f76476 -r 4b3dadb4fe33 src/Pure/Isar/proof_context.ML --- 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); diff -r 9d6154f76476 -r 4b3dadb4fe33 src/Pure/Isar/skip_proof.ML --- 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 *) diff -r 9d6154f76476 -r 4b3dadb4fe33 src/Pure/Isar/term_style.ML --- 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; diff -r 9d6154f76476 -r 4b3dadb4fe33 src/Pure/Proof/extraction.ML --- 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 ****) diff -r 9d6154f76476 -r 4b3dadb4fe33 src/Pure/Proof/proof_rewrite_rules.ML --- 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 ****) diff -r 9d6154f76476 -r 4b3dadb4fe33 src/Pure/Thy/html.ML --- 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); diff -r 9d6154f76476 -r 4b3dadb4fe33 src/Pure/Thy/present.ML --- 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] diff -r 9d6154f76476 -r 4b3dadb4fe33 src/Pure/Tools/class_package.ML --- 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 *) diff -r 9d6154f76476 -r 4b3dadb4fe33 src/Pure/Tools/codegen_package.ML --- 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 *) diff -r 9d6154f76476 -r 4b3dadb4fe33 src/Pure/Tools/compute.ML --- 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 diff -r 9d6154f76476 -r 4b3dadb4fe33 src/Pure/axclass.ML --- 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")]); diff -r 9d6154f76476 -r 4b3dadb4fe33 src/Pure/codegen.ML --- 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 (\"\", 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; diff -r 9d6154f76476 -r 4b3dadb4fe33 src/Pure/proof_general.ML --- 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; diff -r 9d6154f76476 -r 4b3dadb4fe33 src/Pure/simplifier.ML --- 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; diff -r 9d6154f76476 -r 4b3dadb4fe33 src/Sequents/prover.ML --- 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; diff -r 9d6154f76476 -r 4b3dadb4fe33 src/ZF/Tools/ind_cases.ML --- 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 *) diff -r 9d6154f76476 -r 4b3dadb4fe33 src/ZF/Tools/induct_tacs.ML --- 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 *) diff -r 9d6154f76476 -r 4b3dadb4fe33 src/ZF/Tools/numeral_syntax.ML --- 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; diff -r 9d6154f76476 -r 4b3dadb4fe33 src/ZF/Tools/typechk.ML --- 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 **)