src/Pure/Tools/named_thms.ML
author wenzelm
Thu Mar 20 16:04:34 2008 +0100 (2008-03-20)
changeset 26363 9d95309f8069
parent 24867 e5b55d7be9bb
child 26397 df68e8dfd0e3
permissions -rw-r--r--
export add/del_thm;
     1 (*  Title:      Pure/Tools/named_thms.ML
     2     ID:         $Id$
     3     Author:     Makarius
     4 
     5 Named collections of theorems in canonical order.
     6 *)
     7 
     8 signature NAMED_THMS =
     9 sig
    10   val get: Proof.context -> thm list
    11   val pretty: Proof.context -> Pretty.T
    12   val add_thm: thm -> Context.generic -> Context.generic
    13   val del_thm: thm -> Context.generic -> Context.generic
    14   val add: attribute
    15   val del: attribute
    16   val setup: theory -> theory
    17 end;
    18 
    19 functor NamedThmsFun(val name: string val description: string): NAMED_THMS =
    20 struct
    21 
    22 structure Data = GenericDataFun
    23 (
    24   type T = thm list;
    25   val empty = [];
    26   val extend = I;
    27   fun merge _ = Thm.merge_thms;
    28 );
    29 
    30 val get = Data.get o Context.Proof;
    31 
    32 fun pretty ctxt =
    33   Pretty.big_list (description ^ ":") (map (ProofContext.pretty_thm ctxt) (get ctxt));
    34 
    35 val add_thm = Data.map o Thm.add_thm;
    36 val del_thm = Data.map o Thm.del_thm;
    37 
    38 val add = Thm.declaration_attribute add_thm;
    39 val del = Thm.declaration_attribute del_thm;
    40 
    41 val setup =
    42   Attrib.add_attributes [(name, Attrib.add_del_args add del, "declaration of " ^ description)];
    43 
    44 val _ =
    45   OuterSyntax.improper_command ("print_" ^ name ^ "_rules") ("print " ^ description)
    46     OuterKeyword.diag
    47     (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
    48       Toplevel.keep (Pretty.writeln o pretty o Toplevel.context_of)));
    49 
    50 end;