src/Tools/Compute_Oracle/linker.ML
2009-07-17 wenzelm 2009-07-17 tuned/modernized Envir.subst_XXX;
2009-07-09 wenzelm 2009-07-09 renamed functor TableFun to Table, and GraphFun to Graph;
2008-12-31 wenzelm 2008-12-31 moved old add_type_XXX, add_term_XXX etc. to structure OldTerm; use regular Term.add_XXX etc.;
2008-12-31 wenzelm 2008-12-31 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML); tuned signature of structure Term;
2008-03-20 wenzelm 2008-03-20 simplified get_thm(s): back to plain name argument;
2008-03-19 wenzelm 2008-03-19 renamed datatype thmref to Facts.ref, tuned interfaces;
2007-12-03 obua 2007-12-03 improvements
2007-10-27 obua 2007-10-27 better compute oracle
2007-09-15 haftmann 2007-09-15 fixed title
2007-08-14 wenzelm 2007-08-14 avoid low-level tsig;
2007-08-03 wenzelm 2007-08-03 replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
2007-07-11 obua 2007-07-11 fixed for SML/NJ
2007-07-09 obua 2007-07-09 new version of computing oracle