equal
deleted
inserted
replaced
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 has_skip_proof: thm list -> bool |
12 val pretty_thm_oracles: Proof.context -> thm list -> Pretty.T |
12 val pretty_thm_oracles: Proof.context -> thm list -> Pretty.T |
13 val thm_deps: theory -> thm list -> (Proofterm.thm_id * Thm_Name.T) list |
13 val thm_deps: theory -> thm list -> (Proofterm.thm_id * Thm_Name.T) list |
14 val pretty_thm_deps: theory -> thm list -> Pretty.T |
14 val pretty_thm_deps: theory -> thm list -> Pretty.T |
|
15 val proof_boxes: (Proofterm.thm_id -> bool) -> thm -> Proofterm.thm_id list |
15 val unused_thms_cmd: theory list * theory list -> (string * thm) list |
16 val unused_thms_cmd: theory list * theory list -> (string * thm) list |
16 end; |
17 end; |
17 |
18 |
18 structure Thm_Deps: THM_DEPS = |
19 structure Thm_Deps: THM_DEPS = |
19 struct |
20 struct |
77 |> map (fn ((marks, xname), i) => |
78 |> map (fn ((marks, xname), i) => |
78 Pretty.item [Pretty.marks_str (marks, Thm_Name.print (xname, i))]); |
79 Pretty.item [Pretty.marks_str (marks, Thm_Name.print (xname, i))]); |
79 in Pretty.big_list ("dependencies: " ^ string_of_int (length items)) items end; |
80 in Pretty.big_list ("dependencies: " ^ string_of_int (length items)) items end; |
80 |
81 |
81 |
82 |
|
83 (* proof boxes: undefined PThm nodes *) |
|
84 |
|
85 fun proof_boxes defined thm = |
|
86 let |
|
87 fun boxes (i, thm_node) res = |
|
88 let val thm_id = Proofterm.thm_id (i, thm_node) in |
|
89 if defined thm_id orelse Inttab.defined res i then res |
|
90 else |
|
91 Inttab.update (i, thm_id) res |
|
92 |> fold boxes (Proofterm.thm_node_thms thm_node) |
|
93 end; |
|
94 in Inttab.fold_rev (cons o #2) (fold boxes (Thm.thm_deps thm) Inttab.empty) [] end; |
|
95 |
|
96 |
82 (* unused_thms_cmd *) |
97 (* unused_thms_cmd *) |
83 |
98 |
84 fun unused_thms_cmd (base_thys, thys) = |
99 fun unused_thms_cmd (base_thys, thys) = |
85 let |
100 let |
86 fun add_fact transfer space (name, ths) = |
101 fun add_fact transfer space (name, ths) = |