--- a/src/Tools/WWW_Find/etc/symbols	Sat Feb 22 15:07:33 2014 +0100
+++ b/src/Tools/WWW_Find/etc/symbols	Sat Feb 22 16:11:23 2014 +0100
@@ -1,4 +1,4 @@
-# Default interpretation of some Isabelle symbols
+# Default interpretation of some Isabelle symbols (outdated version for WWW_Find)
 
 \<zero>                 code: 0x01d7ec  group: digit
 \<one>                  code: 0x01d7ed  group: digit