src/Tools/Compute_Oracle/linker.ML
Wed, 21 Jul 2010 15:13:36 +0200 wenzelm explicit dependency on theory HOL;
Tue, 20 Jul 2010 23:09:49 +0200 wenzelm discontinued pervasive val theory = Thy_Info.get_theory -- prefer antiquotations in most situations;
Sat, 27 Feb 2010 23:13:01 +0100 wenzelm modernized structure Term_Ord;
Sat, 17 Oct 2009 14:43:18 +0200 wenzelm eliminated hard tabulators, guessing at each author's individual tab-width;
Tue, 29 Sep 2009 16:24:36 +0200 wenzelm explicit indication of Unsynchronized.ref;
Fri, 17 Jul 2009 23:11:40 +0200 wenzelm tuned/modernized Envir.subst_XXX;
Thu, 09 Jul 2009 22:01:41 +0200 wenzelm renamed functor TableFun to Table, and GraphFun to Graph;
Wed, 31 Dec 2008 18:53:19 +0100 wenzelm moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
Wed, 31 Dec 2008 15:30:10 +0100 wenzelm moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
Thu, 20 Mar 2008 00:20:44 +0100 wenzelm simplified get_thm(s): back to plain name argument;
Wed, 19 Mar 2008 22:27:57 +0100 wenzelm renamed datatype thmref to Facts.ref, tuned interfaces;
Mon, 03 Dec 2007 17:47:35 +0100 obua improvements
Sat, 27 Oct 2007 18:37:33 +0200 obua better compute oracle
Sat, 15 Sep 2007 19:27:35 +0200 haftmann fixed title
Tue, 14 Aug 2007 23:22:51 +0200 wenzelm avoid low-level tsig;
Fri, 03 Aug 2007 16:28:15 +0200 wenzelm replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
Wed, 11 Jul 2007 11:47:13 +0200 obua fixed for SML/NJ
Mon, 09 Jul 2007 17:36:25 +0200 obua new version of computing oracle
less more (0) tip