# HG changeset patch
# User nipkow
# Date 978715908 -3600
# Node ID 4d6cf7702e3c391be765a601a2e641f1a79517d2
# Parent  78dfc5904eea957fa7f55ec29e0ca79aee929c67
*** empty log message ***

diff -r 78dfc5904eea -r 4d6cf7702e3c NEWS
--- a/NEWS	Fri Jan 05 18:16:01 2001 +0100
+++ b/NEWS	Fri Jan 05 18:31:48 2001 +0100
@@ -1,4 +1,3 @@
-
 Isabelle NEWS -- history user-relevant changes
 ==============================================
 
@@ -11,6 +10,9 @@
 
 * HOL: contrapos, contrapos2 renamed to contrapos_nn, contrapos_pp;
 
+* HOL: infix "dvd" now has priority 50 rather than 70
+ (because it is a relation)
+
 * Isar: 'obtain' no longer declares "that" fact as simp/intro;
 
 * Isar/HOL: method 'induct' now handles non-atomic goals; as a