"The Supplemental Isabelle/HOL Library";
authorwenzelm
Wed Oct 18 23:31:16 2000 +0200 (2000-10-18)
changeset 1025373b46b18c348
parent 10252 dd46544e259d
child 10254 ed35c2b0e65c
"The Supplemental Isabelle/HOL Library";
src/HOL/Library/Library.thy
src/HOL/Library/README.html
src/HOL/Library/ROOT.ML
src/HOL/Library/document/root.bib
src/HOL/Library/document/root.tex
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Library/Library.thy	Wed Oct 18 23:31:16 2000 +0200
     1.3 @@ -0,0 +1,9 @@
     1.4 +(*<*)
     1.5 +theory Library =
     1.6 +  Accessible_Part +
     1.7 +  Multiset +
     1.8 +  Quotient +
     1.9 +  While_Combinator + While_Combinator_Example:
    1.10 +
    1.11 +end
    1.12 +(*>*)
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Library/README.html	Wed Oct 18 23:31:16 2000 +0200
     2.3 @@ -0,0 +1,114 @@
     2.4 +<html>
     2.5 +
     2.6 +<!-- $Id$ -->
     2.7 +
     2.8 +<head><title>HOL-Library/README</title></head>
     2.9 +
    2.10 +<body>
    2.11 +
    2.12 +<h1>HOL-Library: supplemental theories for main Isabelle/HOL</h1>
    2.13 +
    2.14 +This is a collection of generic theories that may be used together
    2.15 +with main Isabelle/HOL.  Note that theory loader path already includes
    2.16 +this directory by default.
    2.17 +
    2.18 +<p>
    2.19 +
    2.20 +Addition of new theories should be done with some care, as the
    2.21 +``module system'' of Isabelle is rather simplistic.  The following
    2.22 +guidelines may be helpful to achieve maximum re-usability and minimum
    2.23 +clashes with existing developments.
    2.24 +
    2.25 +<dl>
    2.26 +
    2.27 +<dt><strong>Files</strong>
    2.28 +<dd>Avoid unnecessary scattering of theories over several files.  Use
    2.29 +new-style theories only, as old ones tend to clutter the file space
    2.30 +with separate <tt>.thy</tt> and <tt>.ML</tt> files.
    2.31 +
    2.32 +<dt><strong>Examples</strong>
    2.33 +
    2.34 +<dd>Theories should be as ``generic'' as is sensible.  Unused (or
    2.35 +rather unusable?) standalone theories should be avoided; common
    2.36 +applications should actually refer to the present theory.  Small
    2.37 +example uses may be included as well, but should be put in a separate
    2.38 +theory, such as <tt>Foobar</tt> accompanied by
    2.39 +<tt>Foobar_Examples</tt>.
    2.40 +
    2.41 +<dt><strong>Theory names</strong>
    2.42 +<dd>The theory loader name space is <em>flat</em>, so use sufficiently
    2.43 +long and descriptive names to reduce the danger of clashes with the
    2.44 +user's own theories.  The convention for theory names is as follows:
    2.45 +<tt>Foobar_Doobar</tt> (this looks best in LaTeX output).
    2.46 +
    2.47 +<dt><strong>Names of logical items</strong>
    2.48 +<dd>There are separate hierarchically structured name spaces for
    2.49 +types, constants, theorems etc.  Nevertheless, some care should be
    2.50 +taken, as the name spaces are always ``open''.  Use adequate names;
    2.51 +avoid unreadable abbreviations.  The general naming convention is to
    2.52 +separate word constituents by underscores, as in <tt>foo_bar</tt> or
    2.53 +<tt>Foo_Bar</tt> (this looks best in LaTeX output).
    2.54 +
    2.55 +<p>
    2.56 +
    2.57 +Note that syntax is <em>global</em>; qualified names loose syntax on
    2.58 +output.  Do not use ``exotic'' symbols for syntax (such as
    2.59 +<tt>\&lt;oplus&gt;</tt>), but leave these for user applications.
    2.60 +
    2.61 +<dt><strong>Global context declarations</strong>
    2.62 +<dd>Only items introduced in the present theory should be declared
    2.63 +globally (e.g. as Simplifier rules).  Note that adding / deleting
    2.64 +rules stemming from parent theories may result in strange behavior
    2.65 +later, depending on the user's arrangement of import lists.
    2.66 +
    2.67 +<dt><strong>Mathematical symbols</strong>
    2.68 +<dd>Non-ASCII symbols should be used with some care. In particular,
    2.69 +avoid unreadable arrows: <tt>==&gt;</tt> should be preferred over
    2.70 +<tt>\&lt;Longrightarrow&gt;</tt>. Use <tt>isatool unsymbolize</tt> to
    2.71 +clean up the sources.
    2.72 +
    2.73 +<p>
    2.74 +
    2.75 +The following ASCII symbols of HOL should be generally avoided:
    2.76 +<tt>@</tt>, <tt>!</tt>, <tt>?</tt>, <tt>?!</tt>, <tt>%</tt>, better
    2.77 +use <tt>SOME</tt>, <tt>ALL</tt> (or <tt>\&lt;forall&gt;</tt>),
    2.78 +<tt>EX</tt> (or <tt>\&lt;exists&gt;</tt>), <tt>EX!</tt> (or
    2.79 +<tt>\&lt;exists;&gt!</tt>), <tt>\&lt;lambda&gt;</tt>, respectively.
    2.80 +Note that bracket notation <tt>[|&nbsp;|]</tt> looks bad in LaTeX
    2.81 +output.
    2.82 +
    2.83 +<p>
    2.84 +
    2.85 +Some additional mathematical symbols are quite suitable for both
    2.86 +readable sources and output document:
    2.87 +<tt>\&lt;Inter&gt;</tt>,
    2.88 +<tt>\&lt;Union&gt;</tt>,
    2.89 +<tt>\&lt;and&gt;</tt>,
    2.90 +<tt>\&lt;in&gt;</tt>,
    2.91 +<tt>\&lt;inter&gt;</tt>,
    2.92 +<tt>\&lt;not&gt;</tt>,
    2.93 +<tt>\&lt;noteq&gt;</tt>,
    2.94 +<tt>\&lt;notin&gt;</tt>,
    2.95 +<tt>\&lt;or&gt;</tt>,
    2.96 +<tt>\&lt;subset&gt;</tt>,
    2.97 +<tt>\&lt;subseteq&gt;</tt>,
    2.98 +<tt>\&lt;times&gt;</tt>,
    2.99 +<tt>\&lt;union&gt;</tt>.
   2.100 +
   2.101 +<dt><strong>Spacing</strong>
   2.102 +
   2.103 +<dd>Isabelle is able to produce a high-quality LaTeX document from the
   2.104 +theory sources, provided some minor issues are taken care of.  In
   2.105 +particular, spacing and line breaks are directly taken from source
   2.106 +text.  Incidently, output looks very good common type-setting
   2.107 +conventions are observed: put a single space <em>after</em> each
   2.108 +punctuation character ("<tt>,</tt>", "<tt>.</tt>", etc.), but none
   2.109 +before it; do not extra spaces inside of parentheses, unless the
   2.110 +delimiters are composed of multiple symbols (as in
   2.111 +<tt>[|&nbsp;|]</tt>); do not attempt to simulate table markup with
   2.112 +spaces, avoid ``hanging'' indentations.
   2.113 +
   2.114 +</dl>
   2.115 +
   2.116 +</body>
   2.117 +</html>
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Library/ROOT.ML	Wed Oct 18 23:31:16 2000 +0200
     3.3 @@ -0,0 +1,2 @@
     3.4 +
     3.5 +use_thy "Library";
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/Library/document/root.bib	Wed Oct 18 23:31:16 2000 +0200
     4.3 @@ -0,0 +1,27 @@
     4.4 +
     4.5 +@InProceedings{Slotosch:1997,
     4.6 +  author = 	 {Oscar Slotosch},
     4.7 +  title = 	 {FIXME},
     4.8 +  crossref =     {tphols97}}
     4.9 +
    4.10 +@InProceedings{paulin-tlca,
    4.11 +  author	= {Christine Paulin-Mohring},
    4.12 +  title		= {Inductive Definitions in the System {Coq}: Rules and
    4.13 +		 Properties},
    4.14 +  crossref	= {tlca93},
    4.15 +  pages		= {328-345}}
    4.16 +
    4.17 +@Proceedings{tlca93,
    4.18 +  title		= {Typed Lambda Calculi and Applications},
    4.19 +  booktitle	= {Typed Lambda Calculi and Applications},
    4.20 +  editor	= {M. Bezem and J.F. Groote},
    4.21 +  year		= 1993,
    4.22 +  publisher	= {Springer},
    4.23 +  series	= {LNCS 664}}
    4.24 +
    4.25 +@Proceedings{tphols97,
    4.26 +  title		= {Theorem Proving in Higher Order Logics: {TPHOLs} '97},
    4.27 +  booktitle	= {Theorem Proving in Higher Order Logics: {TPHOLs} '97},
    4.28 +  editor	= {Elsa L. Gunter and Amy Felty},
    4.29 +  series	= {LNCS 1275},
    4.30 +  year		= 1997}
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/Library/document/root.tex	Wed Oct 18 23:31:16 2000 +0200
     5.3 @@ -0,0 +1,42 @@
     5.4 +
     5.5 +% $Id$
     5.6 +
     5.7 +\documentclass[11pt,a4paper]{article}
     5.8 +\usepackage{ifthen}
     5.9 +\usepackage{isabelle,isabellesym,pdfsetup}
    5.10 +
    5.11 +\urlstyle{rm}
    5.12 +\isabellestyle{it}
    5.13 +\pagestyle{myheadings}
    5.14 +
    5.15 +\begin{document}
    5.16 +
    5.17 +\title{The Supplemental Isabelle/HOL Library}
    5.18 +\author{
    5.19 +  Gertrud Bauer \\
    5.20 +  Tobias Nipkow \\
    5.21 +  Lawrence C Paulson \\
    5.22 +  Markus Wenzel}
    5.23 +\maketitle
    5.24 +
    5.25 +\tableofcontents
    5.26 +\newpage
    5.27 +
    5.28 +%now hack the "header" markup to support \title and \author
    5.29 +\newcommand{\isabelletitle}{}\newcommand{\title}[1]{\gdef\isabelletitle{#1}}
    5.30 +\newcommand{\isabelleauthor}{}\newcommand{\author}[1]{\gdef\isabelleauthor{#1}}
    5.31 +\renewcommand{\isamarkupheader}[1]%
    5.32 +{\newpage\title{***~Theory ``\isabellecontext'': unknown title}\author{}#1%
    5.33 +\markright{THEORY~``\isabellecontext''}
    5.34 +\ifthenelse{\equal{}{\isabelletitle}}{}{\section{\isabelletitle}}%
    5.35 +\ifthenelse{\equal{}{\isabelleauthor}}{}%
    5.36 +{{\flushright\footnotesize\sl (By \isabelleauthor)\par\bigskip}}}
    5.37 +
    5.38 +\parindent 0pt \parskip 0.5ex
    5.39 +\input{session}
    5.40 +
    5.41 +\pagestyle{headings}
    5.42 +\bibliographystyle{abbrv}
    5.43 +\bibliography{root}
    5.44 +
    5.45 +\end{document}