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 @@
 
 <dd>Non-ASCII symbols should be used as appropriate, with some
 care. In particular, avoid unreadable arrows: <tt>==&gt;</tt> should
-be preferred over <tt>\&lt;Longrightarrow&gt;</tt>. Use <tt>isatool
+be preferred over <tt>\&lt;Longrightarrow&gt;</tt>. Use <tt>isabelle
 unsymbolize</tt> to clean up the sources.
 
 <p>