# HG changeset patch
# User nipkow
# Date 979129825 -3600
# Node ID e8a5340418b636244e50aaed61aac3c764937f3c
# Parent  140a1ed65665b0a776f20c54c1903bcd9f32d2cc
*** empty log message ***

diff -r 140a1ed65665 -r e8a5340418b6 NEWS
--- a/NEWS	Wed Jan 10 12:53:50 2001 +0100
+++ b/NEWS	Wed Jan 10 13:30:25 2001 +0100
@@ -12,9 +12,12 @@
 
 * HOL: infix "dvd" now has priority 50 rather than 70
   (because it is a relation)
-  infix ^^ has been renamed ```
+  infix ^^ has been renamed ``
+  infix `` has been renamed `
   "univalent" has been renamed "single_valued"
 
+* HOLCF: infix ` has been renamed $
+
 * Isar: 'obtain' no longer declares "that" fact as simp/intro;
 
 * Isar/HOL: method 'induct' now handles non-atomic goals; as a