src/HOL/Library/README.html
changeset 26406 be5b78d95801
parent 15582 7219facb3fd0
child 28504 7ad7d7d6df47
equal deleted inserted replaced
26405:0cb6f2013e99 26406:be5b78d95801
    57 separate word constituents by underscores, as in <tt>foo_bar</tt> or
    57 separate word constituents by underscores, as in <tt>foo_bar</tt> or
    58 <tt>Foo_Bar</tt> (this looks best in LaTeX output).
    58 <tt>Foo_Bar</tt> (this looks best in LaTeX output).
    59 
    59 
    60 <p>
    60 <p>
    61 
    61 
    62 Note that syntax is <em>global</em>; qualified names loose syntax on
    62 Note that syntax is <em>global</em>; qualified names lose syntax on
    63 output.  Do not use ``exotic'' symbols for syntax (such as
    63 output.  Do not use ``exotic'' symbols for syntax (such as
    64 <tt>\&lt;oplus&gt;</tt>), but leave these for user applications.
    64 <tt>\&lt;oplus&gt;</tt>), but leave these for user applications.
    65 
    65 
    66 <dt><strong>Global context declarations</strong>
    66 <dt><strong>Global context declarations</strong>
    67 
    67 
   109 <dt><strong>Spacing</strong>
   109 <dt><strong>Spacing</strong>
   110 
   110 
   111 <dd>Isabelle is able to produce a high-quality LaTeX document from the
   111 <dd>Isabelle is able to produce a high-quality LaTeX document from the
   112 theory sources, provided some minor issues are taken care of.  In
   112 theory sources, provided some minor issues are taken care of.  In
   113 particular, spacing and line breaks are directly taken from source
   113 particular, spacing and line breaks are directly taken from source
   114 text.  Incidently, output looks very good common type-setting
   114 text.  Incidentally, output looks very good if common type-setting
   115 conventions are observed: put a single space <em>after</em> each
   115 conventions are observed: put a single space <em>after</em> each
   116 punctuation character ("<tt>,</tt>", "<tt>.</tt>", etc.), but none
   116 punctuation character ("<tt>,</tt>", "<tt>.</tt>", etc.), but none
   117 before it; do not extra spaces inside of parentheses, unless the
   117 before it; do not extra spaces inside of parentheses, unless the
   118 delimiters are composed of multiple symbols (as in
   118 delimiters are composed of multiple symbols (as in
   119 <tt>[|&nbsp;|]</tt>); do not attempt to simulate table markup with
   119 <tt>[|&nbsp;|]</tt>); do not attempt to simulate table markup with