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;
wenzelm@24047
     1
(*  Title:      Pure/Tools/named_thms.ML
wenzelm@24047
     2
    ID:         $Id$
wenzelm@24047
     3
    Author:     Makarius
wenzelm@24047
     4
wenzelm@24047
     5
Named collections of theorems in canonical order.
wenzelm@24047
     6
*)
wenzelm@24047
     7
wenzelm@24047
     8
signature NAMED_THMS =
wenzelm@24047
     9
sig
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@24047
    18
functor NamedThmsFun(val name: string val description: string): NAMED_THMS =
wenzelm@24047
    19
struct
wenzelm@24047
    20
wenzelm@24047
    21
structure Data = GenericDataFun
wenzelm@24047
    22
(
wenzelm@24047
    23
  type T = thm list;
wenzelm@24047
    24
  val empty = [];
wenzelm@24047
    25
  val extend = I;
wenzelm@24047
    26
  fun merge _ = Thm.merge_thms;
wenzelm@24047
    27
);
wenzelm@24047
    28
wenzelm@24047
    29
val get = Data.get o Context.Proof;
wenzelm@24047
    30
wenzelm@26363
    31
val add_thm = Data.map o Thm.add_thm;
wenzelm@26363
    32
val del_thm = Data.map o Thm.del_thm;
wenzelm@26363
    33
wenzelm@26363
    34
val add = Thm.declaration_attribute add_thm;
wenzelm@26363
    35
val del = Thm.declaration_attribute del_thm;
wenzelm@24047
    36
wenzelm@24047
    37
val setup =
wenzelm@26397
    38
  Attrib.add_attributes [(name, Attrib.add_del_args add del, "declaration of " ^ description)] #>
wenzelm@26397
    39
  PureThy.add_thms_dynamic (name, Data.get);
wenzelm@24047
    40
wenzelm@24047
    41
end;