src/HOL/ex/Refute_Examples.thy
2016-01-11 wenzelm 2016-01-11 eliminated old defs;
2015-12-26 wenzelm 2015-12-26 isabelle update_cartouches -c -t;
2015-10-06 wenzelm 2015-10-06 isabelle update_cartouches;
2015-10-06 wenzelm 2015-10-06 fewer aliases for toplevel theorem statements;
2015-04-09 blanchet 2015-04-09 removed a refute example that caused trouble with testing
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
2014-09-11 blanchet 2014-09-11 updated news
2014-09-11 blanchet 2014-09-11 renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
2014-09-11 blanchet 2014-09-11 took out some datatype tests for Refute -- these yield timeouts on some Isatests after transition to new datatypes, for some reason (and Refute is obsolete anyway)
2014-09-08 blanchet 2014-09-08 adapted examples to latest changes
2014-09-04 blanchet 2014-09-04 tuned Nitpick and Refute examples, which are too slow on some testing machines
2014-09-02 blanchet 2014-09-02 removed more slow Refute tests
2014-09-02 blanchet 2014-09-02 tuned Refute example
2014-09-01 blanchet 2014-09-01 ported Refute to use new datatypes when possible
2014-05-04 blanchet 2014-05-04 renamed 'dpll_p' to 'cdclite', to avoid confusion with the old 'dpll' and to reflect the idea that the new prover implements some ideas from CDCL not in DPLL -- this follows its author's, Sascha B.'s, wish
2014-05-04 boehmes 2014-05-04 removed obsolete internal SAT solvers
2014-05-01 boehmes 2014-05-01 added internal proof-producing SAT solver
2014-03-21 wenzelm 2014-03-21 more qualified names;
2014-03-03 blanchet 2014-03-03 rationalized internals
2014-02-12 blanchet 2014-02-12 adapted theories to 'xxx_case' to 'case_xxx' * * * 'char_case' -> 'case_char' and same for 'rec' * * * compile * * * renamed 'xxx_case' to 'case_xxx'
2014-02-12 blanchet 2014-02-12 renamed 'nat_{case,rec}' to '{case,rec}_nat'
2014-02-12 blanchet 2014-02-12 adapted theories to '{case,rec}_{list,option}' names
2014-02-12 blanchet 2014-02-12 removed trivial 'rec' examples for nonrecursive types (I could also have added the 'old.' prefix in front of the constant names)
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