equal
deleted
inserted
replaced
6 *) |
6 *) |
7 |
7 |
8 signature NAMED_THMS = |
8 signature NAMED_THMS = |
9 sig |
9 sig |
10 val get: Proof.context -> thm list |
10 val get: Proof.context -> thm list |
11 val pretty: Proof.context -> Pretty.T |
|
12 val add_thm: thm -> Context.generic -> Context.generic |
11 val add_thm: thm -> Context.generic -> Context.generic |
13 val del_thm: thm -> Context.generic -> Context.generic |
12 val del_thm: thm -> Context.generic -> Context.generic |
14 val add: attribute |
13 val add: attribute |
15 val del: attribute |
14 val del: attribute |
16 val setup: theory -> theory |
15 val setup: theory -> theory |
27 fun merge _ = Thm.merge_thms; |
26 fun merge _ = Thm.merge_thms; |
28 ); |
27 ); |
29 |
28 |
30 val get = Data.get o Context.Proof; |
29 val get = Data.get o Context.Proof; |
31 |
30 |
32 fun pretty ctxt = |
|
33 Pretty.big_list (description ^ ":") (map (ProofContext.pretty_thm ctxt) (get ctxt)); |
|
34 |
|
35 val add_thm = Data.map o Thm.add_thm; |
31 val add_thm = Data.map o Thm.add_thm; |
36 val del_thm = Data.map o Thm.del_thm; |
32 val del_thm = Data.map o Thm.del_thm; |
37 |
33 |
38 val add = Thm.declaration_attribute add_thm; |
34 val add = Thm.declaration_attribute add_thm; |
39 val del = Thm.declaration_attribute del_thm; |
35 val del = Thm.declaration_attribute del_thm; |
40 |
36 |
41 val setup = |
37 val setup = |
42 Attrib.add_attributes [(name, Attrib.add_del_args add del, "declaration of " ^ description)] #> |
38 Attrib.add_attributes [(name, Attrib.add_del_args add del, "declaration of " ^ description)] #> |
43 PureThy.add_thms_dynamic (name, Data.get); |
39 PureThy.add_thms_dynamic (name, Data.get); |
44 |
40 |
45 val _ = |
|
46 OuterSyntax.improper_command ("print_" ^ name ^ "_rules") ("print " ^ description) |
|
47 OuterKeyword.diag |
|
48 (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o |
|
49 Toplevel.keep (Pretty.writeln o pretty o Toplevel.context_of))); |
|
50 |
|
51 end; |
41 end; |