avoid unicode text, which causes problems when recoding symbols (e.g. via UTF8-Isabelle in Isabelle/jEdit);
authorwenzelm
Wed Jan 01 12:57:26 2014 +0100 (2014-01-01)
changeset 548934061ec8adb1c
parent 54890 cb892d835803
child 54894 cb9d981fa9a0
avoid unicode text, which causes problems when recoding symbols (e.g. via UTF8-Isabelle in Isabelle/jEdit);
NEWS
     1.1 --- a/NEWS	Wed Jan 01 01:05:48 2014 +0100
     1.2 +++ b/NEWS	Wed Jan 01 12:57:26 2014 +0100
     1.3 @@ -33,10 +33,10 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 -* "declare [[code abort: …]]" replaces "code_abort …".
     1.8 -INCOMPATIBILITY.
     1.9 -
    1.10 -* "declare [[code drop: …]]" drops all code equations associated
    1.11 +* "declare [[code abort: ...]]" replaces "code_abort ...".
    1.12 +INCOMPATIBILITY.
    1.13 +
    1.14 +* "declare [[code drop: ...]]" drops all code equations associated
    1.15  with the given constants.
    1.16  
    1.17  * Abolished slightly odd global lattice interpretation for min/max.
    1.18 @@ -121,7 +121,7 @@
    1.19    * When devising rule sets for number calculation, consider the
    1.20      following canonical cases: 0, 1, numeral _, - 1, - numeral _.
    1.21    * HOLogic.dest_number also recognizes numerals in non-canonical forms
    1.22 -    like "numeral One", "- numeral One", "- 0" and even "- … - _".
    1.23 +    like "numeral One", "- numeral One", "- 0" and even "- ... - _".
    1.24    * Syntax for negative numerals is mere input syntax.
    1.25  INCOMPATBILITY.
    1.26  
    1.27 @@ -155,7 +155,7 @@
    1.28  Consider simplification with algebra_simps or field_simps.
    1.29  
    1.30  b) Lifting rules from addition to subtraction:
    1.31 -Try with "using <rule for addition> of [… "- _" …]" by simp".
    1.32 +Try with "using <rule for addition> of [... "- _" ...]" by simp".
    1.33  
    1.34  c) Simplification with "diff_def": just drop "diff_def".
    1.35  Consider simplification with algebra_simps or field_simps;