diff -r dd46544e259d -r 73b46b18c348 src/HOL/Library/README.html --- /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 @@ + + + + +HOL-Library/README + + + +

HOL-Library: supplemental theories for main Isabelle/HOL

+ +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. + +

+ +
Files +
Avoid unnecessary scattering of theories over several files. Use +new-style theories only, as old ones tend to clutter the file space +with separate .thy and .ML files. + +
Examples + +
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 Foobar accompanied by +Foobar_Examples. + +
Theory names +
The theory loader name space is flat, 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: +Foobar_Doobar (this looks best in LaTeX output). + +
Names of logical items +
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 foo_bar or +Foo_Bar (this looks best in LaTeX output). + +

+ +Note that syntax is global; qualified names loose syntax on +output. Do not use ``exotic'' symbols for syntax (such as +\<oplus>), but leave these for user applications. + +

Global context declarations +
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. + +
Mathematical symbols +
Non-ASCII symbols should be used with some care. In particular, +avoid unreadable arrows: ==> should be preferred over +\<Longrightarrow>. Use isatool unsymbolize to +clean up the sources. + +

+ +The following ASCII symbols of HOL should be generally avoided: +@, !, ?, ?!, %, better +use SOME, ALL (or \<forall>), +EX (or \<exists>), EX! (or +\<exists;>!), \<lambda>, respectively. +Note that bracket notation [| |] looks bad in LaTeX +output. + +

+ +Some additional mathematical symbols are quite suitable for both +readable sources and output document: +\<Inter>, +\<Union>, +\<and>, +\<in>, +\<inter>, +\<not>, +\<noteq>, +\<notin>, +\<or>, +\<subset>, +\<subseteq>, +\<times>, +\<union>. + +

Spacing + +
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 after each +punctuation character (",", ".", etc.), but none +before it; do not extra spaces inside of parentheses, unless the +delimiters are composed of multiple symbols (as in +[| |]); do not attempt to simulate table markup with +spaces, avoid ``hanging'' indentations. + +
+ + +