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;
Sat, 14 Jan 2012 17:45:04 +0100 wenzelm discontinued old-style Term.list_all_free in favour of plain Logic.all;
Wed, 14 Dec 2011 12:18:19 +0100 wenzelm eliminated dead code;
Wed, 19 Oct 2011 15:41:12 +0200 wenzelm tuned legacy signature;
Wed, 10 Aug 2011 20:53:43 +0200 wenzelm old term operations are legacy;
Sat, 16 Apr 2011 16:15:37 +0200 wenzelm modernized structure Proof_Context;
Fri, 08 Apr 2011 13:31:16 +0200 wenzelm explicit structure Syntax_Trans;
Sun, 12 Sep 2010 19:04:02 +0200 wenzelm eliminated aliases of Type.constraint;
Mon, 12 Jul 2010 21:38:37 +0200 wenzelm moved misc legacy stuff from OldGoals to Misc_Legacy;
less more (0) tip