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