src/Pure/Tools/named_thms.ML
author wenzelm
Sat Mar 20 17:33:11 2010 +0100 (2010-03-20)
changeset 35845 e5980f0ad025
parent 33519 e31a85f92ce9
child 36296 5cc547abd995
permissions -rw-r--r--
renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
     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 get: Proof.context -> thm list
    10   val add_thm: thm -> Context.generic -> Context.generic
    11   val del_thm: thm -> Context.generic -> Context.generic
    12   val add: attribute
    13   val del: attribute
    14   val setup: theory -> theory
    15 end;
    16 
    17 functor Named_Thms(val name: string val description: string): NAMED_THMS =
    18 struct
    19 
    20 structure Data = Generic_Data
    21 (
    22   type T = thm Item_Net.T;
    23   val empty = Thm.full_rules;
    24   val extend = I;
    25   val merge = Item_Net.merge;
    26 );
    27 
    28 val content = Item_Net.content o Data.get;
    29 val get = content o Context.Proof;
    30 
    31 val add_thm = Data.map o Item_Net.update;
    32 val del_thm = Data.map o Item_Net.remove;
    33 
    34 val add = Thm.declaration_attribute add_thm;
    35 val del = Thm.declaration_attribute del_thm;
    36 
    37 val setup =
    38   Attrib.setup (Binding.name name) (Attrib.add_del add del) ("declaration of " ^ description) #>
    39   PureThy.add_thms_dynamic (Binding.name name, content);
    40 
    41 end;