src/Pure/Thy/thm_deps.ML
changeset 7783 9ace4017ead8
parent 7765 fa28bac7903c
child 7785 c06825c396e8
equal deleted inserted replaced
7782:d4a6464ed61e 7783:9ace4017ead8
    62     val _ = writeln "Generating graph ...";
    62     val _ = writeln "Generating graph ...";
    63     val gra = map snd (Symtab.dest (fst (foldl make_deps_graph ((Symtab.empty, []),
    63     val gra = map snd (Symtab.dest (fst (foldl make_deps_graph ((Symtab.empty, []),
    64       map (#der o rep_thm) thms))));
    64       map (#der o rep_thm) thms))));
    65     val path = File.tmp_path (Path.unpack "theorems.graph");
    65     val path = File.tmp_path (Path.unpack "theorems.graph");
    66     val _ = put_graph gra path;
    66     val _ = put_graph gra path;
    67     val _ = execute ("isatool browser -d " ^ Path.pack (Path.expand path) ^ " &");
    67     val _ = execute ("$ISATOOL browser -d " ^ Path.pack (Path.expand path) ^ " &");
    68   in () end;
    68   in () end;
    69 
    69 
    70 end;
    70 end;
    71 
    71 
    72 open ThmDeps;
    72 open ThmDeps;