# HG changeset patch
# User wenzelm
# Date 1185712203 -7200
# Node ID 47b588ce11ec06a9e42bea38b8c385d3460430ae
# Parent  10f681043e078f6fced503f707586ca207962200
Named collections of theorems in canonical order.

diff -r 10f681043e07 -r 47b588ce11ec src/Pure/Tools/named_thms.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Tools/named_thms.ML	Sun Jul 29 14:30:03 2007 +0200
@@ -0,0 +1,42 @@
+(*  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;