diff -r 0dfd34f0d33d -r b852e2d2a39a NEWS --- a/NEWS Wed Dec 03 17:25:43 1997 +0100 +++ b/NEWS Wed Dec 03 17:31:25 1997 +0100 @@ -155,6 +155,10 @@ it be used with the new `split_asm_tac'. +* HOL/Nat: users are strongly encouraged to write "0 < n" rather than + "n ~= 0". Theorems and proof tools have been modified towards this + `standard'. + * HOL/Lists: the function "set_of_list" has been renamed "set" (and its theorems too);