src/Provers/quasi.ML
Wed, 04 Mar 2015 20:47:29 +0100 wenzelm tuned;
Tue, 10 Feb 2015 14:48:26 +0100 wenzelm proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
Thu, 30 Oct 2014 22:45:19 +0100 wenzelm eliminated aliases;
Wed, 08 Jun 2011 15:56:57 +0200 wenzelm more robust exception pattern General.Subscript;
Sat, 16 Apr 2011 18:11:20 +0200 wenzelm eliminated old List.nth;
Sat, 16 Apr 2011 16:15:37 +0200 wenzelm modernized structure Proof_Context;
Mon, 06 Sep 2010 19:13:10 +0200 wenzelm more antiquotations;
Thu, 08 Jul 2010 16:19:24 +0200 haftmann tuned titles
Thu, 22 Oct 2009 13:48:06 +0200 haftmann map_range (and map_index) combinator
Thu, 15 Oct 2009 23:28:10 +0200 wenzelm replaced String.concat by implode;
Tue, 29 Sep 2009 16:24:36 +0200 wenzelm explicit indication of Unsynchronized.ref;
Thu, 30 Jul 2009 18:43:52 +0200 wenzelm trancl_tac etc.: back to static context -- problem was caused by bad solver in AFP/JiveDataStoreModel;
Thu, 30 Jul 2009 12:20:43 +0200 wenzelm qualified Subgoal.FOCUS;
Wed, 29 Jul 2009 22:34:31 +0200 wenzelm trans_tac: use theory from goal state, not the static context, which seems to be outdated under certain circumstances (why?);
Sun, 26 Jul 2009 22:28:31 +0200 wenzelm replaced old METAHYPS by FOCUS;
Wed, 31 Dec 2008 19:54:03 +0100 wenzelm qualified Term.rename_wrt_term;
Wed, 04 Apr 2007 00:11:03 +0200 wenzelm removed obsolete sign_of/sign_of_thm;
Sat, 11 Mar 2006 21:23:10 +0100 wenzelm got rid of type Sign.sg;
Thu, 03 Mar 2005 12:43:01 +0100 skalberg Move towards standard functions.
Sun, 13 Feb 2005 17:15:14 +0100 skalberg Deleted Library.option type.
Tue, 03 Aug 2004 14:47:51 +0200 ballarin New transitivity reasoners for transitivity only and quasi orders.
less more (0) tip