src/HOL/Library/README.html
changeset 26406 be5b78d95801
parent 15582 7219facb3fd0
child 28504 7ad7d7d6df47
     1.1 --- a/src/HOL/Library/README.html	Wed Mar 26 20:14:38 2008 +0100
     1.2 +++ b/src/HOL/Library/README.html	Wed Mar 26 21:05:58 2008 +0100
     1.3 @@ -59,7 +59,7 @@
     1.4  
     1.5  <p>
     1.6  
     1.7 -Note that syntax is <em>global</em>; qualified names loose syntax on
     1.8 +Note that syntax is <em>global</em>; qualified names lose syntax on
     1.9  output.  Do not use ``exotic'' symbols for syntax (such as
    1.10  <tt>\&lt;oplus&gt;</tt>), but leave these for user applications.
    1.11  
    1.12 @@ -111,7 +111,7 @@
    1.13  <dd>Isabelle is able to produce a high-quality LaTeX document from the
    1.14  theory sources, provided some minor issues are taken care of.  In
    1.15  particular, spacing and line breaks are directly taken from source
    1.16 -text.  Incidently, output looks very good common type-setting
    1.17 +text.  Incidentally, output looks very good if common type-setting
    1.18  conventions are observed: put a single space <em>after</em> each
    1.19  punctuation character ("<tt>,</tt>", "<tt>.</tt>", etc.), but none
    1.20  before it; do not extra spaces inside of parentheses, unless the