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