src/HOL/Library/README.html
changeset 10253 73b46b18c348
child 10282 b7d96e94796f
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Library/README.html	Wed Oct 18 23:31:16 2000 +0200
     1.3 @@ -0,0 +1,114 @@
     1.4 +<html>
     1.5 +
     1.6 +<!-- $Id$ -->
     1.7 +
     1.8 +<head><title>HOL-Library/README</title></head>
     1.9 +
    1.10 +<body>
    1.11 +
    1.12 +<h1>HOL-Library: supplemental theories for main Isabelle/HOL</h1>
    1.13 +
    1.14 +This is a collection of generic theories that may be used together
    1.15 +with main Isabelle/HOL.  Note that theory loader path already includes
    1.16 +this directory by default.
    1.17 +
    1.18 +<p>
    1.19 +
    1.20 +Addition of new theories should be done with some care, as the
    1.21 +``module system'' of Isabelle is rather simplistic.  The following
    1.22 +guidelines may be helpful to achieve maximum re-usability and minimum
    1.23 +clashes with existing developments.
    1.24 +
    1.25 +<dl>
    1.26 +
    1.27 +<dt><strong>Files</strong>
    1.28 +<dd>Avoid unnecessary scattering of theories over several files.  Use
    1.29 +new-style theories only, as old ones tend to clutter the file space
    1.30 +with separate <tt>.thy</tt> and <tt>.ML</tt> files.
    1.31 +
    1.32 +<dt><strong>Examples</strong>
    1.33 +
    1.34 +<dd>Theories should be as ``generic'' as is sensible.  Unused (or
    1.35 +rather unusable?) standalone theories should be avoided; common
    1.36 +applications should actually refer to the present theory.  Small
    1.37 +example uses may be included as well, but should be put in a separate
    1.38 +theory, such as <tt>Foobar</tt> accompanied by
    1.39 +<tt>Foobar_Examples</tt>.
    1.40 +
    1.41 +<dt><strong>Theory names</strong>
    1.42 +<dd>The theory loader name space is <em>flat</em>, so use sufficiently
    1.43 +long and descriptive names to reduce the danger of clashes with the
    1.44 +user's own theories.  The convention for theory names is as follows:
    1.45 +<tt>Foobar_Doobar</tt> (this looks best in LaTeX output).
    1.46 +
    1.47 +<dt><strong>Names of logical items</strong>
    1.48 +<dd>There are separate hierarchically structured name spaces for
    1.49 +types, constants, theorems etc.  Nevertheless, some care should be
    1.50 +taken, as the name spaces are always ``open''.  Use adequate names;
    1.51 +avoid unreadable abbreviations.  The general naming convention is to
    1.52 +separate word constituents by underscores, as in <tt>foo_bar</tt> or
    1.53 +<tt>Foo_Bar</tt> (this looks best in LaTeX output).
    1.54 +
    1.55 +<p>
    1.56 +
    1.57 +Note that syntax is <em>global</em>; qualified names loose syntax on
    1.58 +output.  Do not use ``exotic'' symbols for syntax (such as
    1.59 +<tt>\&lt;oplus&gt;</tt>), but leave these for user applications.
    1.60 +
    1.61 +<dt><strong>Global context declarations</strong>
    1.62 +<dd>Only items introduced in the present theory should be declared
    1.63 +globally (e.g. as Simplifier rules).  Note that adding / deleting
    1.64 +rules stemming from parent theories may result in strange behavior
    1.65 +later, depending on the user's arrangement of import lists.
    1.66 +
    1.67 +<dt><strong>Mathematical symbols</strong>
    1.68 +<dd>Non-ASCII symbols should be used with some care. In particular,
    1.69 +avoid unreadable arrows: <tt>==&gt;</tt> should be preferred over
    1.70 +<tt>\&lt;Longrightarrow&gt;</tt>. Use <tt>isatool unsymbolize</tt> to
    1.71 +clean up the sources.
    1.72 +
    1.73 +<p>
    1.74 +
    1.75 +The following ASCII symbols of HOL should be generally avoided:
    1.76 +<tt>@</tt>, <tt>!</tt>, <tt>?</tt>, <tt>?!</tt>, <tt>%</tt>, better
    1.77 +use <tt>SOME</tt>, <tt>ALL</tt> (or <tt>\&lt;forall&gt;</tt>),
    1.78 +<tt>EX</tt> (or <tt>\&lt;exists&gt;</tt>), <tt>EX!</tt> (or
    1.79 +<tt>\&lt;exists;&gt!</tt>), <tt>\&lt;lambda&gt;</tt>, respectively.
    1.80 +Note that bracket notation <tt>[|&nbsp;|]</tt> looks bad in LaTeX
    1.81 +output.
    1.82 +
    1.83 +<p>
    1.84 +
    1.85 +Some additional mathematical symbols are quite suitable for both
    1.86 +readable sources and output document:
    1.87 +<tt>\&lt;Inter&gt;</tt>,
    1.88 +<tt>\&lt;Union&gt;</tt>,
    1.89 +<tt>\&lt;and&gt;</tt>,
    1.90 +<tt>\&lt;in&gt;</tt>,
    1.91 +<tt>\&lt;inter&gt;</tt>,
    1.92 +<tt>\&lt;not&gt;</tt>,
    1.93 +<tt>\&lt;noteq&gt;</tt>,
    1.94 +<tt>\&lt;notin&gt;</tt>,
    1.95 +<tt>\&lt;or&gt;</tt>,
    1.96 +<tt>\&lt;subset&gt;</tt>,
    1.97 +<tt>\&lt;subseteq&gt;</tt>,
    1.98 +<tt>\&lt;times&gt;</tt>,
    1.99 +<tt>\&lt;union&gt;</tt>.
   1.100 +
   1.101 +<dt><strong>Spacing</strong>
   1.102 +
   1.103 +<dd>Isabelle is able to produce a high-quality LaTeX document from the
   1.104 +theory sources, provided some minor issues are taken care of.  In
   1.105 +particular, spacing and line breaks are directly taken from source
   1.106 +text.  Incidently, output looks very good common type-setting
   1.107 +conventions are observed: put a single space <em>after</em> each
   1.108 +punctuation character ("<tt>,</tt>", "<tt>.</tt>", etc.), but none
   1.109 +before it; do not extra spaces inside of parentheses, unless the
   1.110 +delimiters are composed of multiple symbols (as in
   1.111 +<tt>[|&nbsp;|]</tt>); do not attempt to simulate table markup with
   1.112 +spaces, avoid ``hanging'' indentations.
   1.113 +
   1.114 +</dl>
   1.115 +
   1.116 +</body>
   1.117 +</html>