n ~= 0 should become 0 < n

--- 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);