*** empty log message ***
authornipkow
Fri, 05 Jan 2001 18:31:48 +0100
changeset 10793 4d6cf7702e3c
parent 10792 78dfc5904eea
child 10794 65d18005d802
*** empty log message ***
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