author | nipkow |
Tue, 20 Sep 2011 05:48:23 +0200 | |
changeset 45015 | fdac1e9880eb |
parent 39557 | fe5722fce758 |
child 45294 | 3c5d3d286055 |
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 |
||
31901 | 18 |
functor Named_Thms(val name: string 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 = |
|
30528 | 41 |
Attrib.setup (Binding.name name) (Attrib.add_del add del) ("declaration of " ^ description) #> |
39557
fe5722fce758
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
wenzelm
parents:
36296
diff
changeset
|
42 |
Global_Theory.add_thms_dynamic (Binding.name name, content); |
24047 | 43 |
|
44 |
end; |