summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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