24047
|
1 |
(* Title: Pure/Tools/named_thms.ML
|
|
2 |
ID: $Id$
|
|
3 |
Author: Makarius
|
|
4 |
|
|
5 |
Named collections of theorems in canonical order.
|
|
6 |
*)
|
|
7 |
|
|
8 |
signature NAMED_THMS =
|
|
9 |
sig
|
|
10 |
val get: Proof.context -> thm list
|
|
11 |
val pretty: Proof.context -> Pretty.T
|
|
12 |
val print: Proof.context -> unit
|
|
13 |
val add: attribute
|
|
14 |
val del: attribute
|
|
15 |
val setup: theory -> theory
|
|
16 |
end;
|
|
17 |
|
|
18 |
functor NamedThmsFun(val name: string val description: string): NAMED_THMS =
|
|
19 |
struct
|
|
20 |
|
|
21 |
structure Data = GenericDataFun
|
|
22 |
(
|
|
23 |
type T = thm list;
|
|
24 |
val empty = [];
|
|
25 |
val extend = I;
|
|
26 |
fun merge _ = Thm.merge_thms;
|
|
27 |
);
|
|
28 |
|
|
29 |
val get = Data.get o Context.Proof;
|
|
30 |
|
|
31 |
fun pretty ctxt =
|
|
32 |
Pretty.big_list (description ^ ":") (map (ProofContext.pretty_thm ctxt) (get ctxt));
|
|
33 |
|
|
34 |
val print = Pretty.writeln o pretty;
|
|
35 |
|
|
36 |
val add = Thm.declaration_attribute (Data.map o Thm.add_thm);
|
|
37 |
val del = Thm.declaration_attribute (Data.map o Thm.del_thm);
|
|
38 |
|
|
39 |
val setup =
|
|
40 |
Attrib.add_attributes [(name, Attrib.add_del_args add del, "declaration of " ^ description)];
|
|
41 |
|
|
42 |
end;
|