<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 togetherwith main Isabelle/HOL. Note that theory loader path already includesthis directory by default.<p>Addition of new theories should be done with some care, as the``module system'' of Isabelle is rather simplistic. The followingguidelines may be helpful to achieve maximum re-usability and minimumclashes with existing developments.<dl><dt><strong>Files</strong><dd>Avoid unnecessary scattering of theories over several files. Usenew-style theories only, as old ones tend to clutter the file spacewith separate <tt>.thy</tt> and <tt>.ML</tt> files.<dt><strong>Examples</strong><dd>Theories should be as ``generic'' as is sensible. Unused (orrather unusable?) theories should be avoided; common applicationsshould actually refer to the present theory. Small example uses maybe included in the library as well, but should be put in a separatetheory, 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 sufficientlylong and descriptive names to reduce the danger of clashes with theuser'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 fortypes, constants, theorems etc. Nevertheless, some care should betaken, as the name spaces are always ``open''. Use adequate names;avoid unreadable abbreviations. The general naming convention is toseparate 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 onoutput. 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 declaredglobally (e.g. as Simplifier rules). Note that adding and deletingrules 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 as appropriate, with somecare. In particular, avoid unreadable arrows: <tt>==></tt> shouldbe preferred over <tt>\<Longrightarrow></tt>. Use <tt>isatoolunsymbolize</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>, betteruse <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 LaTeXoutput.<p>Some additional mathematical symbols are quite suitable for bothreadable sources and the output document:<tt>\<Inter></tt>,<tt>\<Union></tt>,<tt>\<and></tt>,<tt>\<in></tt>,<tt>\<inter></tt>,<tt>\<le></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 thetheory sources, provided some minor issues are taken care of. Inparticular, spacing and line breaks are directly taken from sourcetext. Incidently, output looks very good common type-settingconventions are observed: put a single space <em>after</em> eachpunctuation character ("<tt>,</tt>", "<tt>.</tt>", etc.), but nonebefore it; do not extra spaces inside of parentheses, unless thedelimiters are composed of multiple symbols (as in<tt>[| |]</tt>); do not attempt to simulate table markup withspaces, avoid ``hanging'' indentations.</dl></body></html>