src/Provers/trancl.ML
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