--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Library.thy Wed Oct 18 23:31:16 2000 +0200
@@ -0,0 +1,9 @@
+(*<*)
+theory Library =
+ Accessible_Part +
+ Multiset +
+ Quotient +
+ While_Combinator + While_Combinator_Example:
+
+end
+(*>*)
--- /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>
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/ROOT.ML Wed Oct 18 23:31:16 2000 +0200
@@ -0,0 +1,2 @@
+
+use_thy "Library";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/document/root.bib Wed Oct 18 23:31:16 2000 +0200
@@ -0,0 +1,27 @@
+
+@InProceedings{Slotosch:1997,
+ author = {Oscar Slotosch},
+ title = {FIXME},
+ crossref = {tphols97}}
+
+@InProceedings{paulin-tlca,
+ author = {Christine Paulin-Mohring},
+ title = {Inductive Definitions in the System {Coq}: Rules and
+ Properties},
+ crossref = {tlca93},
+ pages = {328-345}}
+
+@Proceedings{tlca93,
+ title = {Typed Lambda Calculi and Applications},
+ booktitle = {Typed Lambda Calculi and Applications},
+ editor = {M. Bezem and J.F. Groote},
+ year = 1993,
+ publisher = {Springer},
+ series = {LNCS 664}}
+
+@Proceedings{tphols97,
+ title = {Theorem Proving in Higher Order Logics: {TPHOLs} '97},
+ booktitle = {Theorem Proving in Higher Order Logics: {TPHOLs} '97},
+ editor = {Elsa L. Gunter and Amy Felty},
+ series = {LNCS 1275},
+ year = 1997}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/document/root.tex Wed Oct 18 23:31:16 2000 +0200
@@ -0,0 +1,42 @@
+
+% $Id$
+
+\documentclass[11pt,a4paper]{article}
+\usepackage{ifthen}
+\usepackage{isabelle,isabellesym,pdfsetup}
+
+\urlstyle{rm}
+\isabellestyle{it}
+\pagestyle{myheadings}
+
+\begin{document}
+
+\title{The Supplemental Isabelle/HOL Library}
+\author{
+ Gertrud Bauer \\
+ Tobias Nipkow \\
+ Lawrence C Paulson \\
+ Markus Wenzel}
+\maketitle
+
+\tableofcontents
+\newpage
+
+%now hack the "header" markup to support \title and \author
+\newcommand{\isabelletitle}{}\newcommand{\title}[1]{\gdef\isabelletitle{#1}}
+\newcommand{\isabelleauthor}{}\newcommand{\author}[1]{\gdef\isabelleauthor{#1}}
+\renewcommand{\isamarkupheader}[1]%
+{\newpage\title{***~Theory ``\isabellecontext'': unknown title}\author{}#1%
+\markright{THEORY~``\isabellecontext''}
+\ifthenelse{\equal{}{\isabelletitle}}{}{\section{\isabelletitle}}%
+\ifthenelse{\equal{}{\isabelleauthor}}{}%
+{{\flushright\footnotesize\sl (By \isabelleauthor)\par\bigskip}}}
+
+\parindent 0pt \parskip 0.5ex
+\input{session}
+
+\pagestyle{headings}
+\bibliographystyle{abbrv}
+\bibliography{root}
+
+\end{document}