src/Pure/Tools/named_thms.ML
author wenzelm
Tue Nov 07 16:50:26 2017 +0100 (20 months ago)
changeset 67026 687c822ee5e3
parent 45294 3c5d3d286055
permissions -rw-r--r--
tuned signature;
     1 (*  Title:      Pure/Tools/named_thms.ML
     2     Author:     Makarius
     3 
     4 Named collections of theorems in canonical order.
     5 *)
     6 
     7 signature NAMED_THMS =
     8 sig
     9   val member: Proof.context -> thm -> bool
    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 Named_Thms(val name: binding val description: string): NAMED_THMS =
    19 struct
    20 
    21 structure Data = Generic_Data
    22 (
    23   type T = thm Item_Net.T;
    24   val empty = Thm.full_rules;
    25   val extend = I;
    26   val merge = Item_Net.merge;
    27 );
    28 
    29 val member = Item_Net.member o Data.get o Context.Proof;
    30 
    31 val content = Item_Net.content o Data.get;
    32 val get = content o Context.Proof;
    33 
    34 val add_thm = Data.map o Item_Net.update;
    35 val del_thm = Data.map o Item_Net.remove;
    36 
    37 val add = Thm.declaration_attribute add_thm;
    38 val del = Thm.declaration_attribute del_thm;
    39 
    40 val setup =
    41   Attrib.setup name (Attrib.add_del add del) ("declaration of " ^ description) #>
    42   Global_Theory.add_thms_dynamic (name, content);
    43 
    44 end;