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