src/HOL/Nitpick.thy
Wed, 31 Oct 2012 11:23:21 +0100 blanchet moved "SAT" before "FunDef" and moved back all SAT-related ML files to where they belong
Wed, 22 Aug 2012 22:55:41 +0200 wenzelm prefer ML_file over old uses;
Thu, 24 May 2012 17:25:53 +0200 wenzelm tuned proofs;
Fri, 11 May 2012 00:45:24 +0200 blanchet fixed "real" after they were redefined as a 'quotient_type'
Thu, 15 Mar 2012 22:08:53 +0100 wenzelm declare command keywords via theory header, including strict checking outside Pure;
Mon, 23 Jan 2012 17:40:32 +0100 blanchet added problem importer
Mon, 23 Jan 2012 17:40:31 +0100 blanchet rebranded Nitrox, for more uniformity
Sat, 24 Dec 2011 15:53:10 +0100 haftmann adjusted to set/pred distinction by means of type constructor `set`
Thu, 13 Oct 2011 23:27:46 +0200 haftmann bouned transitive closure
Thu, 18 Aug 2011 13:55:26 +0200 haftmann observe distinction between sets and predicates more properly
Tue, 02 Aug 2011 12:27:24 +0200 krauss replaced Nitpick's hardwired basic_ersatz_table by context data
Tue, 02 Aug 2011 10:36:50 +0200 krauss moved recdef package to HOL/Library/Old_Recdef.thy
Tue, 22 Mar 2011 19:04:32 +0100 blanchet added first-order TPTP version of Nitpick to Isabelle, so that its sources stay in sync with Isabelle and it is easier to install new versions for SystemOnTPTP and CASC -- the tool is called "isabelle nitrox" but is deliberately omitted from the tool list unless the component is explicitly enabled, to avoid clutter
Mon, 21 Feb 2011 11:50:38 +0100 blanchet rename Nitpick's (internal) auxiliary lemmas
Mon, 21 Feb 2011 10:44:19 +0100 blanchet renamed "nitpick\_def" to "nitpick_unfold" to reflect its new semantics
Tue, 07 Dec 2010 11:56:53 +0100 blanchet remove the "fin_fun" optimization in Nitpick -- it was always a hack and didn't help much
Tue, 07 Dec 2010 11:56:01 +0100 blanchet fix special handling of set products
Tue, 14 Sep 2010 16:33:38 +0200 blanchet remove more clutter related to old "fast_descrs" optimization
Mon, 13 Sep 2010 11:13:15 +0200 nipkow renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
Wed, 08 Sep 2010 16:01:06 +0200 blanchet merge
Mon, 06 Sep 2010 17:51:26 +0200 blanchet remove "minipick" (the toy version of Nitpick) and some tests;
Tue, 07 Sep 2010 10:05:19 +0200 nipkow expand_fun_eq -> ext_iff
Thu, 12 Aug 2010 17:56:41 +0200 haftmann group record-related ML files
Sat, 03 Jul 2010 00:50:35 +0200 blanchet adapt Nitpick to "prod_case" and "*" -> "sum" renaming;
Fri, 11 Jun 2010 17:05:11 +0200 blanchet adjust Nitpick's handling of "<" on "rat"s and "reals"
Mon, 31 May 2010 17:20:41 +0200 blanchet fix handling of "split" w.r.t. new definition + fix exception handling w.r.t. "expect" option
Fri, 14 May 2010 15:27:07 +0200 blanchet add "no_atp"s to Nitpick lemmas
Fri, 16 Apr 2010 21:28:09 +0200 wenzelm replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
Wed, 17 Mar 2010 09:14:43 +0100 blanchet added support for "specification" and "ax_specification" constructs to Nitpick
Wed, 10 Mar 2010 19:21:59 +0100 blanchet improve precision of "card" in Nitpick
Tue, 09 Mar 2010 14:18:21 +0100 blanchet improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
Tue, 09 Mar 2010 09:25:23 +0100 blanchet added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
Tue, 23 Feb 2010 11:05:32 +0100 blanchet improved Nitpick's support for quotient types
Mon, 22 Feb 2010 19:31:00 +0100 blanchet enabled Nitpick's support for quotient types + shortened the Nitpick tests a bit
Thu, 18 Feb 2010 18:48:07 +0100 blanchet added support for nonstandard "nat"s to Nitpick and fixed bugs in binary "nat"s and "int"s
Sat, 13 Feb 2010 15:04:09 +0100 blanchet more work on Nitpick's support for nonstandard models + fix in model reconstruction
Fri, 12 Feb 2010 19:44:37 +0100 blanchet various cosmetic changes to Nitpick
Tue, 09 Feb 2010 17:06:05 +0100 blanchet merged (manual for "nitpick_hol.ML" and "kodkod.ML")
Thu, 04 Feb 2010 16:03:15 +0100 blanchet split "nitpick_hol.ML" into two files to make it more manageable;
Fri, 05 Feb 2010 14:33:50 +0100 haftmann more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
Tue, 02 Feb 2010 11:38:38 +0100 blanchet added support for nonstandard models to Nitpick (based on an idea by Koen Claessen) and did other fixes to Nitpick
Wed, 20 Jan 2010 11:54:19 +0100 blanchet fix issues with previous Nitpick change
Thu, 17 Dec 2009 15:22:11 +0100 blanchet added support for binary nat/int representation to Nitpick
Tue, 17 Nov 2009 23:47:57 +0100 blanchet bump up Nitpick's axiom/definition unfolding limits, because some real-world problems (e.g. from Boogie) ran into the previous limits;
Wed, 11 Nov 2009 09:02:37 +0100 haftmann tuned imports
Wed, 28 Oct 2009 18:09:30 +0100 blanchet merged my Auto Nitpick change with Lukas's Predicate Compiler changes
Wed, 28 Oct 2009 17:43:43 +0100 blanchet introduced Auto Nitpick in addition to Auto Quickcheck;
Tue, 27 Oct 2009 16:52:06 +0100 blanchet renamed Nitpick option "coalesce_type_vars" to "merge_type_vars" (shorter) and cleaned up old hacks that are no longer necessary
Tue, 27 Oct 2009 15:32:20 +0100 haftmann dropped obsolete comment
Thu, 22 Oct 2009 14:51:47 +0200 blanchet added Nitpick's theory and ML files to Isabelle/HOL;
less more (0) tip