equal
deleted
inserted
replaced
6 *) |
6 *) |
7 |
7 |
8 signature THM_DEPS = |
8 signature THM_DEPS = |
9 sig |
9 sig |
10 val all_oracles: thm list -> Proofterm.oracle list |
10 val all_oracles: thm list -> Proofterm.oracle list |
|
11 val pretty_thm_oracles: Proof.context -> thm list -> Pretty.T |
11 val thm_deps: theory -> thm list -> unit |
12 val thm_deps: theory -> thm list -> unit |
12 val unused_thms: theory list * theory list -> (string * thm) list |
13 val unused_thms: theory list * theory list -> (string * thm) list |
13 end; |
14 end; |
14 |
15 |
15 structure Thm_Deps: THM_DEPS = |
16 structure Thm_Deps: THM_DEPS = |
17 |
18 |
18 (* oracles *) |
19 (* oracles *) |
19 |
20 |
20 fun all_oracles thms = |
21 fun all_oracles thms = |
21 Proofterm.all_oracles_of (map Thm.proof_body_of thms); |
22 Proofterm.all_oracles_of (map Thm.proof_body_of thms); |
|
23 |
|
24 fun pretty_thm_oracles ctxt thms = |
|
25 let |
|
26 fun prt_oracle (name, NONE) = [Thm.pretty_oracle ctxt name] |
|
27 | prt_oracle (name, SOME prop) = |
|
28 [Thm.pretty_oracle ctxt name, Pretty.str ":", Pretty.brk 1, Syntax.pretty_term ctxt prop]; |
|
29 in Pretty.big_list "oracles:" (map (Pretty.item o prt_oracle) (all_oracles thms)) end; |
22 |
30 |
23 |
31 |
24 (* thm_deps *) |
32 (* thm_deps *) |
25 |
33 |
26 fun thm_deps thy thms = |
34 fun thm_deps thy thms = |