NEWS
 changeset 54893 4061ec8adb1c parent 54890 cb892d835803 child 55001 f26a7f06266d
```--- a/NEWS	Wed Jan 01 01:05:48 2014 +0100
+++ b/NEWS	Wed Jan 01 12:57:26 2014 +0100
@@ -33,10 +33,10 @@

*** HOL ***

-* "declare [[code abort: …]]" replaces "code_abort …".
-INCOMPATIBILITY.
-
-* "declare [[code drop: …]]" drops all code equations associated
+* "declare [[code abort: ...]]" replaces "code_abort ...".
+INCOMPATIBILITY.
+
+* "declare [[code drop: ...]]" drops all code equations associated
with the given constants.

* Abolished slightly odd global lattice interpretation for min/max.
@@ -121,7 +121,7 @@
* When devising rule sets for number calculation, consider the
following canonical cases: 0, 1, numeral _, - 1, - numeral _.
* HOLogic.dest_number also recognizes numerals in non-canonical forms
-    like "numeral One", "- numeral One", "- 0" and even "- … - _".
+    like "numeral One", "- numeral One", "- 0" and even "- ... - _".
* Syntax for negative numerals is mere input syntax.
INCOMPATBILITY.

@@ -155,7 +155,7 @@
Consider simplification with algebra_simps or field_simps.

b) Lifting rules from addition to subtraction:
-Try with "using <rule for addition> of [… "- _" …]" by simp".
+Try with "using <rule for addition> of [... "- _" ...]" by simp".

c) Simplification with "diff_def": just drop "diff_def".
Consider simplification with algebra_simps or field_simps;```