Mercurial Mercurial > repos > isabelle / file revisions
summary | shortlog | changelog | graph | tags | bookmarks | branches | file | revisions | annotate | diff | comparison | rss | help
(0) -100 -60 tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/Nitpick/nitpick.ML
Sat, 16 Apr 2011 16:15:37 +0200 wenzelm modernized structure Proof_Context; file | diff | annotate
Fri, 18 Mar 2011 11:43:28 +0100 blanchet optimize Kodkod bounds when "need" is specified file | diff | annotate
Thu, 17 Mar 2011 22:07:17 +0100 blanchet reintroduced "show_skolems" option -- useful when too many Skolems are displayed file | diff | annotate
Thu, 17 Mar 2011 14:43:53 +0100 blanchet reword Nitpick's wording concerning potential counterexamples file | diff | annotate
Tue, 15 Mar 2011 15:49:42 +0100 blanchet support non-ground "need" values file | diff | annotate
Sun, 13 Mar 2011 16:01:00 +0100 wenzelm Path.print is the official way to show file-system paths to users -- note that Path.implode often indicates violation of the abstract datatype; file | diff | annotate
Wed, 09 Mar 2011 10:25:29 +0100 blanchet perform no arity check in debug mode so that we get to see the Kodkod problem file | diff | annotate
Thu, 03 Mar 2011 14:25:15 +0100 blanchet don't forget to look for constants appearing only in "need" option -- otherwise we get exceptions in "the_name" later on file | diff | annotate
Thu, 03 Mar 2011 11:20:48 +0100 blanchet simplify "need" option's syntax file | diff | annotate
Thu, 03 Mar 2011 11:20:48 +0100 blanchet renamed "preconstr" option "need" file | diff | annotate
Wed, 02 Mar 2011 15:51:22 +0100 blanchet added missing spaces in output file | diff | annotate
Wed, 02 Mar 2011 14:50:16 +0100 blanchet lower threshold for implicitly using "nitpick_simp" for predicate definitions when "total_consts" is on file | diff | annotate
Wed, 02 Mar 2011 13:09:57 +0100 blanchet robust handling of types occurring in "eval" and "preconstr" options but not in the goal file | diff | annotate
Wed, 02 Mar 2011 13:09:57 +0100 blanchet make "preconstr" option more robust -- shouldn't throw exceptions file | diff | annotate
Mon, 28 Feb 2011 17:53:10 +0100 blanchet if "total_consts" is set, report cex's as quasi-genuine file | diff | annotate
Mon, 28 Feb 2011 17:53:10 +0100 blanchet added "total_consts" option file | diff | annotate
Mon, 21 Feb 2011 17:36:32 +0100 blanchet more work on "fix_datatype_vals" optimization (renamed "preconstruct") file | diff | annotate
Mon, 21 Feb 2011 16:33:21 +0100 blanchet more work on "fix_datatype_vals" file | diff | annotate
Mon, 21 Feb 2011 15:45:44 +0100 blanchet first steps in implementing "fix_datatype_vals" optimization file | diff | annotate
Mon, 21 Feb 2011 11:50:31 +0100 blanchet tweaked Nitpick based on C++ memory model example file | diff | annotate
Mon, 21 Feb 2011 10:42:29 +0100 blanchet always unfold constant defitions marked with "nitpick_def" -- to prevent unfolding, there's already "nitpick_simp" file | diff | annotate
Mon, 21 Feb 2011 10:29:13 +0100 blanchet don't distinguish between "fixes" and other free variables -- this confuses users file | diff | annotate
Fri, 18 Feb 2011 16:19:08 +0100 blanchet make Nitpick's timeout mechanism somewhat more reliable/friendly; file | diff | annotate
Sun, 19 Dec 2010 11:48:42 +0100 blanchet added a timestamp to Nitpick in verbose mode for debugging purposes; file | diff | annotate
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 file | diff | annotate
Tue, 07 Dec 2010 11:56:01 +0100 blanchet give the inner timeout mechanism a chance, since it gives more precise information to the user file | diff | annotate
Tue, 07 Dec 2010 11:56:01 +0100 blanchet added a hint when the user obviously just forgot a colon after the lemma's name file | diff | annotate
Mon, 06 Dec 2010 13:33:09 +0100 blanchet use ML SAT solvers up to a certain time limit, then switch to faster solvers with a timeout -- this becomes necessary with the new, more powerful monotonicity calculus file | diff | annotate
Mon, 06 Dec 2010 13:33:09 +0100 blanchet removed old baggage from monotonicity calculus -- the "calculus" option didn't really work anyway because of on-the-fly simplifications file | diff | annotate
Mon, 06 Dec 2010 13:18:25 +0100 blanchet support 3 monotonicity calculi in one and fix soundness bug file | diff | annotate
Sun, 07 Nov 2010 13:29:59 +0100 blanchet removed explicit "Interrupt" handling for conformity with async model -- unfortunately the user loses the information about how many scopes were checked, but this needs to be retought with the new interface anyway file | diff | annotate
Fri, 05 Nov 2010 19:47:20 +0100 wenzelm explicit indication of some remaining violations of the Isabelle/ML interrupt model; file | diff | annotate
Wed, 03 Nov 2010 22:26:53 +0100 blanchet standardize on seconds for Nitpick and Sledgehammer timeouts file | diff | annotate
Thu, 28 Oct 2010 09:29:57 +0200 blanchet clear identification file | diff | annotate
Mon, 25 Oct 2010 21:06:56 +0200 wenzelm renamed Output.priority to Output.urgent_message to emphasize its special role more clearly; file | diff | annotate
Tue, 14 Sep 2010 14:12:18 +0200 blanchet tuning file | diff | annotate
Tue, 14 Sep 2010 13:24:18 +0200 blanchet remove "fast_descs" option from Nitpick; file | diff | annotate
Mon, 13 Sep 2010 20:21:40 +0200 blanchet remove unreferenced identifiers file | diff | annotate
Sat, 11 Sep 2010 10:20:25 +0200 blanchet change defaults of Auto Nitpick so that it consumes less resources (time and Kodkod threads) file | diff | annotate
Fri, 27 Aug 2010 19:34:23 +0200 haftmann renamed class/constant eq to equal; tuned some instantiations file | diff | annotate
Wed, 18 Aug 2010 11:14:33 +0200 blanchet with Kodkodi 1.2.15, Java 1.5 is fine file | diff | annotate
Wed, 18 Aug 2010 10:42:04 +0200 blanchet gracefully handle the case where the JVM is too old in Nitpick file | diff | annotate
Fri, 06 Aug 2010 17:05:29 +0200 blanchet local versions of Nitpick.register_xxx functions file | diff | annotate
Fri, 06 Aug 2010 11:33:58 +0200 blanchet added a friendly warning file | diff | annotate
Fri, 06 Aug 2010 10:50:52 +0200 blanchet improved "merge_type_vars" option: map supersorts to subsorts, to avoid distinguishing, say, "{}", and "HOL.type" file | diff | annotate
Thu, 05 Aug 2010 20:17:50 +0200 blanchet added "whack" file | diff | annotate
Tue, 03 Aug 2010 21:20:31 +0200 blanchet better "Pretty" handling file | diff | annotate
Tue, 03 Aug 2010 15:15:17 +0200 blanchet more helpful message file | diff | annotate
Tue, 03 Aug 2010 12:16:32 +0200 blanchet fix soundness bug w.r.t. "Suc" with "binary_ints" file | diff | annotate
Tue, 03 Aug 2010 02:18:05 +0200 blanchet handle free variables even more gracefully; file | diff | annotate
Tue, 03 Aug 2010 01:16:08 +0200 blanchet optimize local "def"s by treating them as definitions file | diff | annotate
Sun, 01 Aug 2010 15:51:25 +0200 blanchet added manual symmetry breaking for datatypes file | diff | annotate
Sat, 31 Jul 2010 16:39:32 +0200 blanchet started implementation of custom sym break file | diff | annotate
Sat, 31 Jul 2010 12:29:56 +0200 blanchet clarify Nitpick's output in case of a potential counterexample file | diff | annotate
Wed, 21 Jul 2010 21:16:58 +0200 blanchet do a better job at Skolemizing in Nitpick, for TPTP FOF file | diff | annotate
Sat, 03 Jul 2010 00:50:35 +0200 blanchet adapt Nitpick to "prod_case" and "*" -> "sum" renaming; file | diff | annotate
Tue, 22 Jun 2010 13:17:59 +0200 blanchet distinguish between "unknown" and "no Kodkodi installed" errors file | diff | annotate
Tue, 01 Jun 2010 17:52:19 +0200 blanchet merged file | diff | annotate
Tue, 01 Jun 2010 12:20:08 +0200 blanchet added "atoms" option to Nitpick (request from Karlsruhe) + wrap Refute. functions to "nitpick_util.ML" file | diff | annotate
Tue, 01 Jun 2010 10:32:29 +0200 blanchet remove comment file | diff | annotate
less more (0) -100 -60 tip
isabelle