1.1 --- a/NEWS	Fri May 14 22:43:24 2010 +0200
     1.2 +++ b/NEWS	Fri May 14 23:16:33 2010 +0200
     1.3 @@ -347,6 +347,31 @@
     1.4    Nat_Int_Bij.bij_nat_to_int_bij  ~> bij_int_encode
     1.5    Nat_Int_Bij.bij_int_to_nat_bij  ~> bij_int_decode
     1.6  
     1.7 +* Nitpick:
     1.8 +  - Added and implemented "binary_ints" and "bits" options.
     1.9 +  - Added "std" option and implemented support for nonstandard models.
    1.10 +  - Added and implemented "finitize" option to improve the precision
    1.11 +    of infinite datatypes based on a monotonicity analysis.
    1.12 +  - Added support for quotient types.
    1.13 +  - Added support for "specification" and "ax_specification"
    1.14 +    constructs.
    1.15 +  - Added support for local definitions (for "function" and
    1.16 +    "termination" proofs).
    1.17 +  - Added support for term postprocessors.
    1.18 +  - Optimized "Multiset.multiset" and "FinFun.finfun".
    1.19 +  - Improved efficiency of "destroy_constrs" optimization.
    1.20 +  - Fixed soundness bugs related to "destroy_constrs" optimization and
    1.21 +    record getters.
    1.22 +  - Fixed soundness bug related to higher-order constructors
    1.23 +  - Improved precision of set constructs.
    1.24 +  - Added cache to speed up repeated Kodkod invocations on the same
    1.25 +    problems.
    1.26 +  - Renamed "MiniSatJNI", "zChaffJNI", "BerkMinAlloy", and
    1.27 +    "SAT4JLight" to "MiniSat_JNI", "zChaff_JNI", "BerkMin_Alloy", and
    1.28 +    "SAT4J_Light".  INCOMPATIBILITY.
    1.29 +  - Removed "skolemize", "uncurry", "sym_break", "flatten_prop",
    1.30 +    "sharing_depth", and "show_skolems" options.  INCOMPATIBILITY.
    1.31 +
    1.32  
    1.33  *** HOLCF ***
    1.34