NEWS
changeset 4361 c77a484e4f95
parent 4357 b852e2d2a39a
child 4370 162abcd128a1
     1.1 --- a/NEWS	Thu Dec 04 12:44:37 1997 +0100
     1.2 +++ b/NEWS	Thu Dec 04 12:50:02 1997 +0100
     1.3 @@ -155,9 +155,13 @@
     1.4  
     1.5    it be used with the new `split_asm_tac'.
     1.6  
     1.7 -* HOL/Nat: users are strongly encouraged to write "0 < n" rather than
     1.8 -  "n ~= 0". Theorems and proof tools have been modified towards this
     1.9 -  `standard'.
    1.10 +* HOL/Arithmetic:
    1.11 +  - `pred n' is automatically converted to `n-1'.
    1.12 +    Users are strongly encouraged not to use `pred' any longer,
    1.13 +    because it will disappear altogether at some point.
    1.14 +  - Users are strongly encouraged to write "0 < n" rather than
    1.15 +    "n ~= 0". Theorems and proof tools have been modified towards this
    1.16 +    `standard'.
    1.17  
    1.18  * HOL/Lists: the function "set_of_list" has been renamed "set"
    1.19    (and its theorems too);