diff -r a30b7169fdd1 -r 7ad7d7d6df47 src/HOL/Library/README.html --- a/src/HOL/Library/README.html Sat Oct 04 16:19:49 2008 +0200 +++ b/src/HOL/Library/README.html Sat Oct 04 17:40:56 2008 +0200 @@ -74,7 +74,7 @@
Non-ASCII symbols should be used as appropriate, with some care. In particular, avoid unreadable arrows: ==> should -be preferred over \<Longrightarrow>. Use isatool +be preferred over \<Longrightarrow>. Use isabelle unsymbolize to clean up the sources.