changeset 28504 | 7ad7d7d6df47 |
parent 26406 | be5b78d95801 |
child 31975 | 366ad09d39ef |
--- 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>==></tt> should -be preferred over <tt>\<Longrightarrow></tt>. Use <tt>isatool +be preferred over <tt>\<Longrightarrow></tt>. Use <tt>isabelle unsymbolize</tt> to clean up the sources. <p>