src/HOL/ex/Refute_Examples.thy
2012-10-31 blanchet 2012-10-31 fixes related to Refute's move
2012-10-12 wenzelm 2012-10-12 discontinued obsolete typedef (open) syntax;
2012-01-03 blanchet 2012-01-03 reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
2011-12-24 haftmann 2011-12-24 commented out examples which choke on strict set/pred distinction
2011-11-30 wenzelm 2011-11-30 prefer typedef without extra definition and alternative name; tuned proofs;
2010-06-08 haftmann 2010-06-08 tuned quotes, antiquotations and whitespace
2010-04-23 wenzelm 2010-04-23 mark schematic statements explicitly;
2010-04-13 blanchet 2010-04-13 adapt Refute example to reflect latest soundness fix to Refute
2010-03-01 haftmann 2010-03-01 replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
2010-02-23 haftmann 2010-02-23 dropped axclass
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-10-17 wenzelm 2009-10-17 tuned;
2008-10-07 haftmann 2008-10-07 arbitrary is undefined
2007-10-15 webertj 2007-10-15 interpreter for List.append added again
2007-10-15 webertj 2007-10-15 quick_and_dirty (again) not touched anymore
2007-10-12 webertj 2007-10-12 significant code overhaul, bugfix for inductive data types
2007-08-28 wenzelm 2007-08-28 do not touch quick_and_dirty;
2007-07-11 berghofe 2007-07-11 Adapted to new inductive definition package.
2007-06-03 wenzelm 2007-06-03 tuned document;
2007-02-07 berghofe 2007-02-07 Adapted to changes in Finite_Set theory.
2007-01-19 webertj 2007-01-19 interpreter for Finite_Set.finite added
2007-01-04 webertj 2007-01-04 constants are unfolded, universal quantifiers are stripped, some minor changes
2006-11-27 webertj 2006-11-27 outermost universal quantifiers are stripped
2006-11-23 wenzelm 2006-11-23 prefer antiquotations over LaTeX macros;
2006-01-26 webertj 2006-01-26 smaller example to prevent timeout
2006-01-24 webertj 2006-01-24 works with DPLL solver now
2005-07-26 webertj 2005-07-26 minor parameter changes
2005-05-23 webertj 2005-05-23 interpreters for lfp/gfp added
2005-04-18 webertj 2005-04-18 support for recursion over mutually recursive IDTs
2005-02-23 webertj 2005-02-23 major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
2004-11-18 webertj 2004-11-18 imports (new syntax for theory headers)
2004-08-26 webertj 2004-08-26 comment modified
2004-05-26 webertj 2004-05-26 mainly new/different datatype examples
2004-03-26 webertj 2004-03-26 satsolver=dpll
2004-03-12 webertj 2004-03-12 \<dots> replaced by ...
2004-03-11 webertj 2004-03-11 Refute_Examples added/fixed
2004-03-10 webertj 2004-03-10 Updated examples
2004-01-10 webertj 2004-01-10 Adding 'refute' to HOL.