doc-src/Nitpick/nitpick.tex
2011-05-01 wenzelm 2011-05-01 eliminated copies of isabelle style files;
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-03 blanchet 2011-03-03 simplify "need" option's syntax
2011-03-03 blanchet 2011-03-03 renamed "preconstr" option "need"
2011-02-28 blanchet 2011-02-28 document new "total_consts" option
2011-02-21 blanchet 2011-02-21 document new "preconstr" option
2011-02-21 blanchet 2011-02-21 updated docs w.r.t. "nitpick_unfold" attribute
2011-02-21 blanchet 2011-02-21 updated docs
2011-02-21 blanchet 2011-02-21 tweaked Nitpick based on C++ memory model example
2010-12-07 blanchet 2010-12-07 updated Nitpick's documentation w.r.t. finitization
2010-11-24 blanchet 2010-11-24 document requirement on theory import
2010-11-03 blanchet 2010-11-03 use floating-point numbers for Sledgehammer's "thresholds" option rather than percentages; updated docs
2010-11-03 blanchet 2010-11-03 standardize on seconds for Nitpick and Sledgehammer timeouts
2010-10-26 blanchet 2010-10-26 improved English
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-11 blanchet 2010-09-11 document changes to Auto Nitpick
2010-08-31 blanchet 2010-08-31 fix typo
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-09 blanchet 2010-08-09 use "declaration" instead of "setup" to register Nitpick extensions
2010-08-06 blanchet 2010-08-06 minor doc changes
2010-08-06 blanchet 2010-08-06 document the non-legacy interfaces
2010-08-06 blanchet 2010-08-06 extend the scope of limitation about nonconservative extensions
2010-08-05 blanchet 2010-08-05 added "whack"
2010-08-05 blanchet 2010-08-05 added support for "Abs_" and "Rep_" functions on quotient types
2010-08-05 blanchet 2010-08-05 more docs
2010-08-05 blanchet 2010-08-05 make nitpick accept "==" for "nitpick_(p)simp"s
2010-08-03 blanchet 2010-08-03 updated example timings
2010-08-03 blanchet 2010-08-03 also mention gfp
2010-08-03 blanchet 2010-08-03 more documentation, based on email discussions with a user
2010-08-03 blanchet 2010-08-03 make example easier to parse
2010-08-03 blanchet 2010-08-03 clarify attribute documentation
2010-08-03 blanchet 2010-08-03 choose better example
2010-08-03 blanchet 2010-08-03 document something I explained in an email to a poweruser
2010-08-03 blanchet 2010-08-03 make Nitpick more flexible when parsing (p)simp rules
2010-08-01 blanchet 2010-08-01 document new Nitpick options
2010-07-31 blanchet 2010-07-31 change the order of the SAT solvers, from fastest to slowest
2010-07-31 blanchet 2010-07-31 clarify Nitpick's output in case of a potential counterexample
2010-07-31 blanchet 2010-07-31 added support for CryptoMiniSat
2010-06-01 blanchet 2010-06-01 removed "nitpick_intro" attribute -- Nitpick noew uses Spec_Rules instead
2010-06-01 blanchet 2010-06-01 document new option
2010-05-27 blanchet 2010-05-27 make Nitpick "show_all" option behave less surprisingly
2010-05-14 blanchet 2010-05-14 added Sledgehammer manual; some material was recovered from the Isar material, the rest is new
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 fix typesetting
2010-04-24 blanchet 2010-04-24 Fruhjahrsputz: remove three mostly useless Nitpick options
2010-04-21 blanchet 2010-04-21 use only one thread in "Manual_Nits"; the second thread isn't helping much, and might very well be the cause of the Cygwin Isatest failure
2010-04-13 blanchet 2010-04-13 cosmetics
2010-03-17 blanchet 2010-03-17 minor additions to Nitpick docs
2010-03-17 blanchet 2010-03-17 document "nitpick_choice_spec" attribute
2010-03-11 blanchet 2010-03-11 added a mechanism to Nitpick to support custom rendering of terms, and used it for multisets
2010-03-11 blanchet 2010-03-11 made "Manual_Nits" tests more robust
2010-03-10 blanchet 2010-03-10 fixed soundness bug in Nitpick
2010-03-09 blanchet 2010-03-09 added "finitize" option to Nitpick + remove dependency on "Coinductive_List"
2010-02-26 blanchet 2010-02-26 more work on the new monotonicity stuff in Nitpick
2010-02-25 blanchet 2010-02-25 improved precision of infinite "shallow" datatypes in Nitpick; e.g. strings used for variable names, instead of an opaque type