equal
deleted
inserted
replaced
64 |
64 |
65 fun thm_deps thms = |
65 fun thm_deps thms = |
66 let |
66 let |
67 val _ = writeln "Generating graph ..."; |
67 val _ = writeln "Generating graph ..."; |
68 val gra = map snd (Symtab.dest (fst (foldl make_deps_graph ((Symtab.empty, []), |
68 val gra = map snd (Symtab.dest (fst (foldl make_deps_graph ((Symtab.empty, []), |
69 map (#der o Thm.rep_thm) thms)))); |
69 map (#2 o #der o Thm.rep_thm) thms)))); |
70 val path = File.tmp_path (Path.unpack "theorems.graph"); |
70 val path = File.tmp_path (Path.unpack "theorems.graph"); |
71 val _ = Present.write_graph gra path; |
71 val _ = Present.write_graph gra path; |
72 val _ = system ("$ISATOOL browser -d " ^ Path.pack (Path.expand path) ^ " &"); |
72 val _ = system ("$ISATOOL browser -d " ^ Path.pack (Path.expand path) ^ " &"); |
73 in () end; |
73 in () end; |
74 |
74 |