tuned;
authorwenzelm
Fri Oct 20 13:15:26 2000 +0200 (2000-10-20)
changeset 10282b7d96e94796f
parent 10281 9554ce1c2e54
child 10283 ff003e2b790c
tuned;
src/HOL/Library/README.html
     1.1 --- a/src/HOL/Library/README.html	Fri Oct 20 08:46:41 2000 +0200
     1.2 +++ b/src/HOL/Library/README.html	Fri Oct 20 13:15:26 2000 +0200
     1.3 @@ -22,6 +22,7 @@
     1.4  <dl>
     1.5  
     1.6  <dt><strong>Files</strong>
     1.7 +
     1.8  <dd>Avoid unnecessary scattering of theories over several files.  Use
     1.9  new-style theories only, as old ones tend to clutter the file space
    1.10  with separate <tt>.thy</tt> and <tt>.ML</tt> files.
    1.11 @@ -29,19 +30,21 @@
    1.12  <dt><strong>Examples</strong>
    1.13  
    1.14  <dd>Theories should be as ``generic'' as is sensible.  Unused (or
    1.15 -rather unusable?) standalone theories should be avoided; common
    1.16 -applications should actually refer to the present theory.  Small
    1.17 -example uses may be included as well, but should be put in a separate
    1.18 +rather unusable?) theories should be avoided; common applications
    1.19 +should actually refer to the present theory.  Small example uses may
    1.20 +be included in the library as well, but should be put in a separate
    1.21  theory, such as <tt>Foobar</tt> accompanied by
    1.22  <tt>Foobar_Examples</tt>.
    1.23  
    1.24  <dt><strong>Theory names</strong>
    1.25 +
    1.26  <dd>The theory loader name space is <em>flat</em>, so use sufficiently
    1.27  long and descriptive names to reduce the danger of clashes with the
    1.28  user's own theories.  The convention for theory names is as follows:
    1.29  <tt>Foobar_Doobar</tt> (this looks best in LaTeX output).
    1.30  
    1.31  <dt><strong>Names of logical items</strong>
    1.32 +
    1.33  <dd>There are separate hierarchically structured name spaces for
    1.34  types, constants, theorems etc.  Nevertheless, some care should be
    1.35  taken, as the name spaces are always ``open''.  Use adequate names;
    1.36 @@ -56,16 +59,18 @@
    1.37  <tt>\&lt;oplus&gt;</tt>), but leave these for user applications.
    1.38  
    1.39  <dt><strong>Global context declarations</strong>
    1.40 +
    1.41  <dd>Only items introduced in the present theory should be declared
    1.42 -globally (e.g. as Simplifier rules).  Note that adding / deleting
    1.43 -rules stemming from parent theories may result in strange behavior
    1.44 -later, depending on the user's arrangement of import lists.
    1.45 +globally (e.g. as Simplifier rules).  Note that adding and deleting
    1.46 +rules from parent theories may result in strange behavior later,
    1.47 +depending on the user's arrangement of import lists.
    1.48  
    1.49  <dt><strong>Mathematical symbols</strong>
    1.50 -<dd>Non-ASCII symbols should be used with some care. In particular,
    1.51 -avoid unreadable arrows: <tt>==&gt;</tt> should be preferred over
    1.52 -<tt>\&lt;Longrightarrow&gt;</tt>. Use <tt>isatool unsymbolize</tt> to
    1.53 -clean up the sources.
    1.54 +
    1.55 +<dd>Non-ASCII symbols should be used as appropriate, with some
    1.56 +care. In particular, avoid unreadable arrows: <tt>==&gt;</tt> should
    1.57 +be preferred over <tt>\&lt;Longrightarrow&gt;</tt>. Use <tt>isatool
    1.58 +unsymbolize</tt> to clean up the sources.
    1.59  
    1.60  <p>
    1.61  
    1.62 @@ -73,14 +78,14 @@
    1.63  <tt>@</tt>, <tt>!</tt>, <tt>?</tt>, <tt>?!</tt>, <tt>%</tt>, better
    1.64  use <tt>SOME</tt>, <tt>ALL</tt> (or <tt>\&lt;forall&gt;</tt>),
    1.65  <tt>EX</tt> (or <tt>\&lt;exists&gt;</tt>), <tt>EX!</tt> (or
    1.66 -<tt>\&lt;exists;&gt!</tt>), <tt>\&lt;lambda&gt;</tt>, respectively.
    1.67 +<tt>\&lt;exists&gt;!</tt>), <tt>\&lt;lambda&gt;</tt>, respectively.
    1.68  Note that bracket notation <tt>[|&nbsp;|]</tt> looks bad in LaTeX
    1.69  output.
    1.70  
    1.71  <p>
    1.72  
    1.73  Some additional mathematical symbols are quite suitable for both
    1.74 -readable sources and output document:
    1.75 +readable sources and the output document:
    1.76  <tt>\&lt;Inter&gt;</tt>,
    1.77  <tt>\&lt;Union&gt;</tt>,
    1.78  <tt>\&lt;and&gt;</tt>,