equal
deleted
inserted
replaced
36 {name = Long_Name.base_name name, |
36 {name = Long_Name.base_name name, |
37 ID = name, |
37 ID = name, |
38 dir = space_implode "/" (session @ prefix), |
38 dir = space_implode "/" (session @ prefix), |
39 unfold = false, |
39 unfold = false, |
40 path = "", |
40 path = "", |
41 parents = parents}; |
41 parents = parents, |
|
42 content = []}; |
42 in cons entry end; |
43 in cons entry end; |
43 val deps = Proofterm.fold_body_thms add_dep (Thm.proof_bodies_of thms) []; |
44 val deps = Proofterm.fold_body_thms add_dep (Thm.proof_bodies_of thms) []; |
44 in Present.display_graph (sort_wrt #ID deps) end; |
45 in Graph_Display.display_graph (sort_wrt #ID deps) end; |
45 |
46 |
46 |
47 |
47 (* unused_thms *) |
48 (* unused_thms *) |
48 |
49 |
49 fun unused_thms (base_thys, thys) = |
50 fun unused_thms (base_thys, thys) = |