# HG changeset patch # User wenzelm # Date 1136918044 -3600 # Node ID 89a7978f90e1c38db80db6bf85eb450d282e7239 # Parent 6954633b6a7674bc6558a05f46320eb19e935400 generic attributes; diff -r 6954633b6a76 -r 89a7978f90e1 src/HOL/Tools/datatype_package.ML --- a/src/HOL/Tools/datatype_package.ML Tue Jan 10 19:33:42 2006 +0100 +++ b/src/HOL/Tools/datatype_package.ML Tue Jan 10 19:34:04 2006 +0100 @@ -365,10 +365,10 @@ fun proj i = ProjectRule.project induction (i + 1); fun named_rules (name, {index, exhaustion, ...}: datatype_info) = - [(("", proj index), [InductAttrib.induct_type_global name]), - (("", exhaustion), [InductAttrib.cases_type_global name])]; + [(("", proj index), [Attrib.theory (InductAttrib.induct_type name)]), + (("", exhaustion), [Attrib.theory (InductAttrib.cases_type name)])]; fun unnamed_rule i = - (("", proj i), [Drule.kind_internal, InductAttrib.induct_type_global ""]); + (("", proj i), [Drule.kind_internal, Attrib.theory (InductAttrib.induct_type "")]); in PureThy.add_thms (List.concat (map named_rules infos) @ diff -r 6954633b6a76 -r 89a7978f90e1 src/HOL/Tools/inductive_package.ML --- a/src/HOL/Tools/inductive_package.ML Tue Jan 10 19:33:42 2006 +0100 +++ b/src/HOL/Tools/inductive_package.ML Tue Jan 10 19:34:04 2006 +0100 @@ -435,12 +435,12 @@ thy |> Theory.parent_path |> Theory.add_path (Sign.base_name name) - |> PureThy.add_thms [(("cases", elim), [InductAttrib.cases_set_global name])] |> snd + |> PureThy.add_thms [(("cases", elim), [Attrib.theory (InductAttrib.cases_set name)])] |> snd |> Theory.restore_naming thy; val cases_specs = if no_elim then [] else map2 cases_spec names elims; val induct_att = - if coind then InductAttrib.coinduct_set_global else InductAttrib.induct_set_global; + Attrib.theory o (if coind then InductAttrib.coinduct_set else InductAttrib.induct_set); val induct_specs = if no_induct then I else diff -r 6954633b6a76 -r 89a7978f90e1 src/HOL/Tools/record_package.ML --- a/src/HOL/Tools/record_package.ML Tue Jan 10 19:33:42 2006 +0100 +++ b/src/HOL/Tools/record_package.ML Tue Jan 10 19:34:04 2006 +0100 @@ -1215,8 +1215,8 @@ (* attributes *) fun case_names_fields x = RuleCases.case_names ["fields"] x; -fun induct_type_global name = [case_names_fields, InductAttrib.induct_type_global name]; -fun cases_type_global name = [case_names_fields, InductAttrib.cases_type_global name]; +fun induct_type_global name = [case_names_fields, Attrib.theory (InductAttrib.induct_type name)]; +fun cases_type_global name = [case_names_fields, Attrib.theory (InductAttrib.cases_type name)]; (* tactics *) diff -r 6954633b6a76 -r 89a7978f90e1 src/HOL/Tools/typedef_package.ML --- a/src/HOL/Tools/typedef_package.ML Tue Jan 10 19:33:42 2006 +0100 +++ b/src/HOL/Tools/typedef_package.ML Tue Jan 10 19:34:04 2006 +0100 @@ -176,13 +176,17 @@ ((Rep_name ^ "_inject", make Rep_inject), []), ((Abs_name ^ "_inject", make Abs_inject), []), ((Rep_name ^ "_cases", make Rep_cases), - [RuleCases.case_names [Rep_name], InductAttrib.cases_set_global full_name]), + [RuleCases.case_names [Rep_name], + Attrib.theory (InductAttrib.cases_set full_name)]), ((Abs_name ^ "_cases", make Abs_cases), - [RuleCases.case_names [Abs_name], InductAttrib.cases_type_global full_tname]), + [RuleCases.case_names [Abs_name], + Attrib.theory (InductAttrib.cases_type full_tname)]), ((Rep_name ^ "_induct", make Rep_induct), - [RuleCases.case_names [Rep_name], InductAttrib.induct_set_global full_name]), + [RuleCases.case_names [Rep_name], + Attrib.theory (InductAttrib.induct_set full_name)]), ((Abs_name ^ "_induct", make Abs_induct), - [RuleCases.case_names [Abs_name], InductAttrib.induct_type_global full_tname])]) + [RuleCases.case_names [Abs_name], + Attrib.theory (InductAttrib.induct_type full_tname)])]) ||> Theory.parent_path; val result = {type_definition = type_definition, set_def = set_def, Rep = Rep, Rep_inverse = Rep_inverse, Abs_inverse = Abs_inverse, diff -r 6954633b6a76 -r 89a7978f90e1 src/Provers/classical.ML --- a/src/Provers/classical.ML Tue Jan 10 19:33:42 2006 +0100 +++ b/src/Provers/classical.ML Tue Jan 10 19:34:04 2006 +0100 @@ -968,7 +968,7 @@ val haz_dest_global = change_global_cs (op addDs); val haz_elim_global = change_global_cs (op addEs); val haz_intro_global = change_global_cs (op addIs); -val rule_del_global = change_global_cs (op delrules) o ContextRules.rule_del_global; +val rule_del_global = change_global_cs (op delrules) o Attrib.theory ContextRules.rule_del; val safe_dest_local = change_local_cs (op addSDs); val safe_elim_local = change_local_cs (op addSEs); @@ -976,7 +976,7 @@ val haz_dest_local = change_local_cs (op addDs); val haz_elim_local = change_local_cs (op addEs); val haz_intro_local = change_local_cs (op addIs); -val rule_del_local = change_local_cs (op delrules) o ContextRules.rule_del_local; +val rule_del_local = change_local_cs (op delrules) o Attrib.context ContextRules.rule_del; (* tactics referring to the implicit claset *) @@ -1019,16 +1019,16 @@ val setup_attrs = Attrib.add_attributes [("swapped", (swapped, swapped), "classical swap of introduction rule"), (destN, - (add_rule ContextRules.dest_query_global haz_dest_global safe_dest_global, - add_rule ContextRules.dest_query_local haz_dest_local safe_dest_local), + (add_rule (Attrib.theory o ContextRules.dest_query) haz_dest_global safe_dest_global, + add_rule (Attrib.context o ContextRules.dest_query) haz_dest_local safe_dest_local), "declaration of destruction rule"), (elimN, - (add_rule ContextRules.elim_query_global haz_elim_global safe_elim_global, - add_rule ContextRules.elim_query_local haz_elim_local safe_elim_local), + (add_rule (Attrib.theory o ContextRules.elim_query) haz_elim_global safe_elim_global, + add_rule (Attrib.context o ContextRules.elim_query) haz_elim_local safe_elim_local), "declaration of elimination rule"), (introN, - (add_rule ContextRules.intro_query_global haz_intro_global safe_intro_global, - add_rule ContextRules.intro_query_local haz_intro_local safe_intro_local), + (add_rule (Attrib.theory o ContextRules.intro_query) haz_intro_global safe_intro_global, + add_rule (Attrib.context o ContextRules.intro_query) haz_intro_local safe_intro_local), "declaration of introduction rule"), (ruleN, (del_rule rule_del_global, del_rule rule_del_local), "remove declaration of intro/elim/dest rule")]; diff -r 6954633b6a76 -r 89a7978f90e1 src/Pure/Isar/obtain.ML --- a/src/Pure/Isar/obtain.ML Tue Jan 10 19:33:42 2006 +0100 +++ b/src/Pure/Isar/obtain.ML Tue Jan 10 19:34:04 2006 +0100 @@ -134,7 +134,8 @@ |> Proof.have_i NONE (K Seq.single) [(("", []), [(obtain_prop, ([], []))])] int |> Proof.proof (SOME Method.succeed_text) |> Seq.hd |> Proof.fix_i [([thesisN], NONE)] - |> Proof.assume_i [((thatN, [ContextRules.intro_query_local NONE]), [(that_prop, ([], []))])] + |> Proof.assume_i + [((thatN, [Attrib.context (ContextRules.intro_query NONE)]), [(that_prop, ([], []))])] |> `Proof.the_facts ||> Proof.chain_facts chain_facts ||> Proof.show_i NONE after_qed [(("", []), [(thesis, ([], []))])] false diff -r 6954633b6a76 -r 89a7978f90e1 src/ZF/Tools/inductive_package.ML --- a/src/ZF/Tools/inductive_package.ML Tue Jan 10 19:33:42 2006 +0100 +++ b/src/ZF/Tools/inductive_package.ML Tue Jan 10 19:34:04 2006 +0100 @@ -514,8 +514,9 @@ val ([induct', mutual_induct'], thy') = thy - |> PureThy.add_thms [((co_prefix ^ "induct", induct), [case_names, InductAttrib.induct_set_global big_rec_name]), - (("mutual_induct", mutual_induct), [case_names])]; + |> PureThy.add_thms [((co_prefix ^ "induct", induct), + [case_names, Attrib.theory (InductAttrib.induct_set big_rec_name)]), + (("mutual_induct", mutual_induct), [case_names])]; in ((thy', induct'), mutual_induct') end; (*of induction_rules*) @@ -536,7 +537,7 @@ |> PureThy.add_thms [(("bnd_mono", bnd_mono), []), (("dom_subset", dom_subset), []), - (("cases", elim), [case_names, InductAttrib.cases_set_global big_rec_name])] + (("cases", elim), [case_names, Attrib.theory (InductAttrib.cases_set big_rec_name)])] ||>> (PureThy.add_thmss o map Thm.no_attributes) [("defs", defs), ("intros", intrs)];