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