# HG changeset patch
# User blanchet
# Date 1273871793 -7200
# Node ID 637100169bc752bccd09c3f8858149e8d1b3ee39
# Parent  476a8d4f5c8be891c54085ba5b41bde750e0099f
document Nitpick changes

diff -r 476a8d4f5c8b -r 637100169bc7 NEWS
--- a/NEWS	Fri May 14 22:43:24 2010 +0200
+++ b/NEWS	Fri May 14 23:16:33 2010 +0200
@@ -347,6 +347,31 @@
   Nat_Int_Bij.bij_nat_to_int_bij  ~> bij_int_encode
   Nat_Int_Bij.bij_int_to_nat_bij  ~> bij_int_decode
 
+* Nitpick:
+  - 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 "specification" and "ax_specification"
+    constructs.
+  - Added support for local definitions (for "function" and
+    "termination" proofs).
+  - Added support for term postprocessors.
+  - Optimized "Multiset.multiset" and "FinFun.finfun".
+  - Improved efficiency of "destroy_constrs" optimization.
+  - Fixed soundness bugs related to "destroy_constrs" optimization and
+    record getters.
+  - Fixed soundness bug related to higher-order constructors
+  - Improved precision of set constructs.
+  - Added cache to speed up repeated Kodkod invocations on the same
+    problems.
+  - Renamed "MiniSatJNI", "zChaffJNI", "BerkMinAlloy", and
+    "SAT4JLight" to "MiniSat_JNI", "zChaff_JNI", "BerkMin_Alloy", and
+    "SAT4J_Light".  INCOMPATIBILITY.
+  - Removed "skolemize", "uncurry", "sym_break", "flatten_prop",
+    "sharing_depth", and "show_skolems" options.  INCOMPATIBILITY.
+
 
 *** HOLCF ***