# HG changeset patch
# User nipkow
# Date 881166685 -3600
# Node ID b852e2d2a39a6e6b4d0a874b512df1dcf95addbb
# Parent  0dfd34f0d33dab1d7b8d7d3492e82c0518dbda9f
n ~= 0 should become 0 < n

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