src/Tools/misc_legacy.ML
Tue, 06 Dec 2016 17:23:54 +0100 wenzelm avoid spurious messages -- potential cause of problems for "meson";
Tue, 22 Dec 2015 15:39:01 +0100 haftmann stripped some legacy
Sun, 05 Jul 2015 15:02:30 +0200 wenzelm simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
Tue, 02 Jun 2015 09:16:19 +0200 wenzelm clarified context;
Fri, 06 Mar 2015 15:58:56 +0100 wenzelm Thm.cterm_of and Thm.ctyp_of operate on local context;
Wed, 04 Mar 2015 19:53:18 +0100 wenzelm tuned signature -- prefer qualified names;
Sun, 21 Dec 2014 15:03:45 +0100 wenzelm proper context;
Sat, 08 Nov 2014 21:31:51 +0100 wenzelm optional proof context for unify operations, for the sake of proper local options;
Fri, 21 Mar 2014 20:33:56 +0100 wenzelm more qualified names;
Fri, 14 Mar 2014 16:54:01 +0100 wenzelm prefer more robust Synchronized.var;
Wed, 29 May 2013 18:25:11 +0200 wenzelm tuned signature -- more explicit flags for low-level Thm.bicompose;
Thu, 14 Mar 2013 14:25:55 +0100 wenzelm tuned signature;
Thu, 19 Apr 2012 10:16:51 +0200 haftmann dropped dead code;
Mon, 19 Mar 2012 21:10:33 +0100 wenzelm moved some legacy stuff;
Tue, 13 Mar 2012 20:04:24 +0100 wenzelm more explicit indication of def names;
less more (0) -15 tip