src/Provers/trancl.ML
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 =)
Mon, 22 Feb 2010 14:11:03 +0100 berghofe Fixed bug that caused (r)trancl_tac to crash when the term denoting the relation
Thu, 22 Oct 2009 13:48:06 +0200 haftmann map_range (and map_index) combinator
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 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;
Sun, 01 Mar 2009 23:36:12 +0100 wenzelm use long names for old-style fold combinators;
Wed, 07 May 2008 10:59:49 +0200 berghofe Terms returned by decomp are now eta-contracted.
Wed, 07 Feb 2007 12:08:48 +0100 berghofe "prove" function now instantiates relation variable in order
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.
Mon, 02 Aug 2004 10:16:40 +0200 ballarin Documentation added/improved.
Tue, 27 Jul 2004 15:39:59 +0200 ballarin *** empty log message ***
Mon, 26 Jul 2004 15:48:50 +0200 ballarin New prover for transitive and reflexive-transitive closure of relations.
less more (0) tip