src/HOL/Library/README.html

--- 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>\&lt;oplus&gt;</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