# HG changeset patch
# User nipkow
# Date 978773779 -3600
# Node ID ea69ee7e117bef170eeda5bf91341cd3b0828b3e
# Parent  0a1446ff6aff303430b2326da520176413a76a10
*** empty log message ***

diff -r 0a1446ff6aff -r ea69ee7e117b NEWS
--- a/NEWS	Fri Jan 05 18:49:16 2001 +0100
+++ b/NEWS	Sat Jan 06 10:36:19 2001 +0100
@@ -11,7 +11,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)
+  (because it is a relation)
+  infix ^^ has been renamed ```
+  "univalent" has been renamed "single_valued"
 
 * Isar: 'obtain' no longer declares "that" fact as simp/intro;