src/HOL/Tools/Nitpick/nitpick.ML
2012-03-25 huffman 2012-03-25 merged fork with new numeral representation (see NEWS)
2012-01-17 blanchet 2012-01-17 updated message
2012-01-04 blanchet 2012-01-04 remove subtlety whose justification got lost in time -- the new code is possibly less precise but sounder
2012-01-03 blanchet 2012-01-03 always treat "unit" as a deep datatype, so that we get a good interaction with the record syntax (2.7 of the Nitpick manual)
2012-01-03 blanchet 2012-01-03 rationalized output (a bit)
2011-11-28 wenzelm 2011-11-28 separate module for concrete Isabelle markup;
2011-08-22 blanchet 2011-08-22 more precise warning
2011-06-30 wenzelm 2011-06-30 standardized use of Path operations;
2011-05-27 blanchet 2011-05-27 handle non-auto try case gracefully in Nitpick
2011-05-27 blanchet 2011-05-27 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
2011-05-24 blanchet 2011-05-24 use \<emdash> rather than \<midarrow>
2011-04-27 wenzelm 2011-04-27 direct use of Variable.is_fixed;
2011-04-19 blanchet 2011-04-19 use "Spec_Rules" for finding axioms -- more reliable and cleaner
2011-04-16 wenzelm 2011-04-16 modernized structure Proof_Context;
2011-03-18 blanchet 2011-03-18 optimize Kodkod bounds when "need" is specified
2011-03-17 blanchet 2011-03-17 reintroduced "show_skolems" option -- useful when too many Skolems are displayed
2011-03-17 blanchet 2011-03-17 reword Nitpick's wording concerning potential counterexamples
2011-03-15 blanchet 2011-03-15 support non-ground "need" values
2011-03-13 wenzelm 2011-03-13 Path.print is the official way to show file-system paths to users -- note that Path.implode often indicates violation of the abstract datatype;
2011-03-09 blanchet 2011-03-09 perform no arity check in debug mode so that we get to see the Kodkod problem
2011-03-03 blanchet 2011-03-03 don't forget to look for constants appearing only in "need" option -- otherwise we get exceptions in "the_name" later on
2011-03-03 blanchet 2011-03-03 simplify "need" option's syntax
2011-03-03 blanchet 2011-03-03 renamed "preconstr" option "need"
2011-03-02 blanchet 2011-03-02 added missing spaces in output
2011-03-02 blanchet 2011-03-02 lower threshold for implicitly using "nitpick_simp" for predicate definitions when "total_consts" is on
2011-03-02 blanchet 2011-03-02 robust handling of types occurring in "eval" and "preconstr" options but not in the goal
2011-03-02 blanchet 2011-03-02 make "preconstr" option more robust -- shouldn't throw exceptions
2011-02-28 blanchet 2011-02-28 if "total_consts" is set, report cex's as quasi-genuine
2011-02-28 blanchet 2011-02-28 added "total_consts" option
2011-02-21 blanchet 2011-02-21 more work on "fix_datatype_vals" optimization (renamed "preconstruct")
2011-02-21 blanchet 2011-02-21 more work on "fix_datatype_vals"
2011-02-21 blanchet 2011-02-21 first steps in implementing "fix_datatype_vals" optimization
2011-02-21 blanchet 2011-02-21 tweaked Nitpick based on C++ memory model example
2011-02-21 blanchet 2011-02-21 always unfold constant defitions marked with "nitpick_def" -- to prevent unfolding, there's already "nitpick_simp"
2011-02-21 blanchet 2011-02-21 don't distinguish between "fixes" and other free variables -- this confuses users
2011-02-18 blanchet 2011-02-18 make Nitpick's timeout mechanism somewhat more reliable/friendly; avoid producing warnings when invoked in "auto" mode
2010-12-19 blanchet 2010-12-19 added a timestamp to Nitpick in verbose mode for debugging purposes; turn on verbose mode for the examples
2010-12-07 blanchet 2010-12-07 remove the "fin_fun" optimization in Nitpick -- it was always a hack and didn't help much
2010-12-07 blanchet 2010-12-07 give the inner timeout mechanism a chance, since it gives more precise information to the user
2010-12-07 blanchet 2010-12-07 added a hint when the user obviously just forgot a colon after the lemma's name
2010-12-06 blanchet 2010-12-06 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
2010-12-06 blanchet 2010-12-06 removed old baggage from monotonicity calculus -- the "calculus" option didn't really work anyway because of on-the-fly simplifications
2010-12-06 blanchet 2010-12-06 support 3 monotonicity calculi in one and fix soundness bug
2010-11-07 blanchet 2010-11-07 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
2010-11-05 wenzelm 2010-11-05 explicit indication of some remaining violations of the Isabelle/ML interrupt model;
2010-11-03 blanchet 2010-11-03 standardize on seconds for Nitpick and Sledgehammer timeouts
2010-10-28 blanchet 2010-10-28 clear identification
2010-10-25 wenzelm 2010-10-25 renamed Output.priority to Output.urgent_message to emphasize its special role more clearly;
2010-09-14 blanchet 2010-09-14 tuning
2010-09-14 blanchet 2010-09-14 remove "fast_descs" option from Nitpick; the option has been unsound for over a year and is too imprecise to be of any use when made sound
2010-09-13 blanchet 2010-09-13 remove unreferenced identifiers
2010-09-11 blanchet 2010-09-11 change defaults of Auto Nitpick so that it consumes less resources (time and Kodkod threads)
2010-08-27 haftmann 2010-08-27 renamed class/constant eq to equal; tuned some instantiations
2010-08-18 blanchet 2010-08-18 with Kodkodi 1.2.15, Java 1.5 is fine
2010-08-18 blanchet 2010-08-18 gracefully handle the case where the JVM is too old in Nitpick
2010-08-06 blanchet 2010-08-06 local versions of Nitpick.register_xxx functions
2010-08-06 blanchet 2010-08-06 added a friendly warning
2010-08-06 blanchet 2010-08-06 improved "merge_type_vars" option: map supersorts to subsorts, to avoid distinguishing, say, "{}", and "HOL.type"
2010-08-05 blanchet 2010-08-05 added "whack"
2010-08-03 blanchet 2010-08-03 better "Pretty" handling