src/Tools/Compute_Oracle/compute.ML
2010-05-15 wenzelm 2010-05-15 less pervasive names from structure Thm;
2009-09-29 wenzelm 2009-09-29 explicit indication of Unsynchronized.ref;
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;
2009-05-31 wenzelm 2009-05-31 attempt to eliminate adhoc makestring at runtime (which is not well-defined);
2009-03-05 wenzelm 2009-03-05 Thm.add_oracle interface: replaced old bstring by binding;
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-09-18 wenzelm 2008-09-18 simplified oracle interface;
2008-04-15 wenzelm 2008-04-15 Theory.subthy;
2008-04-12 wenzelm 2008-04-12 rep_cterm/rep_thm: no longer dereference theory_ref;
2007-12-03 obua 2007-12-03 improvements
2007-10-27 obua 2007-10-27 better compute oracle
2007-10-27 obua 2007-10-27 better compute oracle
2007-09-20 obua 2007-09-20 improved computing
2007-09-15 haftmann 2007-09-15 fixed title
2007-08-03 wenzelm 2007-08-03 replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
2007-07-09 obua 2007-07-09 new version of computing oracle
2007-05-31 wenzelm 2007-05-31 moved Compute_Oracle from Pure/Tools to Tools;