# HG changeset patch
# User nipkow
# Date 979213788 -3600
# Node ID 5af3906edec837e466798525d4cc5f557e8075b7
# Parent  bda1701848cd457faabaad3215e7f759c6289a5c
*** empty log message ***

diff -r bda1701848cd -r 5af3906edec8 NEWS
--- a/NEWS	Thu Jan 11 12:12:01 2001 +0100
+++ b/NEWS	Thu Jan 11 12:49:48 2001 +0100
@@ -1,4 +1,3 @@
-
 Isabelle NEWS -- history user-relevant changes
 ==============================================
 
@@ -15,7 +14,7 @@
 relation); infix "^^" has been renamed "``"; infix "``" has been
 renamed "`"; "univalent" has been renamed "single_valued";
 
-* HOLCF: infix "`" has been renamed "$";
+* HOLCF: infix "`" has been renamed "$"; the symbol syntax is \<cdot>;
 
 * Isar: 'obtain' no longer declares "that" fact as simp/intro;