src/HOL/ex/Refute_Examples.thy
Tue, 06 Oct 2015 17:47:28 +0200 wenzelm isabelle update_cartouches;
Tue, 06 Oct 2015 15:14:28 +0200 wenzelm fewer aliases for toplevel theorem statements;
Thu, 09 Apr 2015 18:00:59 +0200 blanchet removed a refute example that caused trouble with testing
Sun, 02 Nov 2014 18:21:45 +0100 wenzelm modernized header uniformly as section;
Thu, 11 Sep 2014 19:32:36 +0200 blanchet updated news
Thu, 11 Sep 2014 18:54:36 +0200 blanchet renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
Thu, 11 Sep 2014 18:54:36 +0200 blanchet 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)
Mon, 08 Sep 2014 16:14:21 +0200 blanchet adapted examples to latest changes
Thu, 04 Sep 2014 11:53:39 +0200 blanchet tuned Nitpick and Refute examples, which are too slow on some testing machines
Tue, 02 Sep 2014 23:59:49 +0200 blanchet removed more slow Refute tests
Tue, 02 Sep 2014 23:59:46 +0200 blanchet tuned Refute example
Mon, 01 Sep 2014 17:34:03 +0200 blanchet ported Refute to use new datatypes when possible
Sun, 04 May 2014 18:57:45 +0200 blanchet 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
Sun, 04 May 2014 16:17:53 +0200 boehmes removed obsolete internal SAT solvers
Thu, 01 May 2014 22:56:59 +0200 boehmes added internal proof-producing SAT solver
less more (0) -15 tip