equal
deleted
inserted
replaced
5 Dependencies of theorems wrt. internal derivation. |
5 Dependencies of theorems wrt. internal derivation. |
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 thm_deps: theory -> thm list -> unit |
11 val thm_deps: theory -> thm list -> unit |
11 val unused_thms: theory list * theory list -> (string * thm) list |
12 val unused_thms: theory list * theory list -> (string * thm) list |
12 end; |
13 end; |
13 |
14 |
14 structure Thm_Deps: THM_DEPS = |
15 structure Thm_Deps: THM_DEPS = |
15 struct |
16 struct |
|
17 |
|
18 (* oracles *) |
|
19 |
|
20 fun all_oracles thms = |
|
21 Proofterm.all_oracles_of (map Thm.proof_body_of thms); |
|
22 |
16 |
23 |
17 (* thm_deps *) |
24 (* thm_deps *) |
18 |
25 |
19 fun thm_deps thy thms = |
26 fun thm_deps thy thms = |
20 let |
27 let |