24047
|
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
|
26363
|
10 |
val add_thm: thm -> Context.generic -> Context.generic
|
|
11 |
val del_thm: thm -> Context.generic -> Context.generic
|
24047
|
12 |
val add: attribute
|
|
13 |
val del: attribute
|
|
14 |
val setup: theory -> theory
|
|
15 |
end;
|
|
16 |
|
|
17 |
functor NamedThmsFun(val name: string val description: string): NAMED_THMS =
|
|
18 |
struct
|
|
19 |
|
|
20 |
structure Data = GenericDataFun
|
|
21 |
(
|
|
22 |
type T = thm list;
|
|
23 |
val empty = [];
|
|
24 |
val extend = I;
|
|
25 |
fun merge _ = Thm.merge_thms;
|
|
26 |
);
|
|
27 |
|
|
28 |
val get = Data.get o Context.Proof;
|
|
29 |
|
26363
|
30 |
val add_thm = Data.map o Thm.add_thm;
|
|
31 |
val del_thm = Data.map o Thm.del_thm;
|
|
32 |
|
|
33 |
val add = Thm.declaration_attribute add_thm;
|
|
34 |
val del = Thm.declaration_attribute del_thm;
|
24047
|
35 |
|
|
36 |
val setup =
|
26397
|
37 |
Attrib.add_attributes [(name, Attrib.add_del_args add del, "declaration of " ^ description)] #>
|
29579
|
38 |
PureThy.add_thms_dynamic (Binding.name name, Data.get);
|
24047
|
39 |
|
|
40 |
end;
|