src/HOL/Library/refute.ML
2016-03-05 wenzelm 2016-03-05 tuned signature -- clarified modules;
2015-12-01 blanchet 2015-12-01 removed needless ML function
2015-08-13 wenzelm 2015-08-13 tuned signature, in accordance to sortBy in Scala;
2015-04-22 wenzelm 2015-04-22 allow diagnostic proof commands with skip_proofs;
2015-04-16 wenzelm 2015-04-16 explicit error for Toplevel.proof_of; eliminated obsolete Toplevel.unknown_proof; more total Toplevel.proof_position_of;
2015-04-06 wenzelm 2015-04-06 @{command_spec} is superseded by @{command_keyword};
2015-03-04 wenzelm 2015-03-04 tuned signature -- prefer qualified names;
2015-01-11 wenzelm 2015-01-11 tuned warnings: observe Context_Position.is_visible;
2014-11-03 wenzelm 2014-11-03 eliminated unused int_only flag (see also c12484a27367); just proper commands;
2014-10-31 wenzelm 2014-10-31 discontinued obsolete Output.urgent_message;
2014-10-29 wenzelm 2014-10-29 modernized setup;
2014-09-17 blanchet 2014-09-17 support (finite values of) codatatypes in Quickcheck
2014-09-12 blanchet 2014-09-12 fixed spellings
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