src/HOL/Tools/Nitpick/nitpick.ML
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
2010-08-03 blanchet 2010-08-03 more helpful message
2010-08-03 blanchet 2010-08-03 fix soundness bug w.r.t. "Suc" with "binary_ints"
2010-08-03 blanchet 2010-08-03 handle free variables even more gracefully; 1. show those that only occur in assumptions as part of the constants; 2. make sure locally defined Frees are given an Opt rep, just like constants generally owuld
2010-08-03 blanchet 2010-08-03 optimize local "def"s by treating them as definitions
2010-08-01 blanchet 2010-08-01 added manual symmetry breaking for datatypes
2010-07-31 blanchet 2010-07-31 started implementation of custom sym break
2010-07-31 blanchet 2010-07-31 clarify Nitpick's output in case of a potential counterexample
2010-07-21 blanchet 2010-07-21 do a better job at Skolemizing in Nitpick, for TPTP FOF
2010-07-03 blanchet 2010-07-03 adapt Nitpick to "prod_case" and "*" -> "sum" renaming; the code in "Nitpick_Preproc", which sorted the types using "typ_ord", was wrong and evil; it seems to have worked only because "*" was called "*"
2010-06-22 blanchet 2010-06-22 distinguish between "unknown" and "no Kodkodi installed" errors
2010-06-01 blanchet 2010-06-01 merged
2010-06-01 blanchet 2010-06-01 added "atoms" option to Nitpick (request from Karlsruhe) + wrap Refute. functions to "nitpick_util.ML"
2010-06-01 blanchet 2010-06-01 remove comment
2010-06-01 blanchet 2010-06-01 thread along context instead of theory for typedef lookup
2010-05-31 wenzelm 2010-05-31 modernized some structure names, keeping a few legacy aliases;
2010-05-31 blanchet 2010-05-31 fix handling of "split" w.r.t. new definition + fix exception handling w.r.t. "expect" option
2010-05-27 wenzelm 2010-05-27 renamed structure PrintMode to Print_Mode, keeping the old name as legacy alias for some time;
2010-05-14 blanchet 2010-05-14 improve precision of set constructs in Nitpick
2010-04-26 blanchet 2010-04-26 fixes 2a5c6e7b55cb; do not throw out the baby with the bath water
2010-04-26 blanchet 2010-04-26 remove needless code that was copy-pasted from Quickcheck (where it made sense)
2010-04-25 blanchet 2010-04-25 remove "show_skolems" option and change style of record declarations
2010-04-25 blanchet 2010-04-25 remove "skolemize" option from Nitpick, since Skolemization is always useful
2010-04-24 blanchet 2010-04-24 removed Nitpick's "uncurry" option
2010-04-24 blanchet 2010-04-24 Fruhjahrsputz: remove three mostly useless Nitpick options
2010-04-24 blanchet 2010-04-24 remove type annotations as comments; Nitpick is now 1136 lines shorter
2010-04-24 blanchet 2010-04-24 cosmetics
2010-04-23 blanchet 2010-04-23 stop referring to Sledgehammer_Util stuff all over Nitpick code; instead, redeclare any needed function in Nitpick_Util as synonym for the Sledgehammer_Util function of the same name
2010-04-21 blanchet 2010-04-21 clarify error message
2010-04-13 blanchet 2010-04-13 make Nitpick output everything to tracing in debug mode; so that when an exception occurs, I can switch to the tracing window to see what was in the response window before the exception blew everything away
2010-04-13 blanchet 2010-04-13 cosmetics
2010-03-24 blanchet 2010-03-24 simplify Nitpick parameter parsing code a little bit + make compile
2010-03-17 blanchet 2010-03-17 added one-entry cache around Kodkod invocation
2010-03-17 blanchet 2010-03-17 added support for "specification" and "ax_specification" constructs to Nitpick
2010-03-11 blanchet 2010-03-11 added term postprocessor to Nitpick, to provide custom syntax for typedefs
2010-03-10 blanchet 2010-03-10 show nice error message in Nitpick when "java" is not available
2010-03-09 blanchet 2010-03-09 improved Nitpick's precision for "card" and "setsum" + fix incorrect outcome code w.r.t. "bisim_depth = -1"
2010-03-09 blanchet 2010-03-09 added "finitize" option to Nitpick + remove dependency on "Coinductive_List"