src/Provers/order.ML
Wed, 04 Mar 2015 20:47:29 +0100 wenzelm tuned;
Wed, 04 Mar 2015 19:53:18 +0100 wenzelm tuned signature -- prefer qualified names;
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;
Thu, 08 Jul 2010 16:19:24 +0200 haftmann tuned titles
Wed, 05 May 2010 18:25:34 +0200 haftmann farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
Tue, 27 Oct 2009 22:56:14 +0100 wenzelm eliminated some old folds;
Mon, 26 Oct 2009 15:16:28 +0100 haftmann avoid upto if not needed
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 23:19:26 +0200 wenzelm tuned;
Tue, 29 Sep 2009 16:24:36 +0200 wenzelm explicit indication of Unsynchronized.ref;
Thu, 30 Jul 2009 12:20:43 +0200 wenzelm qualified Subgoal.FOCUS;
Sun, 26 Jul 2009 22:28:31 +0200 wenzelm replaced old METAHYPS by FOCUS;
Sun, 01 Mar 2009 23:36:12 +0100 wenzelm use long names for old-style fold combinators;
Wed, 31 Dec 2008 19:54:03 +0100 wenzelm qualified Term.rename_wrt_term;
Wed, 07 May 2008 10:59:49 +0200 berghofe Terms returned by decomp are now eta-contracted.
Tue, 25 Sep 2007 12:56:27 +0200 ballarin Transitivity reasoner gets additional argument of premises to improve integration with simplifier.
Tue, 18 Sep 2007 18:51:07 +0200 ballarin Defunctorised transitivity reasoner; locale interpretation requires dynamic instances.
Thu, 05 Jul 2007 00:06:14 +0200 wenzelm avoid polymorphic equality;
Wed, 04 Apr 2007 00:11:03 +0200 wenzelm removed obsolete sign_of/sign_of_thm;
Thu, 11 May 2006 19:19:31 +0200 wenzelm avoid raw equality on type thm;
Sat, 11 Mar 2006 21:23:10 +0100 wenzelm got rid of type Sign.sg;
Thu, 07 Jul 2005 19:01:04 +0200 obua 1) all theorems in Orderings can now be given as a parameter
Fri, 04 Mar 2005 15:07:34 +0100 skalberg Removed practically all references to Library.foldr.
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.
Mon, 02 Aug 2004 10:16:40 +0200 ballarin Documentation added/improved.
Mon, 08 Mar 2004 12:17:43 +0100 ballarin Bug-fixes for transitivity reasoner.
Thu, 19 Feb 2004 15:57:34 +0100 ballarin Efficient, graph-based reasoner for linear and partial orders.
less more (0) tip