# HG changeset patch
# User huffman
# Date 1206561958 -3600
# Node ID be5b78d9580145622b6675e8c4db6719c7ff03d1
# Parent  0cb6f2013e99500a2e79e4055da806717b5149ad
fix spelling errors

diff -r 0cb6f2013e99 -r be5b78d95801 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