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: {included: Proofterm.thm_id -> bool, excluded: Proofterm.thm_id -> bool} -> |
15 val thm_boxes: {included: Proofterm.thm_id -> bool, excluded: Proofterm.thm_id -> bool} -> |
16 thm list -> Proofterm.thm_id list |
16 thm list -> Proofterm.thm_id list |
17 val unused_thms_cmd: theory list * theory list -> (string * thm) list |
17 val unused_thms_cmd: theory list * theory list -> (string * thm) list |
18 end; |
18 end; |
19 |
19 |
20 structure Thm_Deps: THM_DEPS = |
20 structure Thm_Deps: THM_DEPS = |
79 |> map (fn ((marks, xname), i) => |
79 |> map (fn ((marks, xname), i) => |
80 Pretty.item [Pretty.marks_str (marks, Thm_Name.print (xname, i))]); |
80 Pretty.item [Pretty.marks_str (marks, Thm_Name.print (xname, i))]); |
81 in Pretty.big_list ("dependencies: " ^ string_of_int (length items)) items end; |
81 in Pretty.big_list ("dependencies: " ^ string_of_int (length items)) items end; |
82 |
82 |
83 |
83 |
84 (* proof boxes: undefined PThm nodes *) |
84 (* thm boxes: intermediate PThm nodes *) |
85 |
85 |
86 fun proof_boxes {included, excluded} thms = |
86 fun thm_boxes {included, excluded} thms = |
87 let |
87 let |
88 fun boxes (i, thm_node) res = |
88 fun boxes (i, thm_node) res = |
89 let val thm_id = Proofterm.thm_id (i, thm_node) in |
89 let val thm_id = Proofterm.thm_id (i, thm_node) in |
90 if Inttab.defined res i orelse (excluded thm_id andalso not (included thm_id)) |
90 if Inttab.defined res i orelse (excluded thm_id andalso not (included thm_id)) |
91 then res |
91 then res |