src/HOL/Library/refute.ML
2014-09-01 blanchet 2014-09-01 ported Refute to use new datatypes when possible
2014-09-01 blanchet 2014-09-01 compile
2014-09-01 blanchet 2014-09-01 removed commented out parts
2014-08-09 wenzelm 2014-08-09 tuned;
2014-05-04 blanchet 2014-05-04 tuned structure name
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 blanchet 2014-05-04 renamed 'xxx_size' to 'size_xxx' for old datatype package
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-22 wenzelm 2014-03-22 more antiquotations;
2014-03-22 wenzelm 2014-03-22 more antiquotations;
2014-03-21 wenzelm 2014-03-21 more qualified names;
2014-03-21 wenzelm 2014-03-21 more qualified names;
2014-03-14 wenzelm 2014-03-14 prefer more robust Synchronized.var;
2014-03-03 blanchet 2014-03-03 support 'datatype_new'-defined datatypes in Nitpick + better support for 'codatatype's
2014-02-15 wenzelm 2014-02-15 removed odd comments -- inferred types are shown by Prover IDE;
2014-02-12 blanchet 2014-02-12 repaired hard-coded constant names
2013-12-15 blanchet 2013-12-15 use 'prop' rather than 'bool' systematically in Isar reconstruction code
2013-11-21 blanchet 2013-11-21 compile
2013-04-10 wenzelm 2013-04-10 more standard module name Axclass (according to file name);
2013-03-27 wenzelm 2013-03-27 more robust access Toplevel.proof_of -- prefer warning via Toplevel.unknown_proof over hard crash (notably for skipped proofs);
2012-12-14 wenzelm 2012-12-14 updated some headers;
2012-10-31 blanchet 2012-10-31 moved Refute to "HOL/Library" to speed up building "Main" even more