2011-07-13 wenzelm 2011-07-13 sub-structural sharing after Syntax.check phase, with global interning of logical entities (the latter is relevant when bypassing default parsing via YXML); minor tuning;
2010-07-20 wenzelm 2010-07-20 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; tuned some error messages;
2010-02-27 wenzelm 2010-02-27 modernized structure Term_Ord;
2010-02-27 wenzelm 2010-02-27 further standard instances of functor Graph;
2010-02-27 wenzelm 2010-02-27 just one copy of structure Term_Graph (in Pure);
2009-10-01 wenzelm 2009-10-01 added term_cache; tuned;
2009-07-09 wenzelm 2009-07-09 Sorttab in Pure;
2009-07-09 wenzelm 2009-07-09 renamed functor TableFun to Table, and GraphFun to Graph;
2008-12-31 wenzelm 2008-12-31 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML); tuned signature of structure Term;