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 has_skip_proof: thm list -> bool |
11 val pretty_thm_oracles: Proof.context -> thm list -> Pretty.T |
12 val pretty_thm_oracles: Proof.context -> thm list -> Pretty.T |
12 val thm_deps: theory -> thm list -> unit |
13 val thm_deps: theory -> thm list -> unit |
13 val unused_thms: theory list * theory list -> (string * thm) list |
14 val unused_thms: theory list * theory list -> (string * thm) list |
14 end; |
15 end; |
15 |
16 |
18 |
19 |
19 (* oracles *) |
20 (* oracles *) |
20 |
21 |
21 fun all_oracles thms = |
22 fun all_oracles thms = |
22 Proofterm.all_oracles_of (map Thm.proof_body_of thms); |
23 Proofterm.all_oracles_of (map Thm.proof_body_of thms); |
|
24 |
|
25 fun has_skip_proof thms = |
|
26 all_oracles thms |> exists (fn (name, _) => name = \<^oracle_name>\<open>skip_proof\<close>); |
23 |
27 |
24 fun pretty_thm_oracles ctxt thms = |
28 fun pretty_thm_oracles ctxt thms = |
25 let |
29 let |
26 fun prt_oracle (name, NONE) = [Thm.pretty_oracle ctxt name] |
30 fun prt_oracle (name, NONE) = [Thm.pretty_oracle ctxt name] |
27 | prt_oracle (name, SOME prop) = |
31 | prt_oracle (name, SOME prop) = |