src/Pure/Tools/named_thms.ML
author wenzelm
Sun Nov 11 20:31:46 2012 +0100 (2012-11-11)
changeset 50081 9b92ee8dec98
parent 45294 3c5d3d286055
permissions -rw-r--r--
tuned;
wenzelm@24047
     1
(*  Title:      Pure/Tools/named_thms.ML
wenzelm@24047
     2
    Author:     Makarius
wenzelm@24047
     3
wenzelm@33453
     4
Named collections of theorems in canonical order.
wenzelm@24047
     5
*)
wenzelm@24047
     6
wenzelm@24047
     7
signature NAMED_THMS =
wenzelm@24047
     8
sig
wenzelm@36296
     9
  val member: Proof.context -> thm -> bool
wenzelm@24047
    10
  val get: Proof.context -> thm list
wenzelm@26363
    11
  val add_thm: thm -> Context.generic -> Context.generic
wenzelm@26363
    12
  val del_thm: thm -> Context.generic -> Context.generic
wenzelm@24047
    13
  val add: attribute
wenzelm@24047
    14
  val del: attribute
wenzelm@24047
    15
  val setup: theory -> theory
wenzelm@24047
    16
end;
wenzelm@24047
    17
wenzelm@45294
    18
functor Named_Thms(val name: binding val description: string): NAMED_THMS =
wenzelm@24047
    19
struct
wenzelm@24047
    20
wenzelm@33519
    21
structure Data = Generic_Data
wenzelm@24047
    22
(
wenzelm@33453
    23
  type T = thm Item_Net.T;
wenzelm@33453
    24
  val empty = Thm.full_rules;
wenzelm@24047
    25
  val extend = I;
wenzelm@33519
    26
  val merge = Item_Net.merge;
wenzelm@24047
    27
);
wenzelm@24047
    28
wenzelm@36296
    29
val member = Item_Net.member o Data.get o Context.Proof;
wenzelm@36296
    30
wenzelm@33453
    31
val content = Item_Net.content o Data.get;
wenzelm@33453
    32
val get = content o Context.Proof;
wenzelm@24047
    33
wenzelm@33453
    34
val add_thm = Data.map o Item_Net.update;
wenzelm@33453
    35
val del_thm = Data.map o Item_Net.remove;
wenzelm@26363
    36
wenzelm@26363
    37
val add = Thm.declaration_attribute add_thm;
wenzelm@26363
    38
val del = Thm.declaration_attribute del_thm;
wenzelm@24047
    39
wenzelm@24047
    40
val setup =
wenzelm@45294
    41
  Attrib.setup name (Attrib.add_del add del) ("declaration of " ^ description) #>
wenzelm@45294
    42
  Global_Theory.add_thms_dynamic (name, content);
wenzelm@24047
    43
wenzelm@24047
    44
end;