src/Pure/term_ord.ML
2010-07-20 wenzelm eliminated old-style sys_error/SYS_ERROR in favour of exception Fail -- after careful checking that there is no overlap with existing handling of that;
2010-02-27 wenzelm modernized structure Term_Ord;
2010-02-27 wenzelm further standard instances of functor Graph;
2010-02-27 wenzelm just one copy of structure Term_Graph (in Pure);
2009-10-01 wenzelm added term_cache;
2009-07-09 wenzelm Sorttab in Pure;
2009-07-09 wenzelm renamed functor TableFun to Table, and GraphFun to Graph;
2008-12-31 wenzelm moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
less more (0) tip