--- a/src/HOL/Algebra/ringsimp.ML Sun Mar 15 15:59:44 2009 +0100
+++ b/src/HOL/Algebra/ringsimp.ML Sun Mar 15 15:59:44 2009 +0100
@@ -62,11 +62,11 @@
Thm.declaration_attribute
(fn _ => Data.map (AList.delete struct_eq s));
-val attribute = Attrib.syntax
- (Scan.lift ((Args.add >> K true || Args.del >> K false) --| Args.colon ||
- Scan.succeed true) -- Scan.lift Args.name --
- Scan.repeat Args.term
- >> (fn ((b, n), ts) => if b then add_struct_thm (n, ts) else del_struct (n, ts)));
+val attribute =
+ Scan.lift ((Args.add >> K true || Args.del >> K false) --| Args.colon ||
+ Scan.succeed true) -- Scan.lift Args.name --
+ Scan.repeat Args.term
+ >> (fn ((b, n), ts) => if b then add_struct_thm (n, ts) else del_struct (n, ts));
(** Setup **)
@@ -74,6 +74,6 @@
val setup =
Method.setup @{binding algebra} (Scan.succeed (SIMPLE_METHOD' o algebra_tac))
"normalisation of algebraic structure" #>
- Attrib.add_attributes [("algebra", attribute, "theorems controlling algebra method")];
+ Attrib.setup @{binding algebra} attribute "theorems controlling algebra method";
end;
--- a/src/HOL/Import/hol4rews.ML Sun Mar 15 15:59:44 2009 +0100
+++ b/src/HOL/Import/hol4rews.ML Sun Mar 15 15:59:44 2009 +0100
@@ -649,6 +649,6 @@
in
val hol4_setup =
initial_maps #>
- Attrib.add_attributes
- [("hol4rew", Attrib.no_args add_hol4_rewrite, "HOL4 rewrite rule")]
+ Attrib.setup @{binding hol4rew} (Scan.succeed add_hol4_rewrite) "HOL4 rewrite rule"
+
end
--- a/src/HOL/Import/shuffler.ML Sun Mar 15 15:59:44 2009 +0100
+++ b/src/HOL/Import/shuffler.ML Sun Mar 15 15:59:44 2009 +0100
@@ -689,6 +689,6 @@
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, "declare rule for shuffler")]
+ Attrib.setup @{binding shuffle_rule} (Scan.succeed shuffle_attr) "declare rule for shuffler";
end
--- a/src/HOL/Library/reify_data.ML Sun Mar 15 15:59:44 2009 +0100
+++ b/src/HOL/Library/reify_data.ML Sun Mar 15 15:59:44 2009 +0100
@@ -32,8 +32,8 @@
val radd = Thm.declaration_attribute (Data.map o apsnd o Thm.add_thm);
val rdel = Thm.declaration_attribute (Data.map o apsnd o Thm.del_thm);
-val setup = Attrib.add_attributes
- [("reify", Attrib.add_del_args add del, "Reify data"),
- ("reflection", Attrib.add_del_args radd rdel, "Reflection data")];
+val setup =
+ Attrib.setup @{binding reify} (Attrib.add_del add del) "reify data" #>
+ Attrib.setup @{binding reflection} (Attrib.add_del radd rdel) "reflection data";
end;
--- a/src/HOL/NSA/transfer.ML Sun Mar 15 15:59:44 2009 +0100
+++ b/src/HOL/NSA/transfer.ML Sun Mar 15 15:59:44 2009 +0100
@@ -108,14 +108,13 @@
{intros=intros, unfolds=unfolds, refolds=refolds, consts=c::consts}))
val setup =
- Attrib.add_attributes
- [("transfer_intro", Attrib.add_del_args intro_add intro_del,
- "declaration of transfer introduction rule"),
- ("transfer_unfold", Attrib.add_del_args unfold_add unfold_del,
- "declaration of transfer unfolding rule"),
- ("transfer_refold", Attrib.add_del_args refold_add refold_del,
- "declaration of transfer refolding rule")] #>
- Method.add_method ("transfer", Method.thms_ctxt_args (fn ths => fn ctxt =>
- SIMPLE_METHOD' (transfer_tac ctxt ths)), "transfer principle");
+ Attrib.setup @{binding transfer_intro} (Attrib.add_del intro_add intro_del)
+ "declaration of transfer introduction rule" #>
+ Attrib.setup @{binding transfer_unfold} (Attrib.add_del unfold_add unfold_del)
+ "declaration of transfer unfolding rule" #>
+ Attrib.setup @{binding transfer_refold} (Attrib.add_del refold_add refold_del)
+ "declaration of transfer refolding rule" #>
+ Method.setup @{binding transfer} (Attrib.thms >> (fn ths => fn ctxt =>
+ SIMPLE_METHOD' (transfer_tac ctxt ths))) "transfer principle";
end;
--- a/src/HOL/Nominal/nominal_thmdecls.ML Sun Mar 15 15:59:44 2009 +0100
+++ b/src/HOL/Nominal/nominal_thmdecls.ML Sun Mar 15 15:59:44 2009 +0100
@@ -187,12 +187,14 @@
val setup =
- Attrib.add_attributes
- [("eqvt", Attrib.add_del_args eqvt_add eqvt_del, "equivariance theorem declaration"),
- ("eqvt_force", Attrib.add_del_args eqvt_force_add eqvt_force_del,
- "equivariance theorem declaration (without checking the form of the lemma)"),
- ("fresh", Attrib.add_del_args fresh_add fresh_del, "freshness theorem declaration"),
- ("bij", Attrib.add_del_args bij_add bij_del, "bijection theorem declaration")] #>
+ Attrib.setup @{binding eqvt} (Attrib.add_del eqvt_add eqvt_del)
+ "equivariance theorem declaration" #>
+ Attrib.setup @{binding eqvt_force} (Attrib.add_del eqvt_force_add eqvt_force_del)
+ "equivariance theorem declaration (without checking the form of the lemma)" #>
+ Attrib.setup @{binding fresh} (Attrib.add_del fresh_add fresh_del)
+ "freshness theorem declaration" #>
+ Attrib.setup @{binding "bij"} (Attrib.add_del bij_add bij_del)
+ "bijection theorem declaration" #>
PureThy.add_thms_dynamic (Binding.name "eqvts", #eqvts o Data.get) #>
PureThy.add_thms_dynamic (Binding.name "freshs", #freshs o Data.get) #>
PureThy.add_thms_dynamic (Binding.name "bijs", #bijs o Data.get);
--- a/src/HOL/Orderings.thy Sun Mar 15 15:59:44 2009 +0100
+++ b/src/HOL/Orderings.thy Sun Mar 15 15:59:44 2009 +0100
@@ -372,13 +372,13 @@
Thm.declaration_attribute
(fn _ => Data.map (AList.delete struct_eq s));
-val attribute = Attrib.syntax
- (Scan.lift ((Args.add -- Args.name >> (fn (_, s) => SOME s) ||
- Args.del >> K NONE) --| Args.colon (* FIXME ||
- Scan.succeed true *) ) -- Scan.lift Args.name --
- Scan.repeat Args.term
- >> (fn ((SOME tag, n), ts) => add_struct_thm (n, ts) tag
- | ((NONE, n), ts) => del_struct (n, ts)));
+val attribute =
+ Scan.lift ((Args.add -- Args.name >> (fn (_, s) => SOME s) ||
+ Args.del >> K NONE) --| Args.colon (* FIXME ||
+ Scan.succeed true *) ) -- Scan.lift Args.name --
+ Scan.repeat Args.term
+ >> (fn ((SOME tag, n), ts) => add_struct_thm (n, ts) tag
+ | ((NONE, n), ts) => del_struct (n, ts));
(** Diagnostic command **)
@@ -398,7 +398,7 @@
val setup =
Method.setup @{binding order} (Scan.succeed (SIMPLE_METHOD' o order_tac [])) "transitivity reasoner" #>
- Attrib.add_attributes [("order", attribute, "theorems controlling transitivity reasoner")];
+ Attrib.setup @{binding order} attribute "theorems controlling transitivity reasoner";
end;
--- a/src/HOL/Statespace/state_fun.ML Sun Mar 15 15:59:44 2009 +0100
+++ b/src/HOL/Statespace/state_fun.ML Sun Mar 15 15:59:44 2009 +0100
@@ -371,7 +371,7 @@
val mk_destr = gen_constr_destr (fn a => fn b => Syntax.const "Fun.comp" $ b $ a) "the_"
-fun statefun_simp_attr src (ctxt,thm) =
+val statefun_simp_attr = Thm.declaration_attribute (fn thm => fn ctxt =>
let
val (lookup_ss,ex_lookup_ss,simprocs_active) = StateFunData.get ctxt;
val (lookup_ss', ex_lookup_ss') =
@@ -381,15 +381,14 @@
fun activate_simprocs ctxt =
if simprocs_active then ctxt
else Simplifier.map_ss (fn ss => ss addsimprocs [lookup_simproc,update_simproc]) ctxt
-
-
- val ctxt' = ctxt
- |> activate_simprocs
- |> (StateFunData.put (lookup_ss',ex_lookup_ss',true))
- in (ctxt', thm) end;
+ in
+ ctxt
+ |> activate_simprocs
+ |> (StateFunData.put (lookup_ss',ex_lookup_ss',true))
+ end);
val setup =
- init_state_fun_data
- #> Attrib.add_attributes
- [("statefun_simp",statefun_simp_attr,"simplification in statespaces")]
+ init_state_fun_data #>
+ Attrib.setup @{binding statefun_simp} (Scan.succeed statefun_simp_attr)
+ "simplification in statespaces"
end
--- a/src/HOL/TLA/Action.thy Sun Mar 15 15:59:44 2009 +0100
+++ b/src/HOL/TLA/Action.thy Sun Mar 15 15:59:44 2009 +0100
@@ -124,12 +124,9 @@
| _ => th;
*}
-setup {*
- Attrib.add_attributes [
- ("action_unlift", Attrib.no_args (Thm.rule_attribute (K action_unlift)), ""),
- ("action_rewrite", Attrib.no_args (Thm.rule_attribute (K action_rewrite)), ""),
- ("action_use", Attrib.no_args (Thm.rule_attribute (K action_use)), "")]
-*}
+attribute_setup action_unlift = {* Scan.succeed (Thm.rule_attribute (K action_unlift)) *} ""
+attribute_setup action_rewrite = {* Scan.succeed (Thm.rule_attribute (K action_rewrite)) *} ""
+attribute_setup action_use = {* Scan.succeed (Thm.rule_attribute (K action_use)) *} ""
(* =========================== square / angle brackets =========================== *)
--- a/src/HOL/TLA/Intensional.thy Sun Mar 15 15:59:44 2009 +0100
+++ b/src/HOL/TLA/Intensional.thy Sun Mar 15 15:59:44 2009 +0100
@@ -294,13 +294,10 @@
| _ => th
*}
-setup {*
- Attrib.add_attributes [
- ("int_unlift", Attrib.no_args (Thm.rule_attribute (K int_unlift)), ""),
- ("int_rewrite", Attrib.no_args (Thm.rule_attribute (K int_rewrite)), ""),
- ("flatten", Attrib.no_args (Thm.rule_attribute (K flatten)), ""),
- ("int_use", Attrib.no_args (Thm.rule_attribute (K int_use)), "")]
-*}
+attribute_setup int_unlift = {* Scan.succeed (Thm.rule_attribute (K int_unlift)) *} ""
+attribute_setup int_rewrite = {* Scan.succeed (Thm.rule_attribute (K int_rewrite)) *} ""
+attribute_setup flatten = {* Scan.succeed (Thm.rule_attribute (K flatten)) *} ""
+attribute_setup int_use = {* Scan.succeed (Thm.rule_attribute (K int_use)) *} ""
lemma Not_Rall: "|- (~(! x. F x)) = (? x. ~F x)"
by (simp add: Valid_def)
--- a/src/HOL/TLA/TLA.thy Sun Mar 15 15:59:44 2009 +0100
+++ b/src/HOL/TLA/TLA.thy Sun Mar 15 15:59:44 2009 +0100
@@ -130,13 +130,11 @@
fun try_rewrite th = temp_rewrite th handle THM _ => temp_use th;
*}
-setup {*
- Attrib.add_attributes [
- ("temp_unlift", Attrib.no_args (Thm.rule_attribute (K temp_unlift)), ""),
- ("temp_rewrite", Attrib.no_args (Thm.rule_attribute (K temp_rewrite)), ""),
- ("temp_use", Attrib.no_args (Thm.rule_attribute (K temp_use)), ""),
- ("try_rewrite", Attrib.no_args (Thm.rule_attribute (K try_rewrite)), "")]
-*}
+attribute_setup temp_unlift = {* Scan.succeed (Thm.rule_attribute (K temp_unlift)) *} ""
+attribute_setup temp_rewrite = {* Scan.succeed (Thm.rule_attribute (K temp_rewrite)) *} ""
+attribute_setup temp_use = {* Scan.succeed (Thm.rule_attribute (K temp_use)) *} ""
+attribute_setup try_rewrite = {* Scan.succeed (Thm.rule_attribute (K try_rewrite)) *} ""
+
(* Update classical reasoner---will be updated once more below! *)
--- a/src/HOL/Tools/Groebner_Basis/normalizer_data.ML Sun Mar 15 15:59:44 2009 +0100
+++ b/src/HOL/Tools/Groebner_Basis/normalizer_data.ML Sun Mar 15 15:59:44 2009 +0100
@@ -191,8 +191,8 @@
in
-val att_syntax = Attrib.syntax
- (Scan.lift (Args.$$$ delN >> K del) ||
+val attribute =
+ Scan.lift (Args.$$$ delN >> K del) ||
((keyword2 semiringN opsN |-- terms) --
(keyword2 semiringN rulesN |-- thms)) --
(optional (keyword2 ringN opsN |-- terms) --
@@ -200,7 +200,7 @@
optional (keyword2 idomN rulesN |-- thms) --
optional (keyword2 idealN rulesN |-- thms)
>> (fn (((sr, r), id), idl) =>
- add {semiring = sr, ring = r, idom = id, ideal = idl}));
+ add {semiring = sr, ring = r, idom = id, ideal = idl});
end;
@@ -208,8 +208,7 @@
(* theory setup *)
val setup =
- Attrib.add_attributes
- [("normalizer", att_syntax, "semiring normalizer data"),
- ("algebra", Attrib.add_del_args add_ss del_ss, "Pre-simplification for algebra")];
+ Attrib.setup @{binding normalizer} attribute "semiring normalizer data" #>
+ Attrib.setup @{binding algebra} (Attrib.add_del add_ss del_ss) "pre-simplification for algebra";
end;
--- a/src/HOL/Tools/Qelim/cooper_data.ML Sun Mar 15 15:59:44 2009 +0100
+++ b/src/HOL/Tools/Qelim/cooper_data.ML Sun Mar 15 15:59:44 2009 +0100
@@ -77,15 +77,14 @@
fun optional scan = Scan.optional scan [];
in
-val att_syntax = Attrib.syntax
- ((Scan.lift (Args.$$$ "del") |-- optional (keyword constsN |-- terms)) >> del ||
- optional (keyword constsN |-- terms) >> add)
+val attribute =
+ (Scan.lift (Args.$$$ "del") |-- optional (keyword constsN |-- terms)) >> del ||
+ optional (keyword constsN |-- terms) >> add
end;
(* theory setup *)
-val setup =
- Attrib.add_attributes [("presburger", att_syntax, "Cooper data")];
+val setup = Attrib.setup @{binding presburger} attribute "Cooper data";
end;
--- a/src/HOL/Tools/Qelim/ferrante_rackoff_data.ML Sun Mar 15 15:59:44 2009 +0100
+++ b/src/HOL/Tools/Qelim/ferrante_rackoff_data.ML Sun Mar 15 15:59:44 2009 +0100
@@ -122,8 +122,8 @@
val terms = thms >> map Drule.dest_term;
in
-val att_syntax = Attrib.syntax
- ((keyword minfN |-- thms)
+val attribute =
+ (keyword minfN |-- thms)
-- (keyword pinfN |-- thms)
-- (keyword nmiN |-- thms)
-- (keyword npiN |-- thms)
@@ -135,14 +135,13 @@
add ({minf = minf, pinf = pinf, nmi = nmi, npi = npi, ld = lin_dense,
qe = hd qe, atoms = atoms},
{isolate_conv = undefined, whatis = undefined, simpset = HOL_ss})
- else error "only one theorem for qe!"))
+ else error "only one theorem for qe!")
end;
(* theory setup *)
-val setup =
- Attrib.add_attributes [("ferrack", att_syntax, "Ferrante Rackoff data")];
+val setup = Attrib.setup @{binding ferrack} attribute "Ferrante Rackoff data";
end;
--- a/src/HOL/Tools/Qelim/langford_data.ML Sun Mar 15 15:59:44 2009 +0100
+++ b/src/HOL/Tools/Qelim/langford_data.ML Sun Mar 15 15:59:44 2009 +0100
@@ -85,8 +85,8 @@
val terms = thms >> map Drule.dest_term;
in
-val att_syntax = Attrib.syntax
- ((keyword qeN |-- thms)
+val attribute =
+ (keyword qeN |-- thms)
-- (keyword gatherN |-- thms)
-- (keyword atomsN |-- terms) >>
(fn ((qes,gs), atoms) =>
@@ -97,14 +97,13 @@
val entry = {qe_bnds = q1, qe_nolb = q2,
qe_noub = q3, gs = gss, gst = gst, atoms = atoms}
in add entry end
- else error "Need 3 theorems for qe and at least one for gs"))
+ else error "Need 3 theorems for qe and at least one for gs")
end;
(* theory setup *)
val setup =
- Attrib.add_attributes
-[("langford", att_syntax, "Langford data"),
- ("langfordsimp", Attrib.add_del_args add_simp del_simp, "Langford simpset")];
+ Attrib.setup @{binding langford} attribute "Langford data" #>
+ Attrib.setup @{binding langfordsimp} (Attrib.add_del add_simp del_simp) "Langford simpset";
end;
--- a/src/HOL/Tools/function_package/fundef_package.ML Sun Mar 15 15:59:44 2009 +0100
+++ b/src/HOL/Tools/function_package/fundef_package.ML Sun Mar 15 15:59:44 2009 +0100
@@ -196,9 +196,8 @@
(* setup *)
val setup =
- Attrib.add_attributes
- [("fundef_cong", Attrib.add_del_args FundefCtxTree.cong_add FundefCtxTree.cong_del,
- "declaration of congruence rule for function definitions")]
+ Attrib.setup @{binding fundef_cong} (Attrib.add_del FundefCtxTree.cong_add FundefCtxTree.cong_del)
+ "declaration of congruence rule for function definitions"
#> setup_case_cong
#> FundefRelation.setup
#> FundefCommon.TerminationSimps.setup
--- a/src/HOL/Tools/inductive_package.ML Sun Mar 15 15:59:44 2009 +0100
+++ b/src/HOL/Tools/inductive_package.ML Sun Mar 15 15:59:44 2009 +0100
@@ -935,8 +935,8 @@
val setup =
Method.setup @{binding ind_cases} ind_cases "dynamic case analysis on predicates" #>
- Attrib.add_attributes [("mono", Attrib.add_del_args mono_add mono_del,
- "declaration of monotonicity rule")];
+ Attrib.setup @{binding mono} (Attrib.add_del mono_add mono_del)
+ "declaration of monotonicity rule";
(* outer syntax *)
--- a/src/HOL/Tools/inductive_realizer.ML Sun Mar 15 15:59:44 2009 +0100
+++ b/src/HOL/Tools/inductive_realizer.ML Sun Mar 15 15:59:44 2009 +0100
@@ -505,13 +505,13 @@
| SOME (SOME sets') => sets \\ sets')
end I);
-val ind_realizer = Attrib.syntax
- ((Scan.option (Scan.lift (Args.$$$ "irrelevant") |--
+val ind_realizer =
+ (Scan.option (Scan.lift (Args.$$$ "irrelevant") |--
Scan.option (Scan.lift (Args.colon) |--
- Scan.repeat1 Args.const))) >> rlz_attrib);
+ Scan.repeat1 Args.const))) >> rlz_attrib;
val setup =
- Attrib.add_attributes [("ind_realizer", ind_realizer, "add realizers for inductive set")];
+ Attrib.setup @{binding ind_realizer} ind_realizer "add realizers for inductive set";
end;
--- a/src/HOL/Tools/inductive_set_package.ML Sun Mar 15 15:59:44 2009 +0100
+++ b/src/HOL/Tools/inductive_set_package.ML Sun Mar 15 15:59:44 2009 +0100
@@ -530,20 +530,17 @@
(* setup theory *)
val setup =
- Attrib.add_attributes
- [("pred_set_conv", Attrib.no_args pred_set_conv_att,
- "declare rules for converting between predicate and set notation"),
- ("to_set", Attrib.syntax (Attrib.thms >> to_set_att),
- "convert rule to set notation"),
- ("to_pred", Attrib.syntax (Attrib.thms >> to_pred_att),
- "convert rule to predicate notation")] #>
+ Attrib.setup @{binding pred_set_conv} (Scan.succeed pred_set_conv_att)
+ "declare rules for converting between predicate and set notation" #>
+ Attrib.setup @{binding to_set} (Attrib.thms >> to_set_att) "convert rule to set notation" #>
+ Attrib.setup @{binding to_pred} (Attrib.thms >> to_pred_att) "convert rule to predicate notation" #>
Code.add_attribute ("ind_set",
Scan.option (Args.$$$ "target" |-- Args.colon |-- Args.name) >> code_ind_att) #>
Codegen.add_preprocessor codegen_preproc #>
- Attrib.add_attributes [("mono_set", Attrib.add_del_args mono_add_att mono_del_att,
- "declaration of monotonicity rule for set operators")] #>
- Context.theory_map (Simplifier.map_ss (fn ss =>
- ss addsimprocs [collect_mem_simproc]));
+ Attrib.setup @{binding mono_set} (Attrib.add_del mono_add_att mono_del_att)
+ "declaration of monotonicity rule for set operators" #>
+ Context.theory_map (Simplifier.map_ss (fn ss => ss addsimprocs [collect_mem_simproc]));
+
(* outer syntax *)
--- a/src/HOL/Tools/lin_arith.ML Sun Mar 15 15:59:44 2009 +0100
+++ b/src/HOL/Tools/lin_arith.ML Sun Mar 15 15:59:44 2009 +0100
@@ -930,8 +930,8 @@
Context.mapping
(setup_options #>
Method.setup @{binding arith} arith_method "decide linear arithmetic" #>
- Attrib.add_attributes [("arith_split", Attrib.no_args arith_split_add,
- "declaration of split rules for arithmetic procedure")]) I;
+ Attrib.setup @{binding arith_split} (Scan.succeed arith_split_add)
+ "declaration of split rules for arithmetic procedure") I;
end;
--- a/src/HOL/Tools/recdef_package.ML Sun Mar 15 15:59:44 2009 +0100
+++ b/src/HOL/Tools/recdef_package.ML Sun Mar 15 15:59:44 2009 +0100
@@ -282,10 +282,12 @@
(* setup theory *)
val setup =
- Attrib.add_attributes
- [(recdef_simpN, Attrib.add_del_args simp_add simp_del, "declaration of recdef simp rule"),
- (recdef_congN, Attrib.add_del_args cong_add cong_del, "declaration of recdef cong rule"),
- (recdef_wfN, Attrib.add_del_args wf_add wf_del, "declaration of recdef wf rule")];
+ Attrib.setup @{binding recdef_simp} (Attrib.add_del simp_add simp_del)
+ "declaration of recdef simp rule" #>
+ Attrib.setup @{binding recdef_cong} (Attrib.add_del cong_add cong_del)
+ "declaration of recdef cong rule" #>
+ Attrib.setup @{binding recdef_wf} (Attrib.add_del wf_add wf_del)
+ "declaration of recdef wf rule";
(* outer syntax *)
--- a/src/HOL/Tools/res_axioms.ML Sun Mar 15 15:59:44 2009 +0100
+++ b/src/HOL/Tools/res_axioms.ML Sun Mar 15 15:59:44 2009 +0100
@@ -528,12 +528,11 @@
(** Attribute for converting a theorem into clauses **)
-val clausify = Attrib.syntax (Scan.lift OuterParse.nat
- >> (fn i => Thm.rule_attribute (fn context => fn th =>
- Meson.make_meta_clause (nth (cnf_axiom (Context.theory_of context) th) i))));
+val clausify = Scan.lift OuterParse.nat >>
+ (fn i => Thm.rule_attribute (fn context => fn th =>
+ Meson.make_meta_clause (nth (cnf_axiom (Context.theory_of context) th) i)));
-val setup_attrs = Attrib.add_attributes
- [("clausify", clausify, "conversion of theorem to clauses")];
+val setup_attrs = Attrib.setup @{binding clausify} clausify "conversion of theorem to clauses";
--- a/src/HOL/Tools/split_rule.ML Sun Mar 15 15:59:44 2009 +0100
+++ b/src/HOL/Tools/split_rule.ML Sun Mar 15 15:59:44 2009 +0100
@@ -145,18 +145,17 @@
(* FIXME dynamically scoped due to Args.name_source/pair_tac *)
-val split_format = Attrib.syntax (Scan.lift
+val split_format = Scan.lift
(Args.parens (Args.$$$ "complete") >> K (Thm.rule_attribute (K complete_split_rule)) ||
OuterParse.and_list1 (Scan.repeat Args.name_source)
>> (fn xss => Thm.rule_attribute (fn context =>
- split_rule_goal (Context.proof_of context) xss))));
+ split_rule_goal (Context.proof_of context) xss)));
val setup =
- Attrib.add_attributes
- [("split_format", split_format,
- "split pair-typed subterms in premises, or function arguments"),
- ("split_rule", Attrib.no_args (Thm.rule_attribute (K split_rule)),
- "curries ALL function variables occurring in a rule's conclusion")];
+ Attrib.setup @{binding split_format} split_format
+ "split pair-typed subterms in premises, or function arguments" #>
+ Attrib.setup @{binding split_rule} (Scan.succeed (Thm.rule_attribute (K split_rule)))
+ "curries ALL function variables occurring in a rule's conclusion";
end;
--- a/src/HOL/UNITY/Comp/Alloc.thy Sun Mar 15 15:59:44 2009 +0100
+++ b/src/HOL/UNITY/Comp/Alloc.thy Sun Mar 15 15:59:44 2009 +0100
@@ -298,7 +298,7 @@
lemmas lessThanBspec = lessThan_iff [THEN iffD2, THEN [2] bspec]
-setup {*
+attribute_setup normalized = {*
let
fun normalized th =
normalized (th RS spec
@@ -307,9 +307,9 @@
handle THM _ => th RS (@{thm guarantees_INT_right_iff} RS iffD1))
handle THM _ => th;
in
- Attrib.add_attributes [("normalized", Attrib.no_args (Thm.rule_attribute (K normalized)), "")]
+ Scan.succeed (Thm.rule_attribute (K normalized))
end
-*}
+*} ""
(*** bijectivity of sysOfAlloc [MUST BE AUTOMATED] ***)
ML {*
--- a/src/HOL/ex/predicate_compile.ML Sun Mar 15 15:59:44 2009 +0100
+++ b/src/HOL/ex/predicate_compile.ML Sun Mar 15 15:59:44 2009 +0100
@@ -1334,11 +1334,11 @@
val code_ind_cases_attrib = attrib add_elim_thm
-val setup = Attrib.add_attributes
- [("code_ind_intros", Attrib.no_args code_ind_intros_attrib,
- "adding alternative introduction rules for code generation of inductive predicates"),
- ("code_ind_cases", Attrib.no_args code_ind_cases_attrib,
- "adding alternative elimination rules for code generation of inductive predicates")]
+val setup =
+ Attrib.setup @{binding code_ind_intros} (Scan.succeed code_ind_intros_attrib)
+ "adding alternative introduction rules for code generation of inductive predicates" #>
+ Attrib.setup @{binding code_ind_cases} (Scan.succeed code_ind_cases_attrib)
+ "adding alternative elimination rules for code generation of inductive predicates";
end;
--- a/src/Provers/clasimp.ML Sun Mar 15 15:59:44 2009 +0100
+++ b/src/Provers/clasimp.ML Sun Mar 15 15:59:44 2009 +0100
@@ -268,10 +268,10 @@
val iff_add' = attrib' addIffs_generic;
val iff_del = attrib (op delIffs) o attrib' delIffs_generic;
-val iff_att = Attrib.syntax (Scan.lift
+fun iff_att x = (Scan.lift
(Args.del >> K iff_del ||
Scan.option Args.add -- Args.query >> K iff_add' ||
- Scan.option Args.add >> K iff_add));
+ Scan.option Args.add >> K iff_add)) x;
(* method modifiers *)
@@ -311,8 +311,7 @@
(* theory setup *)
val clasimp_setup =
- (Attrib.add_attributes
- [("iff", iff_att, "declaration of Simplifier / Classical rules")] #>
+ (Attrib.setup @{binding iff} 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"),
--- a/src/Provers/classical.ML Sun Mar 15 15:59:44 2009 +0100
+++ b/src/Provers/classical.ML Sun Mar 15 15:59:44 2009 +0100
@@ -215,7 +215,7 @@
(*Creates rules to eliminate ~A, from rules to introduce A*)
fun swapify intrs = intrs RLN (2, [Data.swap]);
-fun swapped x = Attrib.no_args (fn (x, th) => (x, th RSN (2, Data.swap))) x;
+val swapped = Thm.rule_attribute (fn _ => fn th => th RSN (2, Data.swap));
(*Uses introduction rules in the normal way, or on negated assumptions,
trying rules in order. *)
@@ -956,16 +956,17 @@
val destN = "dest";
val ruleN = "rule";
-val setup_attrs = Attrib.add_attributes
- [("swapped", swapped, "classical swap of introduction rule"),
- (destN, ContextRules.add_args safe_dest haz_dest ContextRules.dest_query,
- "declaration of Classical destruction rule"),
- (elimN, ContextRules.add_args safe_elim haz_elim ContextRules.elim_query,
- "declaration of Classical elimination rule"),
- (introN, ContextRules.add_args safe_intro haz_intro ContextRules.intro_query,
- "declaration of Classical introduction rule"),
- (ruleN, Attrib.syntax (Scan.lift Args.del >> K rule_del),
- "remove declaration of intro/elim/dest rule")];
+val setup_attrs =
+ Attrib.setup @{binding swapped} (Scan.succeed swapped)
+ "classical swap of introduction rule" #>
+ Attrib.setup @{binding dest} (ContextRules.add safe_dest haz_dest ContextRules.dest_query)
+ "declaration of Classical destruction rule" #>
+ Attrib.setup @{binding elim} (ContextRules.add safe_elim haz_elim ContextRules.elim_query)
+ "declaration of Classical elimination rule" #>
+ Attrib.setup @{binding intro} (ContextRules.add safe_intro haz_intro ContextRules.intro_query)
+ "declaration of Classical introduction rule" #>
+ Attrib.setup @{binding rule} (Scan.lift Args.del >> K rule_del)
+ "remove declaration of intro/elim/dest rule";
--- a/src/Provers/splitter.ML Sun Mar 15 15:59:44 2009 +0100
+++ b/src/Provers/splitter.ML Sun Mar 15 15:59:44 2009 +0100
@@ -479,8 +479,7 @@
(* theory setup *)
val setup =
- Attrib.add_attributes
- [(splitN, Attrib.add_del_args split_add split_del, "declaration of case split rule")] #>
+ Attrib.setup @{binding split} (Attrib.add_del split_add split_del) "declare case split rule" #>
Method.setup @{binding split} split_meth "apply case split rule";
end;
--- a/src/Pure/Isar/calculation.ML Sun Mar 15 15:59:44 2009 +0100
+++ b/src/Pure/Isar/calculation.ML Sun Mar 15 15:59:44 2009 +0100
@@ -88,14 +88,13 @@
(* concrete syntax *)
-val trans_att = Attrib.add_del_args trans_add trans_del;
-val sym_att = Attrib.add_del_args sym_add sym_del;
-
val _ = Context.>> (Context.map_theory
- (Attrib.add_attributes
- [("trans", trans_att, "declaration of transitivity rule"),
- ("sym", sym_att, "declaration of symmetry rule"),
- ("symmetric", Attrib.no_args symmetric, "resolution with symmetry rule")] #>
+ (Attrib.setup (Binding.name "trans") (Attrib.add_del trans_add trans_del)
+ "declaration of transitivity rule" #>
+ Attrib.setup (Binding.name "sym") (Attrib.add_del sym_add sym_del)
+ "declaration of symmetry rule" #>
+ Attrib.setup (Binding.name "symmetric") (Scan.succeed symmetric)
+ "resolution with symmetry rule" #>
PureThy.add_thms
[((Binding.empty, transitive_thm), [trans_add]),
((Binding.empty, symmetric_thm), [sym_add])] #> snd));
--- a/src/Pure/Isar/code.ML Sun Mar 15 15:59:44 2009 +0100
+++ b/src/Pure/Isar/code.ML Sun Mar 15 15:59:44 2009 +0100
@@ -100,12 +100,11 @@
val _ =
let
- val code_attr = Attrib.syntax (Scan.peek (fn context =>
- List.foldr op || Scan.fail (map snd (CodeAttr.get (Context.theory_of context)))));
+ val code_attr = Scan.peek (fn context =>
+ List.foldr op || Scan.fail (map snd (CodeAttr.get (Context.theory_of context))));
in
Context.>> (Context.map_theory
- (Attrib.add_attributes
- [("code", code_attr, "declare theorems for code generation")]))
+ (Attrib.setup (Binding.name "code") code_attr "declare theorems for code generation"))
end;
--- a/src/Pure/Isar/rule_insts.ML Sun Mar 15 15:59:44 2009 +0100
+++ b/src/Pure/Isar/rule_insts.ML Sun Mar 15 15:59:44 2009 +0100
@@ -218,8 +218,8 @@
in
-val where_att = Attrib.syntax (Scan.lift (P.and_list inst) >> (fn args =>
- Thm.rule_attribute (fn context => read_instantiate_mixed (Context.proof_of context) args)));
+fun where_att x = (Scan.lift (P.and_list inst) >> (fn args =>
+ Thm.rule_attribute (fn context => read_instantiate_mixed (Context.proof_of context) args))) x;
end;
@@ -241,8 +241,8 @@
in
-val of_att = Attrib.syntax (Scan.lift insts >> (fn args =>
- Thm.rule_attribute (fn context => read_instantiate_mixed' (Context.proof_of context) args)));
+fun of_att x = (Scan.lift insts >> (fn args =>
+ Thm.rule_attribute (fn context => read_instantiate_mixed' (Context.proof_of context) args))) x;
end;
@@ -250,9 +250,8 @@
(* setup *)
val _ = Context.>> (Context.map_theory
- (Attrib.add_attributes
- [("where", where_att, "named instantiation of theorem"),
- ("of", of_att, "positional instantiation of theorem")]));
+ (Attrib.setup (Binding.name "where") where_att "named instantiation of theorem" #>
+ Attrib.setup (Binding.name "of") of_att "positional instantiation of theorem"));
--- a/src/Pure/Proof/extraction.ML Sun Mar 15 15:59:44 2009 +0100
+++ b/src/Pure/Proof/extraction.ML Sun Mar 15 15:59:44 2009 +0100
@@ -374,8 +374,7 @@
val add_expand_thms = fold add_expand_thm;
-val extraction_expand =
- Attrib.no_args (Thm.declaration_attribute (fn th => Context.mapping (add_expand_thm th) I));
+val extraction_expand = Thm.declaration_attribute (fn th => Context.mapping (add_expand_thm th) I);
(** types with computational content **)
@@ -435,9 +434,8 @@
"(realizes (r) (!!x. PROP P (x))) == \
\ (!!x. PROP realizes (r (x)) (PROP P (x)))"] #>
- Attrib.add_attributes
- [("extraction_expand", extraction_expand,
- "specify theorems / definitions to be expanded during extraction")]));
+ Attrib.setup (Binding.name "extraction_expand") (Scan.succeed extraction_expand)
+ "specify theorems / definitions to be expanded during extraction"));
(**** extract program ****)
--- a/src/Pure/Tools/named_thms.ML Sun Mar 15 15:59:44 2009 +0100
+++ b/src/Pure/Tools/named_thms.ML Sun Mar 15 15:59:44 2009 +0100
@@ -34,7 +34,7 @@
val del = Thm.declaration_attribute del_thm;
val setup =
- Attrib.add_attributes [(name, Attrib.add_del_args add del, "declaration of " ^ description)] #>
+ Attrib.setup (Binding.name name) (Attrib.add_del add del) ("declaration of " ^ description) #>
PureThy.add_thms_dynamic (Binding.name name, Data.get);
end;
--- a/src/Pure/simplifier.ML Sun Mar 15 15:59:44 2009 +0100
+++ b/src/Pure/simplifier.ML Sun Mar 15 15:59:44 2009 +0100
@@ -334,11 +334,11 @@
in
-val simproc_att = Attrib.syntax
- (Scan.peek (fn context =>
+val simproc_att =
+ Scan.peek (fn context =>
add_del :|-- (fn decl =>
Scan.repeat1 (Args.named_attribute (decl o get_simproc context))
- >> (Library.apply o map Morphism.form))));
+ >> (Library.apply o map Morphism.form)));
end;
@@ -355,10 +355,10 @@
in
-val simplified =
- Attrib.syntax (conv_mode -- Attrib.thms >> (fn (f, ths) => Thm.rule_attribute (fn context =>
+val simplified = conv_mode -- Attrib.thms >>
+ (fn (f, ths) => Thm.rule_attribute (fn context =>
f ((if null ths then I else MetaSimplifier.clear_ss)
- (local_simpset_of (Context.proof_of context)) addsimps ths))));
+ (local_simpset_of (Context.proof_of context)) addsimps ths)));
end;
@@ -366,11 +366,12 @@
(* setup attributes *)
val _ = Context.>> (Context.map_theory
- (Attrib.add_attributes
- [(simpN, Attrib.add_del_args simp_add simp_del, "declaration of Simplifier rewrite rule"),
- (congN, Attrib.add_del_args cong_add cong_del, "declaration of Simplifier congruence rule"),
- ("simproc", simproc_att, "declaration of simplification procedures"),
- ("simplified", simplified, "simplified rule")]));
+ (Attrib.setup (Binding.name simpN) (Attrib.add_del simp_add simp_del)
+ "declaration of Simplifier rewrite rule" #>
+ Attrib.setup (Binding.name congN) (Attrib.add_del cong_add cong_del)
+ "declaration of Simplifier congruence rule" #>
+ Attrib.setup (Binding.name "simproc") simproc_att "declaration of simplification procedures" #>
+ Attrib.setup (Binding.name "simplified") simplified "simplified rule"));
--- a/src/Tools/induct.ML Sun Mar 15 15:59:44 2009 +0100
+++ b/src/Tools/induct.ML Sun Mar 15 15:59:44 2009 +0100
@@ -253,11 +253,11 @@
Scan.lift (Args.$$$ k -- Args.colon) |-- arg ||
Scan.lift (Args.$$$ k) >> K "";
-fun attrib add_type add_pred del = Attrib.syntax
- (spec typeN Args.tyname >> add_type ||
+fun attrib add_type add_pred del =
+ spec typeN Args.tyname >> add_type ||
spec predN Args.const >> add_pred ||
spec setN Args.const >> add_pred ||
- Scan.lift Args.del >> K del);
+ Scan.lift Args.del >> K del;
val cases_att = attrib cases_type cases_pred cases_del;
val induct_att = attrib induct_type induct_pred induct_del;
@@ -265,10 +265,10 @@
in
-val attrib_setup = Attrib.add_attributes
- [(casesN, cases_att, "declaration of cases rule"),
- (inductN, induct_att, "declaration of induction rule"),
- (coinductN, coinduct_att, "declaration of coinduction rule")];
+val attrib_setup =
+ Attrib.setup @{binding cases} cases_att "declaration of cases rule" #>
+ Attrib.setup @{binding induct} induct_att "declaration of induction rule" #>
+ Attrib.setup @{binding coinduct} coinduct_att "declaration of coinduction rule";
end;
--- a/src/ZF/Tools/typechk.ML Sun Mar 15 15:59:44 2009 +0100
+++ b/src/ZF/Tools/typechk.ML Sun Mar 15 15:59:44 2009 +0100
@@ -110,8 +110,6 @@
(* concrete syntax *)
-val TC_att = Attrib.add_del_args TC_add TC_del;
-
val typecheck_meth =
Method.only_sectioned_args
[Args.add -- Args.colon >> K (I, TC_add),
@@ -127,7 +125,7 @@
(* theory setup *)
val setup =
- Attrib.add_attributes [("TC", TC_att, "declaration of type-checking rule")] #>
+ Attrib.setup @{binding TC} (Attrib.add_del TC_add TC_del) "declaration of type-checking rule" #>
Method.add_methods [("typecheck", typecheck_meth, "ZF type-checking")] #>
Simplifier.map_simpset (fn ss => ss setSolver type_solver);