src/HOL/Library/README.html
author wenzelm
Mon Dec 28 17:43:30 2015 +0100 (2015-12-28)
changeset 61952 546958347e05
parent 57412 b441f330078b
permissions -rw-r--r--
prefer symbols for "Union", "Inter";
     1 <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
     2 
     3 <html>
     4 
     5 <head>
     6   <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
     7   <title>HOL-Library/README</title>
     8 </head>
     9 
    10 <body>
    11 
    12 <h1>HOL-Library: supplemental theories for main Isabelle/HOL</h1>
    13 
    14 This is a collection of generic theories that may be used together
    15 with main Isabelle/HOL.
    16 
    17 <p>
    18 
    19 Addition of new theories should be done with some care, as the
    20 ``module system'' of Isabelle is rather simplistic.  The following
    21 guidelines may be helpful to achieve maximum re-usability and minimum
    22 clashes with existing developments.
    23 
    24 <dl>
    25 
    26 <dt><strong>Examples</strong>
    27 
    28 <dd>Theories should be as ``generic'' as is sensible.  Unused (or
    29 rather unusable?) theories should be avoided; common applications
    30 should actually refer to the present theory.  Small example uses may
    31 be included in the library as well, but should be put in a separate
    32 theory, such as <tt>Foobar</tt> accompanied by
    33 <tt>Foobar_Examples</tt>.
    34 
    35 <dt><strong>Theory names</strong>
    36 
    37 <dd>The theory loader name space is <em>flat</em>, so use sufficiently
    38 long and descriptive names to reduce the danger of clashes with the
    39 user's own theories.  The convention for theory names is as follows:
    40 <tt>Foobar_Doobar</tt> (this looks best in LaTeX output).
    41 
    42 <dt><strong>Names of logical items</strong>
    43 
    44 <dd>There are separate hierarchically structured name spaces for
    45 types, constants, theorems etc.  Nevertheless, some care should be
    46 taken, as the name spaces are always ``open''.  Use adequate names;
    47 avoid unreadable abbreviations.  The general naming convention is to
    48 separate word constituents by underscores, as in <tt>foo_bar</tt> or
    49 <tt>Foo_Bar</tt> (this looks best in LaTeX output).
    50 
    51 <dt><strong>Global context declarations</strong>
    52 
    53 <dd>Only items introduced in the present theory should be declared
    54 globally (e.g. as Simplifier rules).  Note that adding and deleting
    55 rules from parent theories may result in strange behavior later,
    56 depending on the user's arrangement of import lists.
    57 
    58 <dt><strong>Spacing</strong>
    59 
    60 <dd>Isabelle is able to produce a high-quality LaTeX document from the
    61 theory sources, provided some minor issues are taken care of.  In
    62 particular, spacing and line breaks are directly taken from source
    63 text.  Incidentally, output looks very good if common type-setting
    64 conventions are observed: put a single space <em>after</em> each
    65 punctuation character ("<tt>,</tt>", "<tt>.</tt>", etc.), but none
    66 before it; do not extra spaces inside of parentheses; do not attempt
    67 to simulate table markup with spaces, avoid ``hanging'' indentations.
    68 
    69 </dl>
    70 
    71 </body>
    72 </html>