src/Pure/Tools/thm_deps.ML
2017-06-08 wenzelm 2017-06-08 more official session qualifier;
2016-12-16 wenzelm 2016-12-16 tuned signature -- more abstract type thm_node;
2016-12-15 wenzelm 2016-12-15 tuned signature;
2016-04-04 wenzelm 2016-04-04 clarified bootstrap -- more uniform use of ML files;
2015-10-23 wenzelm 2015-10-23 proper transfer of stored facts;
2015-10-06 wenzelm 2015-10-06 just one theorem kind, which is legacy anyway;
2015-04-16 wenzelm 2015-04-16 proper Theory.check;
2015-04-16 wenzelm 2015-04-16 discontinued pointless warnings: commands are only defined inside a theory context;
2015-04-16 wenzelm 2015-04-16 let the system choose Graph_Display.display_graph_old: thm_deps needs tree hierarchy, code_deps needs cycles (!?);
2015-04-15 wenzelm 2015-04-15 ensure that deps are defined in entries, to prevent crash of Graph_View.build_graph;
2015-04-06 wenzelm 2015-04-06 @{command_spec} is superseded by @{command_keyword};
2014-12-31 wenzelm 2014-12-31 clarified Graph_Display.graph etc.: sort_graph determines order from structure (and names); tuned;
2014-12-31 wenzelm 2014-12-31 for graph display, prefer graph data structure over list with dependencies; pragmatic distinction between (historically evolved) "session" nodes and (more abstract) "content" nodes
2014-12-31 wenzelm 2014-12-31 more explict and generic field names
2014-11-26 wenzelm 2014-11-26 renamed "pairself" to "apply2", in accordance to @{apply 2};
2014-11-03 wenzelm 2014-11-03 eliminated unused int_only flag (see also c12484a27367); just proper commands;
2014-08-21 wenzelm 2014-08-21 tuned signature -- define some elementary operations earlier;
2014-08-14 wenzelm 2014-08-14 tuned signature -- prefer self-contained user-space tool;