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