src/HOL/Library/refute.ML
Fri, 04 Jan 2019 23:22:53 +0100 wenzelm isabelle update -u control_cartouches;
Sun, 28 Jan 2018 19:28:52 +0100 wenzelm clarified take/drop/chop prefix/suffix;
Thu, 11 Jan 2018 13:48:17 +0100 wenzelm uniform use of Standard ML op-infix -- eliminated warnings;
Wed, 10 Jan 2018 15:25:09 +0100 nipkow ran isabelle update_op on all sources
Sat, 05 Mar 2016 17:01:45 +0100 wenzelm tuned signature -- clarified modules;
Tue, 01 Dec 2015 22:24:37 +0100 blanchet removed needless ML function
Thu, 13 Aug 2015 11:05:19 +0200 wenzelm tuned signature, in accordance to sortBy in Scala;
Wed, 22 Apr 2015 20:14:43 +0200 wenzelm allow diagnostic proof commands with skip_proofs;
Thu, 16 Apr 2015 14:18:32 +0200 wenzelm explicit error for Toplevel.proof_of;
Mon, 06 Apr 2015 17:06:48 +0200 wenzelm @{command_spec} is superseded by @{command_keyword};
Wed, 04 Mar 2015 19:53:18 +0100 wenzelm tuned signature -- prefer qualified names;
Sun, 11 Jan 2015 21:06:47 +0100 wenzelm tuned warnings: observe Context_Position.is_visible;
Mon, 03 Nov 2014 14:50:27 +0100 wenzelm eliminated unused int_only flag (see also c12484a27367);
Fri, 31 Oct 2014 11:36:41 +0100 wenzelm discontinued obsolete Output.urgent_message;
Wed, 29 Oct 2014 17:01:44 +0100 wenzelm modernized setup;
Wed, 17 Sep 2014 08:23:53 +0200 blanchet support (finite values of) codatatypes in Quickcheck
Fri, 12 Sep 2014 11:16:47 +0200 blanchet fixed spellings
Mon, 01 Sep 2014 17:34:03 +0200 blanchet ported Refute to use new datatypes when possible
Mon, 01 Sep 2014 16:17:47 +0200 blanchet compile
Mon, 01 Sep 2014 16:17:46 +0200 blanchet removed commented out parts
Sat, 09 Aug 2014 21:03:42 +0200 wenzelm tuned;
Sun, 04 May 2014 19:08:29 +0200 blanchet tuned structure name
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 18:14:58 +0200 blanchet renamed 'xxx_size' to 'size_xxx' for old datatype package
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
Sat, 22 Mar 2014 20:42:16 +0100 wenzelm more antiquotations;
Sat, 22 Mar 2014 18:15:09 +0100 wenzelm more antiquotations;
Fri, 21 Mar 2014 20:33:56 +0100 wenzelm more qualified names;
Fri, 21 Mar 2014 12:34:50 +0100 wenzelm more qualified names;
Fri, 14 Mar 2014 16:54:01 +0100 wenzelm prefer more robust Synchronized.var;
Mon, 03 Mar 2014 22:33:22 +0100 blanchet support 'datatype_new'-defined datatypes in Nitpick + better support for 'codatatype's
Sat, 15 Feb 2014 21:09:48 +0100 wenzelm removed odd comments -- inferred types are shown by Prover IDE;
Wed, 12 Feb 2014 08:35:56 +0100 blanchet repaired hard-coded constant names
Sun, 15 Dec 2013 19:01:06 +0100 blanchet use 'prop' rather than 'bool' systematically in Isar reconstruction code
Thu, 21 Nov 2013 21:33:34 +0100 blanchet compile
Wed, 10 Apr 2013 15:30:19 +0200 wenzelm more standard module name Axclass (according to file name);
Wed, 27 Mar 2013 17:58:07 +0100 wenzelm more robust access Toplevel.proof_of -- prefer warning via Toplevel.unknown_proof over hard crash (notably for skipped proofs);
Fri, 14 Dec 2012 16:33:22 +0100 wenzelm updated some headers;
Wed, 31 Oct 2012 11:23:21 +0100 blanchet moved Refute to "HOL/Library" to speed up building "Main" even more
less more (0) tip