src/HOL/Library/README.html
author webertj
Mon Mar 07 19:17:07 2005 +0100 (2005-03-07)
changeset 15582 7219facb3fd0
parent 15283 f21466450330
child 26406 be5b78d95801
permissions -rw-r--r--
HTML 4.01 Transitional conformity
     1 <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
     2 
     3 <!-- $Id$ -->
     4 
     5 <html>
     6 
     7 <head>
     8   <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
     9   <title>HOL-Library/README</title>
    10 </head>
    11 
    12 <body>
    13 
    14 <h1>HOL-Library: supplemental theories for main Isabelle/HOL</h1>
    15 
    16 This is a collection of generic theories that may be used together
    17 with main Isabelle/HOL.  Note that theory loader path already includes
    18 this directory by default.
    19 
    20 <p>
    21 
    22 Addition of new theories should be done with some care, as the
    23 ``module system'' of Isabelle is rather simplistic.  The following
    24 guidelines may be helpful to achieve maximum re-usability and minimum
    25 clashes with existing developments.
    26 
    27 <dl>
    28 
    29 <dt><strong>Files</strong>
    30 
    31 <dd>Avoid unnecessary scattering of theories over several files.  Use
    32 new-style theories only, as old ones tend to clutter the file space
    33 with separate <tt>.thy</tt> and <tt>.ML</tt> files.
    34 
    35 <dt><strong>Examples</strong>
    36 
    37 <dd>Theories should be as ``generic'' as is sensible.  Unused (or
    38 rather unusable?) theories should be avoided; common applications
    39 should actually refer to the present theory.  Small example uses may
    40 be included in the library as well, but should be put in a separate
    41 theory, such as <tt>Foobar</tt> accompanied by
    42 <tt>Foobar_Examples</tt>.
    43 
    44 <dt><strong>Theory names</strong>
    45 
    46 <dd>The theory loader name space is <em>flat</em>, so use sufficiently
    47 long and descriptive names to reduce the danger of clashes with the
    48 user's own theories.  The convention for theory names is as follows:
    49 <tt>Foobar_Doobar</tt> (this looks best in LaTeX output).
    50 
    51 <dt><strong>Names of logical items</strong>
    52 
    53 <dd>There are separate hierarchically structured name spaces for
    54 types, constants, theorems etc.  Nevertheless, some care should be
    55 taken, as the name spaces are always ``open''.  Use adequate names;
    56 avoid unreadable abbreviations.  The general naming convention is to
    57 separate word constituents by underscores, as in <tt>foo_bar</tt> or
    58 <tt>Foo_Bar</tt> (this looks best in LaTeX output).
    59 
    60 <p>
    61 
    62 Note that syntax is <em>global</em>; qualified names loose syntax on
    63 output.  Do not use ``exotic'' symbols for syntax (such as
    64 <tt>\&lt;oplus&gt;</tt>), but leave these for user applications.
    65 
    66 <dt><strong>Global context declarations</strong>
    67 
    68 <dd>Only items introduced in the present theory should be declared
    69 globally (e.g. as Simplifier rules).  Note that adding and deleting
    70 rules from parent theories may result in strange behavior later,
    71 depending on the user's arrangement of import lists.
    72 
    73 <dt><strong>Mathematical symbols</strong>
    74 
    75 <dd>Non-ASCII symbols should be used as appropriate, with some
    76 care. In particular, avoid unreadable arrows: <tt>==&gt;</tt> should
    77 be preferred over <tt>\&lt;Longrightarrow&gt;</tt>. Use <tt>isatool
    78 unsymbolize</tt> to clean up the sources.
    79 
    80 <p>
    81 
    82 The following ASCII symbols of HOL should be generally avoided:
    83 <tt>@</tt>, <tt>!</tt>, <tt>?</tt>, <tt>?!</tt>, <tt>%</tt>, better
    84 use <tt>SOME</tt>, <tt>ALL</tt> (or <tt>\&lt;forall&gt;</tt>),
    85 <tt>EX</tt> (or <tt>\&lt;exists&gt;</tt>), <tt>EX!</tt> (or
    86 <tt>\&lt;exists&gt;!</tt>), <tt>\&lt;lambda&gt;</tt>, respectively.
    87 Note that bracket notation <tt>[|&nbsp;|]</tt> looks bad in LaTeX
    88 output.
    89 
    90 <p>
    91 
    92 Some additional mathematical symbols are quite suitable for both
    93 readable sources and the output document:
    94 <tt>\&lt;Inter&gt;</tt>,
    95 <tt>\&lt;Union&gt;</tt>,
    96 <tt>\&lt;and&gt;</tt>,
    97 <tt>\&lt;in&gt;</tt>,
    98 <tt>\&lt;inter&gt;</tt>,
    99 <tt>\&lt;le&gt;</tt>,
   100 <tt>\&lt;not&gt;</tt>,
   101 <tt>\&lt;noteq&gt;</tt>,
   102 <tt>\&lt;notin&gt;</tt>,
   103 <tt>\&lt;or&gt;</tt>,
   104 <tt>\&lt;subset&gt;</tt>,
   105 <tt>\&lt;subseteq&gt;</tt>,
   106 <tt>\&lt;times&gt;</tt>,
   107 <tt>\&lt;union&gt;</tt>.
   108 
   109 <dt><strong>Spacing</strong>
   110 
   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
   113 particular, spacing and line breaks are directly taken from source
   114 text.  Incidently, output looks very good common type-setting
   115 conventions are observed: put a single space <em>after</em> each
   116 punctuation character ("<tt>,</tt>", "<tt>.</tt>", etc.), but none
   117 before it; do not extra spaces inside of parentheses, unless the
   118 delimiters are composed of multiple symbols (as in
   119 <tt>[|&nbsp;|]</tt>); do not attempt to simulate table markup with
   120 spaces, avoid ``hanging'' indentations.
   121 
   122 </dl>
   123 
   124 </body>
   125 </html>