src/HOL/ex/Refute_Examples.thy
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.