--- a/src/HOL/Tools/Nitpick/HISTORY Tue Mar 09 09:25:23 2010 +0100
+++ b/src/HOL/Tools/Nitpick/HISTORY Tue Mar 09 14:18:21 2010 +0100
@@ -2,13 +2,13 @@
* Added and implemented "binary_ints" and "bits" options
* Added "std" option and implemented support for nonstandard models
+ * Added and implemented "finitize" option to improve the precision of infinite
+ datatypes based on a monotonicity analysis
* Added support for quotient types
- * Added support for local definitions
- * Disabled "fast_descrs" option by default
+ * Added support for local definitions (for "function" and "termination"
+ proofs)
* Optimized "Multiset.multiset" and "FinFun.finfun"
* Improved efficiency of "destroy_constrs" optimization
- * Improved precision of infinite datatypes whose constructors don't appear
- in the formula to falsify based on a monotonicity analysis
* Fixed soundness bugs related to "destroy_constrs" optimization and record
getters
* Renamed "MiniSatJNI", "zChaffJNI", "BerkMinAlloy", and "SAT4JLight" to