src/HOL/Refute.thy
Tue, 26 Oct 2010 12:17:19 +0200 blanchet reverted e7a80c6752c9 -- there's not much point in putting a diagnosis tool (as opposed to a proof method) in Plain, but more importantly Sledgehammer must be in Main to use SMT solvers
Mon, 25 Oct 2010 13:34:57 +0200 haftmann moved sledgehammer to Plain; tuned dependencies
Mon, 04 Oct 2010 22:45:09 +0200 blanchet move Metis into Plain
Thu, 02 Sep 2010 17:12:16 +0200 wenzelm just one refute.ML;
Mon, 14 Dec 2009 12:14:12 +0100 blanchet added "no_assms" option to Refute, and include structured proof assumptions by default;
Mon, 07 Dec 2009 11:46:13 +0100 blanchet avoid using "prop_logic.ML" and "sat_solver.ML" twice (the other occurrence being in "FunDef.thy");
Tue, 10 Nov 2009 16:11:37 +0100 haftmann tuned imports
Fri, 02 Oct 2009 21:41:57 +0200 wenzelm Refute.refute_goal: canonical goal addresses from 1 (renamed from refute_subgoal to clarify change in semantics);
Fri, 06 Feb 2009 13:43:19 +0100 blanchet Rearrange Refute/SAT theory dependencies so as to use even more antiquotations in refute.ML +
Wed, 02 Apr 2008 15:58:57 +0200 haftmann tuned imports
Thu, 11 Jan 2007 01:34:23 +0100 webertj updated to mention the automatic unfolding of constants
Mon, 13 Nov 2006 15:43:09 +0100 haftmann moved upwars in HOL theory graph
Thu, 29 Sep 2005 15:50:44 +0200 wenzelm explicit dependencies of SAT vs. Refute;
Mon, 18 Jul 2005 15:49:34 +0200 webertj Documentation updated
Fri, 17 Jun 2005 16:12:49 +0200 haftmann migrated theory headers to new format
Wed, 17 Nov 2004 19:25:34 +0100 webertj removed explicit mentioning of zChaffs version number
Wed, 18 Aug 2004 11:09:40 +0200 nipkow import -> imports
Mon, 16 Aug 2004 14:22:27 +0200 nipkow New theory header syntax.
Wed, 26 May 2004 18:06:38 +0200 webertj documentation updated
Fri, 21 May 2004 21:17:37 +0200 wenzelm load ML files only once;
Fri, 16 Apr 2004 13:51:04 +0200 wenzelm tuned document;
Thu, 11 Mar 2004 13:03:31 +0100 webertj Documentation updated
Wed, 10 Mar 2004 22:35:37 +0100 webertj *** empty log message ***
Sat, 10 Jan 2004 13:35:10 +0100 webertj Adding 'refute' to HOL.
less more (0) tip