NEWS
changeset 60010 5fe58ca9cf40
parent 60009 bd1c342dbbce
child 60020 065ecea354d0
     1.1 --- a/NEWS	Sat Apr 11 12:40:03 2015 +0200
     1.2 +++ b/NEWS	Sat Apr 11 12:47:46 2015 +0200
     1.3 @@ -138,10 +138,10 @@
     1.4  * Command "class_deps" takes optional sort arguments to constrain then
     1.5  resulting class hierarchy.
     1.6  
     1.7 -* Lexical separation of signed and unsigend numerals: categories "num"
     1.8 -and "float" are unsigend.  INCOMPATIBILITY: subtle change in precedence
     1.9 -of numeral signs, particulary in expressions involving infix syntax like
    1.10 -"(- 1) ^ n".
    1.11 +* Lexical separation of signed and unsigned numerals: categories "num"
    1.12 +and "float" are unsigned. INCOMPATIBILITY: subtle change in precedence
    1.13 +of numeral signs, particularly in expressions involving infix syntax
    1.14 +like "(- 1) ^ n".
    1.15  
    1.16  * Old inner token category "xnum" has been discontinued.  Potential
    1.17  INCOMPATIBILITY for exotic syntax: may use mixfix grammar with "num"
    1.18 @@ -207,7 +207,7 @@
    1.19      INCOMPATIBILITY.
    1.20  
    1.21  * Nitpick:
    1.22 -  - Fixed soundness bug related to the strict and nonstrict subset
    1.23 +  - Fixed soundness bug related to the strict and non-strict subset
    1.24      operations.
    1.25  
    1.26  * Sledgehammer:
    1.27 @@ -216,7 +216,7 @@
    1.28    - Z3 is now always enabled by default, now that it is fully open
    1.29      source. The "z3_non_commercial" option is discontinued.
    1.30    - Minimization is now always enabled by default.
    1.31 -    Removed subcommand:
    1.32 +    Removed sub-command:
    1.33        min
    1.34    - Proof reconstruction, both one-liners and Isar, has been
    1.35      dramatically improved.
    1.36 @@ -364,12 +364,12 @@
    1.37  * HOL-Decision_Procs: New counterexample generator quickcheck
    1.38  [approximation] for inequalities of transcendental functions. Uses
    1.39  hardware floating point arithmetic to randomly discover potential
    1.40 -counterexamples. Counterexamples are certified with the 'approximation'
    1.41 +counterexamples. Counterexamples are certified with the "approximation"
    1.42  method. See HOL/Decision_Procs/ex/Approximation_Quickcheck_Ex.thy for
    1.43  examples.
    1.44  
    1.45  * HOL-Probability: Reworked measurability prover
    1.46 -  - applies destructor rules repeatetly
    1.47 +  - applies destructor rules repeatedly
    1.48    - removed application splitting (replaced by destructor rule)
    1.49    - added congruence rules to rewrite measure spaces under the sets
    1.50      projection
    1.51 @@ -384,7 +384,7 @@
    1.52  considered inaccessible, instead of accessible via the fully-qualified
    1.53  internal name. This mainly affects Name_Space.intern (and derivatives),
    1.54  which may produce an unexpected Long_Name.hidden prefix. Note that
    1.55 -contempory applications use the strict Name_Space.check (and
    1.56 +contemporary applications use the strict Name_Space.check (and
    1.57  derivatives) instead, which is not affected by the change. Potential
    1.58  INCOMPATIBILITY in rare applications of Name_Space.intern.
    1.59