--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/README.html Wed Oct 18 23:31:16 2000 +0200
@@ -0,0 +1,114 @@
+<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>