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
|
26363
|
12 |
val add_thm: thm -> Context.generic -> Context.generic
|
|
13 |
val del_thm: thm -> Context.generic -> Context.generic
|
24047
|
14 |
val add: attribute
|
|
15 |
val del: attribute
|
|
16 |
val setup: theory -> theory
|
|
17 |
end;
|
|
18 |
|
|
19 |
functor NamedThmsFun(val name: string val description: string): NAMED_THMS =
|
|
20 |
struct
|
|
21 |
|
|
22 |
structure Data = GenericDataFun
|
|
23 |
(
|
|
24 |
type T = thm list;
|
|
25 |
val empty = [];
|
|
26 |
val extend = I;
|
|
27 |
fun merge _ = Thm.merge_thms;
|
|
28 |
);
|
|
29 |
|
|
30 |
val get = Data.get o Context.Proof;
|
|
31 |
|
|
32 |
fun pretty ctxt =
|
|
33 |
Pretty.big_list (description ^ ":") (map (ProofContext.pretty_thm ctxt) (get ctxt));
|
|
34 |
|
26363
|
35 |
val add_thm = Data.map o Thm.add_thm;
|
|
36 |
val del_thm = Data.map o Thm.del_thm;
|
|
37 |
|
|
38 |
val add = Thm.declaration_attribute add_thm;
|
|
39 |
val del = Thm.declaration_attribute del_thm;
|
24047
|
40 |
|
|
41 |
val setup =
|
26397
|
42 |
Attrib.add_attributes [(name, Attrib.add_del_args add del, "declaration of " ^ description)] #>
|
|
43 |
PureThy.add_thms_dynamic (name, Data.get);
|
24047
|
44 |
|
24867
|
45 |
val _ =
|
|
46 |
OuterSyntax.improper_command ("print_" ^ name ^ "_rules") ("print " ^ description)
|
24117
|
47 |
OuterKeyword.diag
|
|
48 |
(Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
|
24867
|
49 |
Toplevel.keep (Pretty.writeln o pretty o Toplevel.context_of)));
|
24117
|
50 |
|
24047
|
51 |
end;
|