src/HOL/Refute.thy
2012-03-16 wenzelm 2012-03-16 refute_params are given in *this* theory;
2012-03-15 wenzelm 2012-03-15 declare command keywords via theory header, including strict checking outside Pure;
2010-10-26 blanchet 2010-10-26 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
2010-10-25 haftmann 2010-10-25 moved sledgehammer to Plain; tuned dependencies
2010-10-04 blanchet 2010-10-04 move Metis into Plain
2010-09-02 wenzelm 2010-09-02 just one refute.ML;
2009-12-14 blanchet 2009-12-14 added "no_assms" option to Refute, and include structured proof assumptions by default; will do the same for Quickcheck unless there are objections
2009-12-07 blanchet 2009-12-07 avoid using "prop_logic.ML" and "sat_solver.ML" twice (the other occurrence being in "FunDef.thy"); this produces two copies of the same module, with separate references etc.
2009-11-10 haftmann 2009-11-10 tuned imports
2009-10-02 wenzelm 2009-10-02 Refute.refute_goal: canonical goal addresses from 1 (renamed from refute_subgoal to clarify change in semantics); command 'refute': Proof.flat_goal provides standard view on internally structured Isar goal, suitable for (semi)automated tools;
2009-02-06 blanchet 2009-02-06 Rearrange Refute/SAT theory dependencies so as to use even more antiquotations in refute.ML + find/fix Product_Type.{fst,snd}, which are now called simply fst and snd.
2008-04-02 haftmann 2008-04-02 tuned imports
2007-01-11 webertj 2007-01-11 updated to mention the automatic unfolding of constants
2006-11-13 haftmann 2006-11-13 moved upwars in HOL theory graph
2005-09-29 wenzelm 2005-09-29 explicit dependencies of SAT vs. Refute; moved late refute setup to SAT;
2005-07-18 webertj 2005-07-18 Documentation updated
2005-06-17 haftmann 2005-06-17 migrated theory headers to new format
2004-11-17 webertj 2004-11-17 removed explicit mentioning of zChaffs version number
2004-08-18 nipkow 2004-08-18 import -> imports
2004-08-16 nipkow 2004-08-16 New theory header syntax.
2004-05-26 webertj 2004-05-26 documentation updated
2004-05-21 wenzelm 2004-05-21 load ML files only once;
2004-04-16 wenzelm 2004-04-16 tuned document;
2004-03-11 webertj 2004-03-11 Documentation updated
2004-03-10 webertj 2004-03-10 *** empty log message ***
2004-01-10 webertj 2004-01-10 Adding 'refute' to HOL.