Named collections of theorems in canonical order.
authorwenzelm
Sun Jul 29 14:30:03 2007 +0200 (2007-07-29)
changeset 2404747b588ce11ec
parent 24046 10f681043e07
child 24048 a12b4faff474
Named collections of theorems in canonical order.
src/Pure/Tools/named_thms.ML
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/Tools/named_thms.ML	Sun Jul 29 14:30:03 2007 +0200
     1.3 @@ -0,0 +1,42 @@
     1.4 +(*  Title:      Pure/Tools/named_thms.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     Makarius
     1.7 +
     1.8 +Named collections of theorems in canonical order.
     1.9 +*)
    1.10 +
    1.11 +signature NAMED_THMS =
    1.12 +sig
    1.13 +  val get: Proof.context -> thm list
    1.14 +  val pretty: Proof.context -> Pretty.T
    1.15 +  val print: Proof.context -> unit
    1.16 +  val add: attribute
    1.17 +  val del: attribute
    1.18 +  val setup: theory -> theory
    1.19 +end;
    1.20 +
    1.21 +functor NamedThmsFun(val name: string val description: string): NAMED_THMS =
    1.22 +struct
    1.23 +
    1.24 +structure Data = GenericDataFun
    1.25 +(
    1.26 +  type T = thm list;
    1.27 +  val empty = [];
    1.28 +  val extend = I;
    1.29 +  fun merge _ = Thm.merge_thms;
    1.30 +);
    1.31 +
    1.32 +val get = Data.get o Context.Proof;
    1.33 +
    1.34 +fun pretty ctxt =
    1.35 +  Pretty.big_list (description ^ ":") (map (ProofContext.pretty_thm ctxt) (get ctxt));
    1.36 +
    1.37 +val print = Pretty.writeln o pretty;
    1.38 +
    1.39 +val add = Thm.declaration_attribute (Data.map o Thm.add_thm);
    1.40 +val del = Thm.declaration_attribute (Data.map o Thm.del_thm);
    1.41 +
    1.42 +val setup =
    1.43 +  Attrib.add_attributes [(name, Attrib.add_del_args add del, "declaration of " ^ description)];
    1.44 +
    1.45 +end;