changeset 10253 73b46b18c348
child 10282 b7d96e94796f
--- /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 @@
+<!-- $Id$ -->
+<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.
+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.
+<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.
+<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
+<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).
+Note that syntax is <em>global</em>; qualified names loose syntax on
+output.  Do not use ``exotic'' symbols for syntax (such as
+<tt>\&lt;oplus&gt;</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>==&gt;</tt> should be preferred over
+<tt>\&lt;Longrightarrow&gt;</tt>. Use <tt>isatool unsymbolize</tt> to
+clean up the sources.
+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>\&lt;forall&gt;</tt>),
+<tt>EX</tt> (or <tt>\&lt;exists&gt;</tt>), <tt>EX!</tt> (or
+<tt>\&lt;exists;&gt!</tt>), <tt>\&lt;lambda&gt;</tt>, respectively.
+Note that bracket notation <tt>[|&nbsp;|]</tt> looks bad in LaTeX
+Some additional mathematical symbols are quite suitable for both
+readable sources and output document:
+<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>[|&nbsp;|]</tt>); do not attempt to simulate table markup with
+spaces, avoid ``hanging'' indentations.