author | wenzelm |
Sat, 22 Feb 2014 16:11:23 +0100 (2014-02-22) | |
changeset 55667 | a99f9beba83a |
parent 55666 | cc350eb1087e |
child 55668 | 6e97c1766500 |
--- 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