minor renovation of slightly odd and old README;
authorwenzelm
Fri Jun 27 15:24:56 2014 +0200 (2014-06-27)
changeset 57412b441f330078b
parent 57411 9444489766a1
child 57413 c14af83bd8db
minor renovation of slightly odd and old README;
src/HOL/Library/README.html
     1.1 --- a/src/HOL/Library/README.html	Fri Jun 27 11:30:42 2014 +0200
     1.2 +++ b/src/HOL/Library/README.html	Fri Jun 27 15:24:56 2014 +0200
     1.3 @@ -23,12 +23,6 @@
     1.4  
     1.5  <dl>
     1.6  
     1.7 -<dt><strong>Files</strong>
     1.8 -
     1.9 -<dd>Avoid unnecessary scattering of theories over several files.  Use
    1.10 -new-style theories only, as old ones tend to clutter the file space
    1.11 -with separate <tt>.thy</tt> and <tt>.ML</tt> files.
    1.12 -
    1.13  <dt><strong>Examples</strong>
    1.14  
    1.15  <dd>Theories should be as ``generic'' as is sensible.  Unused (or
    1.16 @@ -54,12 +48,6 @@
    1.17  separate word constituents by underscores, as in <tt>foo_bar</tt> or
    1.18  <tt>Foo_Bar</tt> (this looks best in LaTeX output).
    1.19  
    1.20 -<p>
    1.21 -
    1.22 -Note that syntax is <em>global</em>; qualified names lose syntax on
    1.23 -output.  Do not use ``exotic'' symbols for syntax (such as
    1.24 -<tt>\&lt;oplus&gt;</tt>), but leave these for user applications.
    1.25 -
    1.26  <dt><strong>Global context declarations</strong>
    1.27  
    1.28  <dd>Only items introduced in the present theory should be declared
    1.29 @@ -67,42 +55,6 @@
    1.30  rules from parent theories may result in strange behavior later,
    1.31  depending on the user's arrangement of import lists.
    1.32  
    1.33 -<dt><strong>Mathematical symbols</strong>
    1.34 -
    1.35 -<dd>Non-ASCII symbols should be used as appropriate, with some
    1.36 -care. In particular, avoid unreadable arrows: <tt>==&gt;</tt> should
    1.37 -be preferred over <tt>\&lt;Longrightarrow&gt;</tt>. Use <tt>isabelle
    1.38 -unsymbolize</tt> to clean up the sources.
    1.39 -
    1.40 -<p>
    1.41 -
    1.42 -The following ASCII symbols of HOL should be generally avoided:
    1.43 -<tt>@</tt>, <tt>!</tt>, <tt>?</tt>, <tt>?!</tt>, <tt>%</tt>, better
    1.44 -use <tt>SOME</tt>, <tt>ALL</tt> (or <tt>\&lt;forall&gt;</tt>),
    1.45 -<tt>EX</tt> (or <tt>\&lt;exists&gt;</tt>), <tt>EX!</tt> (or
    1.46 -<tt>\&lt;exists&gt;!</tt>), <tt>\&lt;lambda&gt;</tt>, respectively.
    1.47 -Note that bracket notation <tt>[|&nbsp;|]</tt> looks bad in LaTeX
    1.48 -output.
    1.49 -
    1.50 -<p>
    1.51 -
    1.52 -Some additional mathematical symbols are quite suitable for both
    1.53 -readable sources and the output document:
    1.54 -<tt>\&lt;Inter&gt;</tt>,
    1.55 -<tt>\&lt;Union&gt;</tt>,
    1.56 -<tt>\&lt;and&gt;</tt>,
    1.57 -<tt>\&lt;in&gt;</tt>,
    1.58 -<tt>\&lt;inter&gt;</tt>,
    1.59 -<tt>\&lt;le&gt;</tt>,
    1.60 -<tt>\&lt;not&gt;</tt>,
    1.61 -<tt>\&lt;noteq&gt;</tt>,
    1.62 -<tt>\&lt;notin&gt;</tt>,
    1.63 -<tt>\&lt;or&gt;</tt>,
    1.64 -<tt>\&lt;subset&gt;</tt>,
    1.65 -<tt>\&lt;subseteq&gt;</tt>,
    1.66 -<tt>\&lt;times&gt;</tt>,
    1.67 -<tt>\&lt;union&gt;</tt>.
    1.68 -
    1.69  <dt><strong>Spacing</strong>
    1.70  
    1.71  <dd>Isabelle is able to produce a high-quality LaTeX document from the
    1.72 @@ -111,10 +63,8 @@
    1.73  text.  Incidentally, output looks very good if common type-setting
    1.74  conventions are observed: put a single space <em>after</em> each
    1.75  punctuation character ("<tt>,</tt>", "<tt>.</tt>", etc.), but none
    1.76 -before it; do not extra spaces inside of parentheses, unless the
    1.77 -delimiters are composed of multiple symbols (as in
    1.78 -<tt>[|&nbsp;|]</tt>); do not attempt to simulate table markup with
    1.79 -spaces, avoid ``hanging'' indentations.
    1.80 +before it; do not extra spaces inside of parentheses; do not attempt
    1.81 +to simulate table markup with spaces, avoid ``hanging'' indentations.
    1.82  
    1.83  </dl>
    1.84