<html>
<!-- $Id$ -->
<head><title>HOL-Library/README</title></head>
<body>
<h1>HOL-Library: supplemental theories for main Isabelle/HOL</h1>
This is a collection of generic theories that may be used together
with main Isabelle/HOL. Note that theory loader path already includes
this directory by default.
<p>
Addition of new theories should be done with some care, as the
``module system'' of Isabelle is rather simplistic. The following
guidelines may be helpful to achieve maximum re-usability and minimum
clashes with existing developments.
<dl>
<dt><strong>Files</strong>
<dd>Avoid unnecessary scattering of theories over several files. Use
new-style theories only, as old ones tend to clutter the file space
with separate <tt>.thy</tt> and <tt>.ML</tt> files.
<dt><strong>Examples</strong>
<dd>Theories should be as ``generic'' as is sensible. Unused (or
rather unusable?) standalone theories should be avoided; common
applications should actually refer to the present theory. Small
example uses may be included as well, but should be put in a separate
theory, such as <tt>Foobar</tt> accompanied by
<tt>Foobar_Examples</tt>.
<dt><strong>Theory names</strong>
<dd>The theory loader name space is <em>flat</em>, so use sufficiently
long and descriptive names to reduce the danger of clashes with the
user's own theories. The convention for theory names is as follows:
<tt>Foobar_Doobar</tt> (this looks best in LaTeX output).
<dt><strong>Names of logical items</strong>
<dd>There are separate hierarchically structured name spaces for
types, constants, theorems etc. Nevertheless, some care should be
taken, as the name spaces are always ``open''. Use adequate names;
avoid unreadable abbreviations. The general naming convention is to
separate word constituents by underscores, as in <tt>foo_bar</tt> or
<tt>Foo_Bar</tt> (this looks best in LaTeX output).
<p>
Note that syntax is <em>global</em>; qualified names loose syntax on
output. Do not use ``exotic'' symbols for syntax (such as
<tt>\<oplus></tt>), but leave these for user applications.
<dt><strong>Global context declarations</strong>
<dd>Only items introduced in the present theory should be declared
globally (e.g. as Simplifier rules). Note that adding / deleting
rules stemming from parent theories may result in strange behavior
later, depending on the user's arrangement of import lists.
<dt><strong>Mathematical symbols</strong>
<dd>Non-ASCII symbols should be used with some care. In particular,
avoid unreadable arrows: <tt>==></tt> should be preferred over
<tt>\<Longrightarrow></tt>. Use <tt>isatool unsymbolize</tt> to
clean up the sources.
<p>
The following ASCII symbols of HOL should be generally avoided:
<tt>@</tt>, <tt>!</tt>, <tt>?</tt>, <tt>?!</tt>, <tt>%</tt>, better
use <tt>SOME</tt>, <tt>ALL</tt> (or <tt>\<forall></tt>),
<tt>EX</tt> (or <tt>\<exists></tt>), <tt>EX!</tt> (or
<tt>\<exists;>!</tt>), <tt>\<lambda></tt>, respectively.
Note that bracket notation <tt>[| |]</tt> looks bad in LaTeX
output.
<p>
Some additional mathematical symbols are quite suitable for both
readable sources and output document:
<tt>\<Inter></tt>,
<tt>\<Union></tt>,
<tt>\<and></tt>,
<tt>\<in></tt>,
<tt>\<inter></tt>,
<tt>\<not></tt>,
<tt>\<noteq></tt>,
<tt>\<notin></tt>,
<tt>\<or></tt>,
<tt>\<subset></tt>,
<tt>\<subseteq></tt>,
<tt>\<times></tt>,
<tt>\<union></tt>.
<dt><strong>Spacing</strong>
<dd>Isabelle is able to produce a high-quality LaTeX document from the
theory sources, provided some minor issues are taken care of. In
particular, spacing and line breaks are directly taken from source
text. Incidently, output looks very good common type-setting
conventions are observed: put a single space <em>after</em> each
punctuation character ("<tt>,</tt>", "<tt>.</tt>", etc.), but none
before it; do not extra spaces inside of parentheses, unless the
delimiters are composed of multiple symbols (as in
<tt>[| |]</tt>); do not attempt to simulate table markup with
spaces, avoid ``hanging'' indentations.
</dl>
</body>
</html>