--- a/src/HOL/Library/README.html Wed Mar 26 20:14:38 2008 +0100
+++ b/src/HOL/Library/README.html Wed Mar 26 21:05:58 2008 +0100
@@ -59,7 +59,7 @@
<p>
-Note that syntax is <em>global</em>; qualified names loose syntax on
+Note that syntax is <em>global</em>; qualified names lose syntax on
output. Do not use ``exotic'' symbols for syntax (such as
<tt>\<oplus></tt>), but leave these for user applications.
@@ -111,7 +111,7 @@
<dd>Isabelle is able to produce a high-quality LaTeX document from the
theory sources, provided some minor issues are taken care of. In
particular, spacing and line breaks are directly taken from source
-text. Incidently, output looks very good common type-setting
+text. Incidentally, output looks very good if common type-setting
conventions are observed: put a single space <em>after</em> each
punctuation character ("<tt>,</tt>", "<tt>.</tt>", etc.), but none
before it; do not extra spaces inside of parentheses, unless the