src/Pure/Tools/named_thms.ML

+(*  Title:      Pure/Tools/named_thms.ML
+    ID:         $Id$
+    Author:     Makarius
+
+Named collections of theorems in canonical order.
+*)
+
+signature NAMED_THMS =
+sig
+  val get: Proof.context -> thm list
+  val pretty: Proof.context -> Pretty.T
+  val print: Proof.context -> unit
+  val add: attribute
+  val del: attribute
+  val setup: theory -> theory
+end;
+
+functor NamedThmsFun(val name: string val description: string): NAMED_THMS =
+struct
+
+structure Data = GenericDataFun
+(
+  type T = thm list;
+  val empty = [];
+  val extend = I;
+  fun merge _ = Thm.merge_thms;
+);
+
+val get = Data.get o Context.Proof;
+
+fun pretty ctxt =
+  Pretty.big_list (description ^ ":") (map (ProofContext.pretty_thm ctxt) (get ctxt));
+
+val print = Pretty.writeln o pretty;
+
+val add = Thm.declaration_attribute (Data.map o Thm.add_thm);
+val del = Thm.declaration_attribute (Data.map o Thm.del_thm);
+
+val setup =
+  Attrib.add_attributes [(name, Attrib.add_del_args add del, "declaration of " ^ description)];
+
+end;