NEWS
changeset 55889 6bfbec3dff62
parent 55875 6478b12b7297
child 55931 62156e694f3d
child 55963 a8ebafaa56d4
     1.1 --- a/NEWS	Mon Mar 03 22:33:22 2014 +0100
     1.2 +++ b/NEWS	Mon Mar 03 22:33:22 2014 +0100
     1.3 @@ -367,6 +367,11 @@
     1.4  * Nitpick:
     1.5    - Fixed soundness bug whereby mutually recursive datatypes could take
     1.6      infinite values.
     1.7 +  - Fixed soundness bug with low-level number functions such as "Abs_Integ" and
     1.8 +    "Rep_Integ".
     1.9 +  - Removed "std" option.
    1.10 +  - Renamed "show_datatypes" to "show_types" and "hide_datatypes" to
    1.11 +    "hide_types".
    1.12  
    1.13  * HOL-Multivariate_Analysis:
    1.14    - type class ordered_real_vector for ordered vector spaces
    1.15 @@ -812,16 +817,16 @@
    1.16  INCOMPATIBILITY.
    1.17  
    1.18  * Nitpick:
    1.19 -  - Added option "spy"
    1.20 -  - Reduce incidence of "too high arity" errors
    1.21 +  - Added option "spy".
    1.22 +  - Reduce incidence of "too high arity" errors.
    1.23  
    1.24  * Sledgehammer:
    1.25    - Renamed option:
    1.26        isar_shrink ~> isar_compress
    1.27      INCOMPATIBILITY.
    1.28 -  - Added options "isar_try0", "spy"
    1.29 -  - Better support for "isar_proofs"
    1.30 -  - MaSh has been fined-tuned and now runs as a local server
    1.31 +  - Added options "isar_try0", "spy".
    1.32 +  - Better support for "isar_proofs".
    1.33 +  - MaSh has been fined-tuned and now runs as a local server.
    1.34  
    1.35  * Improved support for ad hoc overloading of constants (see also
    1.36  isar-ref manual and ~~/src/HOL/ex/Adhoc_Overloading_Examples.thy).