# HG changeset patch # User wenzelm # Date 1201363720 -3600 # Node ID 870ae1d0452ea54b15851d8dc3390ad76e8f81f9 # Parent fa26b76d3e7e340817b52ad21adf24e70e7cce0a added theorem group operations; note_thmss: add kind to *all* intermediate thms; get_kind: default to empty name; diff -r fa26b76d3e7e -r 870ae1d0452e src/Pure/pure_thy.ML --- a/src/Pure/pure_thy.ML Sat Jan 26 17:08:39 2008 +0100 +++ b/src/Pure/pure_thy.ML Sat Jan 26 17:08:40 2008 +0100 @@ -34,6 +34,9 @@ val has_name_hint: thm -> bool val get_name_hint: thm -> string val put_name_hint: string -> thm -> thm + val get_group: thm -> string option + val put_group: string -> thm -> thm + val group: string -> attribute val has_kind: thm -> bool val get_kind: thm -> string val kind_rule: string -> thm -> thm @@ -77,6 +80,8 @@ (thmref * attribute list) list) list -> theory -> (bstring * thm list) list * theory val note_thmss_i: string -> ((bstring * attribute list) * (thm list * attribute list) list) list -> theory -> (bstring * thm list) list * theory + val note_thmss_grouped: string -> string -> ((bstring * attribute list) * + (thm list * attribute list) list) list -> theory -> (bstring * thm list) list * theory val note_thmss_qualified: string -> string -> ((bstring * attribute list) * (thm list * attribute list) list) list -> theory -> (bstring * thm list) list * theory val add_axioms: ((bstring * string) * attribute list) list -> theory -> thm list * theory @@ -122,12 +127,22 @@ fun put_name_hint name = untag_rule Markup.nameN #> tag_rule (Markup.nameN, name); +(* theorem groups *) + +fun get_group thm = AList.lookup (op =) (Thm.get_tags thm) Markup.groupN; + +fun put_group name = + if name = "" then I else Thm.map_tags (AList.update (op =) (Markup.groupN, name)); + +fun group name = Thm.rule_attribute (K (put_group name)); + + (* theorem kinds *) fun the_kind thm = the (AList.lookup (op =) (Thm.get_tags thm) Markup.kindN); val has_kind = can the_kind; -val get_kind = the_default "??.unknown" o try the_kind; +val get_kind = the_default "" o try the_kind; fun kind_rule k = tag_rule (Markup.kindN, k) o untag_rule Markup.kindN; fun kind k x = if k = "" then x else Thm.rule_attribute (K (kind_rule k)) x; @@ -384,18 +399,19 @@ local -fun gen_note_thmss get k = fold_map (fn ((bname, more_atts), ths_atts) => fn thy => +fun gen_note_thmss get tag = fold_map (fn ((bname, more_atts), ths_atts) => fn thy => let fun app (x, (ths, atts)) = foldl_map (Thm.theory_attributes atts) (x, ths); val (thms, thy') = thy |> enter_thms (name_thmss true) (name_thms false true) (apsnd flat o foldl_map app) - (bname, map (fn (ths, atts) => (get thy ths, atts @ more_atts @ [kind k])) ths_atts); + (bname, map (fn (ths, atts) => (get thy ths, surround tag (atts @ more_atts))) ths_atts); in ((bname, thms), thy') end); in -val note_thmss = gen_note_thmss get_thms; -val note_thmss_i = gen_note_thmss (K I); +fun note_thmss k = gen_note_thmss get_thms (kind k); +fun note_thmss_i k = gen_note_thmss (K I) (kind k); +fun note_thmss_grouped k g = gen_note_thmss (K I) (kind k #> group g); end;