src/HOL/ex/Refute_Examples.thy
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
Fri, 21 Mar 2014 20:33:56 +0100 wenzelm more qualified names;
Mon, 03 Mar 2014 12:48:20 +0100 blanchet rationalized internals
Wed, 12 Feb 2014 08:35:57 +0100 blanchet adapted theories to 'xxx_case' to 'case_xxx'
Wed, 12 Feb 2014 08:35:57 +0100 blanchet renamed 'nat_{case,rec}' to '{case,rec}_nat'
Wed, 12 Feb 2014 08:35:56 +0100 blanchet adapted theories to '{case,rec}_{list,option}' names
Wed, 12 Feb 2014 08:35:56 +0100 blanchet removed trivial 'rec' examples for nonrecursive types (I could also have added the 'old.' prefix in front of the constant names)
Wed, 31 Oct 2012 11:23:21 +0100 blanchet fixes related to Refute's move
Fri, 12 Oct 2012 18:58:20 +0200 wenzelm discontinued obsolete typedef (open) syntax;
Tue, 03 Jan 2012 18:33:18 +0100 blanchet reintroduced 'refute' calls taken out after reintroducing the "set" constructor, and use "expect" feature
Sat, 24 Dec 2011 15:53:11 +0100 haftmann commented out examples which choke on strict set/pred distinction
Wed, 30 Nov 2011 16:27:10 +0100 wenzelm prefer typedef without extra definition and alternative name;
Tue, 08 Jun 2010 16:37:22 +0200 haftmann tuned quotes, antiquotations and whitespace
Fri, 23 Apr 2010 23:35:43 +0200 wenzelm mark schematic statements explicitly;
Tue, 13 Apr 2010 15:30:15 +0200 blanchet adapt Refute example to reflect latest soundness fix to Refute
Mon, 01 Mar 2010 13:40:23 +0100 haftmann replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
Tue, 23 Feb 2010 10:11:12 +0100 haftmann dropped axclass
Mon, 14 Dec 2009 12:14:12 +0100 blanchet added "no_assms" option to Refute, and include structured proof assumptions by default;
Sat, 17 Oct 2009 16:34:39 +0200 wenzelm tuned;
Tue, 07 Oct 2008 16:07:50 +0200 haftmann arbitrary is undefined
Mon, 15 Oct 2007 01:57:50 +0200 webertj interpreter for List.append added again
Mon, 15 Oct 2007 01:36:22 +0200 webertj quick_and_dirty (again) not touched anymore
Fri, 12 Oct 2007 22:00:47 +0200 webertj significant code overhaul, bugfix for inductive data types
Tue, 28 Aug 2007 11:25:32 +0200 wenzelm do not touch quick_and_dirty;
Wed, 11 Jul 2007 11:54:21 +0200 berghofe Adapted to new inductive definition package.
Sun, 03 Jun 2007 23:16:47 +0200 wenzelm tuned document;
Wed, 07 Feb 2007 18:12:02 +0100 berghofe Adapted to changes in Finite_Set theory.
Fri, 19 Jan 2007 22:04:22 +0100 webertj interpreter for Finite_Set.finite added
Thu, 04 Jan 2007 00:12:30 +0100 webertj constants are unfolded, universal quantifiers are stripped, some minor changes
Mon, 27 Nov 2006 17:35:50 +0100 webertj outermost universal quantifiers are stripped
Thu, 23 Nov 2006 20:34:21 +0100 wenzelm prefer antiquotations over LaTeX macros;
Thu, 26 Jan 2006 20:17:54 +0100 webertj smaller example to prevent timeout
Tue, 24 Jan 2006 15:16:06 +0100 webertj works with DPLL solver now
Tue, 26 Jul 2005 12:13:35 +0200 webertj minor parameter changes
Mon, 23 May 2005 17:17:06 +0200 webertj interpreters for lfp/gfp added
Mon, 18 Apr 2005 17:20:49 +0200 webertj support for recursion over mutually recursive IDTs
Wed, 23 Feb 2005 14:04:53 +0100 webertj major code change: refute can now handle recursion and axiomatic type classes; 3-valued logic with two kinds of equality; some bugfixes
Thu, 18 Nov 2004 18:46:09 +0100 webertj imports (new syntax for theory headers)
Thu, 26 Aug 2004 17:28:57 +0200 webertj comment modified
Wed, 26 May 2004 18:23:46 +0200 webertj mainly new/different datatype examples
Fri, 26 Mar 2004 19:58:43 +0100 webertj satsolver=dpll
Fri, 12 Mar 2004 10:47:59 +0100 webertj \<dots> replaced by ...
Thu, 11 Mar 2004 11:24:54 +0100 webertj Refute_Examples added/fixed
Wed, 10 Mar 2004 20:36:11 +0100 webertj Updated examples
Sat, 10 Jan 2004 13:35:10 +0100 webertj Adding 'refute' to HOL.
less more (0) tip