src/Pure/Tools/named_thms.ML
author wenzelm
Sat Apr 19 12:04:17 2008 +0200 (2008-04-19)
changeset 26724 ff6ff3a9010e
parent 26397 df68e8dfd0e3
child 29579 cb520b766e00
permissions -rw-r--r--
NamedThmsFun: removed obsolete print command -- facts are accesible via dynamic name;
     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 add_thm: thm -> Context.generic -> Context.generic
    12   val del_thm: thm -> Context.generic -> Context.generic
    13   val add: attribute
    14   val del: attribute
    15   val setup: theory -> theory
    16 end;
    17 
    18 functor NamedThmsFun(val name: string val description: string): NAMED_THMS =
    19 struct
    20 
    21 structure Data = GenericDataFun
    22 (
    23   type T = thm list;
    24   val empty = [];
    25   val extend = I;
    26   fun merge _ = Thm.merge_thms;
    27 );
    28 
    29 val get = Data.get o Context.Proof;
    30 
    31 val add_thm = Data.map o Thm.add_thm;
    32 val del_thm = Data.map o Thm.del_thm;
    33 
    34 val add = Thm.declaration_attribute add_thm;
    35 val del = Thm.declaration_attribute del_thm;
    36 
    37 val setup =
    38   Attrib.add_attributes [(name, Attrib.add_del_args add del, "declaration of " ^ description)] #>
    39   PureThy.add_thms_dynamic (name, Data.get);
    40 
    41 end;