NEWS

 "isabelle jedit -m MODE".
 
 
 *** HOL ***
 
-* "declare [[code abort: …]]" replaces "code_abort …".
+* "declare [[code abort: ...]]" replaces "code_abort ...".
 INCOMPATIBILITY.
 
-* "declare [[code drop: …]]" drops all code equations associated
+* "declare [[code drop: ...]]" drops all code equations associated
 with the given constants.
 
 * Abolished slightly odd global lattice interpretation for min/max.
 
 Fact consolidations:

   * Canonical representation for minus one is "- 1".
   * Canonical representation for other negative numbers is "- (numeral _)".
   * 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.
 
 * Elimination of fact duplicates:
     equals_zero_I ~> minus_unique

 
 a) Arbitrary failing proof not involving "diff_def":
 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;
 or the brute way with
 "simp add: diff_conv_add_uminus del: add_uminus_conv_diff".