(*  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 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 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)];

 val _ =

   OuterSyntax.improper_command ("print_" ^ name ^ "_rules") ("print " ^ description)

     OuterKeyword.diag

     (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o

       Toplevel.keep (Pretty.writeln o pretty o Toplevel.context_of)));

 end;