--- a/doc-src/Ref/theories.tex Mon May 05 21:18:01 1997 +0200
+++ b/doc-src/Ref/theories.tex Tue May 06 12:50:16 1997 +0200
@@ -2,12 +2,12 @@
\chapter{Theories, Terms and Types} \label{theories}
\index{theories|(}\index{signatures|bold}
-\index{reading!axioms|see{{\tt assume_ax}}}
-Theories organize the syntax, declarations and axioms of a mathematical
-development. They are built, starting from the Pure theory, by extending
-and merging existing theories. They have the \ML\ type \mltydx{theory}.
-Theory operations signal errors by raising exception \xdx{THEORY},
-returning a message and a list of theories.
+\index{reading!axioms|see{{\tt assume_ax}}} Theories organize the
+syntax, declarations and axioms of a mathematical development. They
+are built, starting from the {\Pure} or {\CPure} theory, by extending
+and merging existing theories. They have the \ML\ type
+\mltydx{theory}. Theory operations signal errors by raising exception
+\xdx{THEORY}, returning a message and a list of theories.
Signatures, which contain information about sorts, types, constants and
syntax, have the \ML\ type~\mltydx{Sign.sg}. For identification, each
@@ -32,11 +32,12 @@
Appendix~\ref{app:TheorySyntax} presents the concrete syntax for theory
definitions; here is an explanation of the constituent parts:
\begin{description}
-\item[{\it theoryDef}]
- is the full definition. The new theory is called $id$. It is the union
- of the named {\bf parent theories}\indexbold{theories!parent}, possibly
- extended with new classes, etc. The basic theory, which contains only
- the meta-logic, is called \thydx{Pure}.
+\item[{\it theoryDef}] is the full definition. The new theory is
+ called $id$. It is the union of the named {\bf parent
+ theories}\indexbold{theories!parent}, possibly extended with new
+ components. \thydx{Pure} and \thydx{CPure} are the basic theories,
+ which contain only the meta-logic. They differ just in their
+ concrete syntax for function applications.
Normally each {\it name\/} is an identifier, the name of the parent theory.
Quoted strings can be used to document additional file dependencies; see
@@ -56,10 +57,9 @@
variables created internally. If omitted, the default sort is the listwise
union of the default sorts of the parent theories (i.e.\ their logical
intersection).
-
-\item[$sort$]
- is a finite set of classes. A single class $id$ abbreviates the singleton
- set {\tt\{}$id${\tt\}}.
+
+\item[$sort$] is a finite set of classes. A single class $id$
+ abbreviates the sort $\ttlbrace id\ttrbrace$.
\item[$types$]
is a series of type declarations. Each declares a new type constructor
@@ -75,19 +75,23 @@
declares a type or constant to be an infix operator of priority $nat$
associating to the left ({\tt infixl}) or right ({\tt infixr}). Only
2-place type constructors can have infix status; an example is {\tt
- ('a,'b)~"*"~(infixr~20)}, which expresses binary product types.
-
-\item[$arities$]
- is a series of arity declarations. Each assigns arities to type
- constructors. The $name$ must be an existing type constructor, which is
- given the additional arity $arity$.
+ ('a,'b)~"*"~(infixr~20)}, which may express binary product types.
-\item[$constDecl$]
- is a series of constant declarations. Each new constant $name$ is given
- the specified type. The optional $mixfix$ annotations may
- attach concrete syntax to the constant. A variant of {\tt consts} is the
- {\tt syntax} section\index{*syntax section}, which adds just syntax without
- declaring logical constants.
+\item[$arities$] is a series of type arity declarations. Each assigns
+ arities to type constructors. The $name$ must be an existing type
+ constructor, which is given the additional arity $arity$.
+
+\item[$consts$] is a series of constant declarations. Each new
+ constant $name$ is given the specified type. The optional $mixfix$
+ annotations may attach concrete syntax to the constant.
+
+\item[$syntax$] \index{*syntax section}\index{print mode} is a variant
+ of $consts$ which adds just syntax without actually declaring
+ logical constants. This gives full control over a theory's context
+ free grammar. The optional $mode$ specifies the print mode where the
+ mixfix productions should be added. If there is no \texttt{output}
+ option given, all productions are also added to the input syntax
+ (regardless of the print mode).
\item[$mixfix$] \index{mixfix declarations}
annotations can take three forms:
@@ -115,13 +119,28 @@
\item[$rules$]
is a series of rule declarations. Each has a name $id$ and the formula is
given by the $string$. Rule names must be distinct within any single
- theory file.
+ theory.
\item[$defs$] is a series of definitions. They are just like $rules$, except
that every $string$ must be a definition (see below for details).
\item[$constdefs$] combines the declaration of constants and their
definition. The first $string$ is the type, the second the definition.
+
+\item[$axclass$] \index{*axclass section} defines an
+ \rmindex{axiomatic type class} as the intersection of existing
+ classes, with additional axioms holding. Class axioms may not
+ contain more than one type variable. The class axioms (with implicit
+ sort constraints added) are bound to the given names. Furthermore a
+ class introduction rule is generated, which is automatically
+ employed by $instance$ to prove instantiations of this class.
+
+\item[$instance$] \index{*instance section} proves class inclusions or
+ type arities at the logical level and then transfers these to the
+ type signature. The instantiation is proven and checked properly.
+ The user has to supply sufficient witness information: theorems
+ ($longident$), axioms ($string$), or even arbitrary \ML{} tactic
+ code $verbatim$.
\item[$oracle$] links the theory to a trusted external reasoner. It is
allowed to create theorems, but each theorem carries a proof object
@@ -137,18 +156,19 @@
\subsection{Definitions}\indexbold{definitions}
-{\bf Definitions} are intended to express abbreviations. The simplest form of
-a definition is $f \equiv t$, where $f$ is a constant. Isabelle also allows a
-derived form where the arguments of~$f$ appear on the left, abbreviating a
-string of $\lambda$-abstractions.
+{\bf Definitions} are intended to express abbreviations. The simplest
+form of a definition is $f \equiv t$, where $f$ is a constant.
+Isabelle also allows a derived forms where the arguments of~$f$ appear
+on the left, abbreviating a string of $\lambda$-abstractions.
Isabelle makes the following checks on definitions:
\begin{itemize}
-\item Arguments (on the left-hand side) must be distinct variables
+\item Arguments (on the left-hand side) must be distinct variables.
\item All variables on the right-hand side must also appear on the left-hand
side.
-\item All type variables on the right-hand side must also appear on the
- left-hand side; this prohibits definitions such as {\tt zero == length []}.
+\item All type variables on the right-hand side must also appear on
+ the left-hand side; this prohibits definitions such as {\tt
+ (zero::nat) == length ([]::'a list)}.
\item The definition must not be recursive. Most object-logics provide
definitional principles that can be used to express recursion safely.
\end{itemize}
@@ -164,31 +184,26 @@
In order to guarantee principal types~\cite{nipkow-prehofer},
arity declarations must obey two conditions:
\begin{itemize}
-\item There must be no two declarations $ty :: (\vec{r})c$ and $ty ::
- (\vec{s})c$ with $\vec{r} \neq \vec{s}$. For example, the following is
- forbidden:
+\item There must not be any two declarations $ty :: (\vec{r})c$ and
+ $ty :: (\vec{s})c$ with $\vec{r} \neq \vec{s}$. For example, this
+ excludes the following:
\begin{ttbox}
-types
- 'a ty
arities
- ty :: ({\ttlbrace}logic{\ttrbrace}) logic
- ty :: ({\ttlbrace}{\ttrbrace})logic
+ foo :: ({\ttlbrace}logic{\ttrbrace}) logic
+ foo :: ({\ttlbrace}{\ttrbrace})logic
\end{ttbox}
\item If there are two declarations $ty :: (s@1,\dots,s@n)c$ and $ty ::
(s@1',\dots,s@n')c'$ such that $c' < c$ then $s@i' \preceq s@i$ must hold
for $i=1,\dots,n$. The relationship $\preceq$, defined as
\[ s' \preceq s \iff \forall c\in s. \exists c'\in s'.~ c'\le c, \]
-expresses that the set of types represented by $s'$ is a subset of the set of
-types represented by $s$. For example, the following is forbidden:
+expresses that the set of types represented by $s'$ is a subset of the
+set of types represented by $s$. Assuming $term \preceq logic$, the
+following is forbidden:
\begin{ttbox}
-classes
- term < logic
-types
- 'a ty
arities
- ty :: ({\ttlbrace}logic{\ttrbrace})logic
- ty :: ({\ttlbrace}{\ttrbrace})term
+ foo :: ({\ttlbrace}logic{\ttrbrace})logic
+ foo :: ({\ttlbrace}{\ttrbrace})term
\end{ttbox}
\end{itemize}
@@ -219,14 +234,15 @@
suppresses the deletion of temporary files.
\end{ttdescription}
%
-Each theory definition must reside in a separate file. Let the file {\it
- T}{\tt.thy} contain the definition of a theory called~$T$, whose parent
-theories are $TB@1$ \dots $TB@n$. Calling \ttindexbold{use_thy}~{\tt"{\it
- T\/}"} reads the file {\it T}{\tt.thy}, writes a temporary \ML{}
-file {\tt.{\it T}.thy.ML}, and reads the latter file. Recursive {\tt
- use_thy} calls load those parent theories that have not been loaded
-previously; the recursive calls may continue to any depth. One {\tt use_thy}
-call can read an entire logic provided all theories are linked appropriately.
+Each theory definition must reside in a separate file. Let the file
+{\it T}{\tt.thy} contain the definition of a theory called~$T$, whose
+parent theories are $TB@1$ \dots $TB@n$. Calling
+\ttindex{use_thy}~{\tt"{\it T\/}"} reads the file {\it T}{\tt.thy},
+writes a temporary \ML{} file {\tt.{\it T}.thy.ML}, and reads the
+latter file. Recursive {\tt use_thy} calls load those parent theories
+that have not been loaded previously; the recursive calls may continue
+to any depth. One {\tt use_thy} call can read an entire logic
+provided all theories are linked appropriately.
The result is an \ML\ structure~$T$ containing at least a component {\tt thy}
for the new theory and components for each of the rules. The structure also
@@ -234,9 +250,9 @@
{\tt.{\it T}.thy.ML} is then deleted if {\tt delete_tmpfiles} is set to {\tt
true} and no errors occurred.
-Finally the file {\it T}{\tt.ML} is read, if it exists. This file normally
-begins with the declaration {\tt open~$T$} and contains proofs involving
-the new theory.
+Finally the file {\it T}{\tt.ML} is read, if it exists. Since the
+structure $T$ is automatically open in this context, proof scripts may
+(or even should) refer to its components by unqualified names.
Some applications construct theories directly by calling \ML\ functions. In
this situation there is no {\tt.thy} file, only an {\tt.ML} file. The
@@ -284,17 +300,18 @@
\end{ttdescription}
-\goodbreak
-\subsection{Important note for Poly/ML users}\index{Poly/{\ML} compiler}
-The theory mechanism depends upon reference variables. At the end of a
-Poly/\ML{} session, the contents of references are lost unless they are
-declared in the current database. In particular, assignments to references
-of the {\tt Pure} database are lost, including all information about loaded
-theories. To avoid losing this information simply call
-\begin{ttbox}
-init_thy_reader();
-\end{ttbox}
-when building the new database.
+%FIXME remove
+%\goodbreak
+%\subsection{Important note for Poly/ML users}\index{Poly/{\ML} compiler}
+%The theory mechanism depends upon reference variables. At the end of a
+%Poly/\ML{} session, the contents of references are lost unless they are
+%declared in the current database. In particular, assignments to references
+%of the {\tt Pure} database are lost, including all information about loaded
+%theories. To avoid losing this information simply call
+%\begin{ttbox}
+%init_thy_reader();
+%\end{ttbox}
+%when building the new database.
\subsection{*Pseudo theories}\label{sec:pseudo-theories}
@@ -346,9 +363,9 @@
The resulting theory ensures that {\tt update} reloads {\tt orphan}
whenever it reloads one of the $A@i$.
-For an extensive example of how this technique can be used to link lots of
-theory files and load them by just a few {\tt use_thy} calls, consult the
-sources of \ZF{} set theory.
+For an extensive example of how this technique can be used to link
+lots of theory files and load them by just a few {\tt use_thy} calls
+see the sources of one of the major object-logics (e.g.\ \ZF).
@@ -384,17 +401,21 @@
\hbox{\verb'?a=?b ==> ?b=?a [!!a b. a=b ==> b=a]'}
\end{ttdescription}
-\subsection{Building a theory}
+\subsection{*Building a theory}
\label{BuildingATheory}
\index{theories!constructing|bold}
\begin{ttbox}
-pure_thy : theory
+Pure.thy : theory
+CPure.thy : theory
merge_theories : theory * theory -> theory
\end{ttbox}
-\begin{ttdescription}
-\item[\ttindexbold{pure_thy}] contains just the syntax and signature
- of the meta-logic. There are no axioms: meta-level inferences are carried
- out by \ML\ functions.
+\begin{description}
+\item[\ttindexbold{Pure.thy}, \ttindexbold{CPure.thy}] contain the
+ syntax and signature of the meta-logic. There are no axioms:
+ meta-level inferences are carried out by \ML\ functions. The two
+ \Pure s just differ in their concrete syntax of function
+ application: $t(u@1, \ldots, u@n)$ vs.\ $t\,u@1,\ldots\,u@n$.
+
\item[\ttindexbold{merge_theories} ($thy@1$, $thy@2$)] merges the two
theories $thy@1$ and $thy@2$. The resulting theory contains all of the
syntax, signature and axioms of the constituent theories. Merging theories
@@ -419,7 +440,7 @@
%\begin{ttbox}
%Attempt to merge different versions of theory: \(T\)
%\end{ttbox}
-\end{ttdescription}
+\end{description}
%% FIXME
%\item [\ttindexbold{extend_theory} $thy$ {\tt"}$T${\tt"}
@@ -456,6 +477,7 @@
\subsection{Inspecting a theory}\label{sec:inspct-thy}
\index{theories!inspecting|bold}
\begin{ttbox}
+print_syntax : theory -> unit
print_theory : theory -> unit
axioms_of : theory -> (string * thm) list
thms_of : theory -> (string * thm) list
@@ -465,9 +487,12 @@
\end{ttbox}
These provide means of viewing a theory's components.
\begin{ttdescription}
-\item[\ttindexbold{print_theory} $thy$]
-prints the contents of $thy$ excluding the syntax related parts (which are
-shown by {\tt print_syntax}). The output is quite verbose.
+\item[\ttindexbold{print_syntax} $thy$] prints the syntax of $thy$
+ (grammar, macros, translation functions etc., see
+ page~\pageref{pg:print_syn} for more details).
+
+\item[\ttindexbold{print_theory} $thy$] prints the logical parts of
+ $thy$, excluding the syntax.
\item[\ttindexbold{axioms_of} $thy$]
returns the additional axioms of the most recent extend node of~$thy$.
@@ -487,223 +512,224 @@
with~$thy$.
\end{ttdescription}
-
-\section{Generating HTML documents}
-\index{HTML|bold}
-
-Isabelle is able to make HTML documents that show a theory's
-definition, the theorems proved in its ML file and the relationship
-with its ancestors and descendants. HTML stands for Hypertext Markup
-Language and is used in the World Wide Web to represent text
-containing images and links to other documents. Web browsers like
-{\tt xmosaic} or {\tt netscape} are used to view these documents.
-
-Besides the three HTML files that are made for every theory
-(definition and theorems, ancestors, descendants), Isabelle stores
-links to all theories in an index file. These indexes are themself
-linked with other indexes to represent the hierarchic structure of
-Isabelle's logics.
-
-To make HTML files for logics that are part of the Isabelle
-distribution, simply set the shell environment variable {\tt
-MAKE_HTML} before compiling a logic. This works for single logics as
-well as for the shell script {\tt make-all} (see
-\ref{sec:shell-scripts}). To make HTML files for {\tt FOL} using a
-{\tt csh} style shell, the following commands can be used:
-
-\begin{ttbox}
-cd FOL
-setenv MAKE_HTML
-make
-\end{ttbox}
-
-The databases made this way do not differ from the ones made with an
-unset {\tt MAKE_HTML}; in particular no HTML files are written if the
-database is used to manually load a theory.
-
-As you will see below, the HTML generation is controlled by a boolean
-reference variable. If you want to make databases which define this
-variable's value as {\tt true} and where therefore HTML files are
-written each time {\tt use_thy} is invoked, you have to set {\tt
-MAKE_HTML} to ``{\tt true}'':
-
-\begin{ttbox}
-cd FOL
-setenv MAKE_HTML true
-make
-\end{ttbox}
-
-All theories loaded from within the {\tt FOL} database and all
-databases derived from it will now cause HTML files to be written.
-This behaviour can be changed by assigning a value of {\tt false} to
-the boolean reference variable {\tt make_html}. Be careful when making
-such databases publicly available since it means that your users will
-generate HTML files though they might not intend to do so.
-
-As some of Isabelle's logics are based on others (e.g. {\tt ZF} on
-{\tt FOL}) and because the HTML files list a theory's ancestors, you
-should not make HTML files for a logic if the HTML files for the base
-logic do not exist. Otherwise some of the hypertext links might point
-to non-existing documents.
-
-The entry point to all logics is the {\tt index.html} file located in
-Isabelle's main directory. You can also access a HTML version of the
-distribution package at
-
-\begin{ttbox}
-http://www4.informatik.tu-muenchen.de/~nipkow/isabelle
-\end{ttbox}
-
-
-\subsection*{Manual HTML generation}
-
-To manually control the generation of HTML files the following
-commands and reference variables are used:
-
-\begin{ttbox}
-init_html : unit -> unit
-make_html : bool ref
-finish_html : unit -> unit
-\end{ttbox}
-
-\begin{ttdescription}
-\item[\ttindexbold{init_html}]
-activates the HTML facility. It stores the current working directory
-as the place where the {\tt index.html} file for all theories loaded
-afterwards will be stored.
-
-\item[\ttindexbold{make_html}]
-is a boolean reference variable read by {\tt use_thy} and other
-functions to decide whether HTML files should be made. After you have
-used {\tt init_html} you can manually change {\tt make_html}'s value
-to temporarily disable HTML generation.
-
-\item[\ttindexbold{finish_html}]
-has to be called after all theories have been read that should be
-listed in the current {\tt index.html} file. It reads a temporary
-file with information about the theories read since the last use of
-{\tt init_html} and makes the {\tt index.html} file. If {\tt
-make_html} is {\tt false} nothing is done.
-
-The indexes made by this function also contain a link to the {\tt
-README} file if there exists one in the directory where the index is
-stored. If there's a {\tt README.html} file it is used instead of
-{\tt README}.
-
-\end{ttdescription}
+%FIXME move to sysman!
+%\section{Generating HTML documents}
+%\index{HTML|bold}
+%
+%Isabelle is able to make HTML documents that show a theory's
+%definition, the theorems proved in its ML file and the relationship
+%with its ancestors and descendants. HTML stands for Hypertext Markup
+%Language and is used in the World Wide Web to represent text
+%containing images and links to other documents. Web browsers like
+%{\tt xmosaic} or {\tt netscape} are used to view these documents.
+%
+%Besides the three HTML files that are made for every theory
+%(definition and theorems, ancestors, descendants), Isabelle stores
+%links to all theories in an index file. These indexes are themself
+%linked with other indexes to represent the hierarchic structure of
+%Isabelle's logics.
+%
+%To make HTML files for logics that are part of the Isabelle
+%distribution, simply set the shell environment variable {\tt
+%MAKE_HTML} before compiling a logic. This works for single logics as
+%well as for the shell script {\tt make-all} (see
+%\ref{sec:shell-scripts}). To make HTML files for {\tt FOL} using a
+%{\tt csh} style shell, the following commands can be used:
+%
+%\begin{ttbox}
+%cd FOL
+%setenv MAKE_HTML
+%make
+%\end{ttbox}
+%
+%The databases made this way do not differ from the ones made with an
+%unset {\tt MAKE_HTML}; in particular no HTML files are written if the
+%database is used to manually load a theory.
+%
+%As you will see below, the HTML generation is controlled by a boolean
+%reference variable. If you want to make databases which define this
+%variable's value as {\tt true} and where therefore HTML files are
+%written each time {\tt use_thy} is invoked, you have to set {\tt
+%MAKE_HTML} to ``{\tt true}'':
+%
+%\begin{ttbox}
+%cd FOL
+%setenv MAKE_HTML true
+%make
+%\end{ttbox}
+%
+%All theories loaded from within the {\tt FOL} database and all
+%databases derived from it will now cause HTML files to be written.
+%This behaviour can be changed by assigning a value of {\tt false} to
+%the boolean reference variable {\tt make_html}. Be careful when making
+%such databases publicly available since it means that your users will
+%generate HTML files though they might not intend to do so.
+%
+%As some of Isabelle's logics are based on others (e.g. {\tt ZF} on
+%{\tt FOL}) and because the HTML files list a theory's ancestors, you
+%should not make HTML files for a logic if the HTML files for the base
+%logic do not exist. Otherwise some of the hypertext links might point
+%to non-existing documents.
+%
+%The entry point to all logics is the {\tt index.html} file located in
+%Isabelle's main directory. You can also access a HTML version of the
+%distribution package at
+%
+%\begin{ttbox}
+%http://www4.informatik.tu-muenchen.de/~nipkow/isabelle/
+%\end{ttbox}
+%
+%
+%\subsection*{Manual HTML generation}
+%
+%To manually control the generation of HTML files the following
+%commands and reference variables are used:
+%
+%\begin{ttbox}
+%init_html : unit -> unit
+%make_html : bool ref
+%finish_html : unit -> unit
+%\end{ttbox}
+%
+%\begin{ttdescription}
+%\item[\ttindexbold{init_html}]
+%activates the HTML facility. It stores the current working directory
+%as the place where the {\tt index.html} file for all theories loaded
+%afterwards will be stored.
+%
+%\item[\ttindexbold{make_html}]
+%is a boolean reference variable read by {\tt use_thy} and other
+%functions to decide whether HTML files should be made. After you have
+%used {\tt init_html} you can manually change {\tt make_html}'s value
+%to temporarily disable HTML generation.
+%
+%\item[\ttindexbold{finish_html}]
+%has to be called after all theories have been read that should be
+%listed in the current {\tt index.html} file. It reads a temporary
+%file with information about the theories read since the last use of
+%{\tt init_html} and makes the {\tt index.html} file. If {\tt
+%make_html} is {\tt false} nothing is done.
+%
+%The indexes made by this function also contain a link to the {\tt
+%README} file if there exists one in the directory where the index is
+%stored. If there's a {\tt README.html} file it is used instead of
+%{\tt README}.
+%
+%\end{ttdescription}
+%
+%The above functions could be used in the following way:
+%
+%\begin{ttbox}
+%init_html();
+%{\out Setting path for index.html to "/home/clasohm/isabelle/HOL"}
+%use_thy "List";
+%\dots
+%finish_html();
+%\end{ttbox}
+%
+%Please note that HTML files are made only for those theories that are
+%read while {\tt make_html} is {\tt true}. These files may contain
+%links to theories that were read with a {\tt false} {\tt make_html}
+%and therefore point to non-existing files.
+%
+%
+%\subsection*{Extending or adding a logic}
+%
+%If you add a new subdirectory to Isabelle's logics (or add a completly
+%new logic), you would have to call {\tt init_html} at the start of every
+%directory's {\tt ROOT.ML} file and {\tt finish_html} at the end of
+%it. This is automatically done if you use
+%
+%\begin{ttbox}\index{use_dir}
+%use_dir : string -> unit
+%\end{ttbox}
+%
+%This function takes a path as its parameter, changes the working
+%directory, calls {\tt init_html} if {\tt make_html} is {\tt true},
+%executes {\tt ROOT.ML}, and calls {\tt finish_html}. The {\tt
+%index.html} file written in this directory will be automatically
+%linked to the first index found in the (recursively searched)
+%superdirectories.
+%
+%Instead of adding something like
+%
+%\begin{ttbox}
+%use"ex/ROOT.ML";
+%\end{ttbox}
+%
+%to the logic's makefile you have to use this:
+%
+%\begin{ttbox}
+%use_dir"ex";
+%\end{ttbox}
+%
+%Since {\tt use_dir} calls {\tt init_html} only if {\tt make_html} is
+%{\tt true} the generation of HTML files depends on the value this
+%reference variable has. It can either be inherited from the used \ML{}
+%database or set in the makefile before {\tt use_dir} is invoked,
+%e.g. to set it's value according to the environment variable {\tt
+%MAKE_HTML}.
+%
+%The generated HTML files contain all theorems that were proved in the
+%theory's \ML{} file with {\tt qed}, {\tt qed_goal} and {\tt qed_goalw},
+%or stored with {\tt bind_thm} and {\tt store_thm}. Additionally there
+%is a hypertext link to the whole \ML{} file.
+%
+%You can add section headings to the list of theorems by using
+%
+%\begin{ttbox}\index{use_dir}
+%section: string -> unit
+%\end{ttbox}
+%
+%in a theory's ML file, which converts a plain string to a HTML
+%heading and inserts it before the next theorem proved or stored with
+%one of the above functions. If {\tt make_html} is {\tt false} nothing
+%is done.
+%
+%
+%\subsection*{Using someone else's database}
+%
+%To make them independent from their storage place, the HTML files only
+%contain relative paths which are derived from absolute ones like the
+%current working directory, {\tt gif_path} or {\tt base_path}. The
+%latter two are reference variables which are initialized at the time
+%when the {\tt Pure} database is made. Because you need write access
+%for the current directory to make HTML files and therefore (probably)
+%generate them in your home directory, the absolute {\tt base_path} is
+%not correct if you use someone else's database or a database derived
+%from it.
+%
+%In that case you first should set {\tt base_path} to the value of {\em
+%your} Isabelle main directory, i.e. the directory that contains the
+%subdirectories where standard logics like {\tt FOL} and {\tt HOL} or
+%your own logics are stored. If you do not do this, the generated HTML
+%files will still be usable but may contain incomplete titles and lack
+%some hypertext links.
+%
+%It's also a good idea to set {\tt gif_path} which points to the
+%directory containing two GIF images used in the HTML
+%documents. Normally this is the {\tt Tools} subdirectory of Isabelle's
+%main directory. While its value in general is still valid, your HTML
+%files would depend on files not owned by you. This prevents you from
+%changing the location of the HTML files (as they contain relative
+%paths) and also causes trouble if the database's maker (re)moves the
+%GIFs.
+%
+%Here's what you should do before invoking {\tt init_html} using
+%someone else's \ML{} database:
+%
+%\begin{ttbox}
+%base_path := "/home/smith/isabelle";
+%gif_path := "/home/smith/isabelle/Tools";
+%init_html();
+%\dots
+%\end{ttbox}
-The above functions could be used in the following way:
-
-\begin{ttbox}
-init_html();
-{\out Setting path for index.html to "/home/clasohm/isabelle/HOL"}
-use_thy "List";
-\dots
-finish_html();
-\end{ttbox}
-
-Please note that HTML files are made only for those theories that are
-read while {\tt make_html} is {\tt true}. These files may contain
-links to theories that were read with a {\tt false} {\tt make_html}
-and therefore point to non-existing files.
-
-
-\subsection*{Extending or adding a logic}
-
-If you add a new subdirectory to Isabelle's logics (or add a completly
-new logic), you would have to call {\tt init_html} at the start of every
-directory's {\tt ROOT.ML} file and {\tt finish_html} at the end of
-it. This is automatically done if you use
-
-\begin{ttbox}\index{use_dir}
-use_dir : string -> unit
-\end{ttbox}
-
-This function takes a path as its parameter, changes the working
-directory, calls {\tt init_html} if {\tt make_html} is {\tt true},
-executes {\tt ROOT.ML}, and calls {\tt finish_html}. The {\tt
-index.html} file written in this directory will be automatically
-linked to the first index found in the (recursively searched)
-superdirectories.
-
-Instead of adding something like
-
-\begin{ttbox}
-use"ex/ROOT.ML";
-\end{ttbox}
-
-to the logic's makefile you have to use this:
-
-\begin{ttbox}
-use_dir"ex";
-\end{ttbox}
-
-Since {\tt use_dir} calls {\tt init_html} only if {\tt make_html} is
-{\tt true} the generation of HTML files depends on the value this
-reference variable has. It can either be inherited from the used \ML{}
-database or set in the makefile before {\tt use_dir} is invoked,
-e.g. to set it's value according to the environment variable {\tt
-MAKE_HTML}.
-
-The generated HTML files contain all theorems that were proved in the
-theory's \ML{} file with {\tt qed}, {\tt qed_goal} and {\tt qed_goalw},
-or stored with {\tt bind_thm} and {\tt store_thm}. Additionally there
-is a hypertext link to the whole \ML{} file.
-
-You can add section headings to the list of theorems by using
-
-\begin{ttbox}\index{use_dir}
-section: string -> unit
-\end{ttbox}
-
-in a theory's ML file, which converts a plain string to a HTML
-heading and inserts it before the next theorem proved or stored with
-one of the above functions. If {\tt make_html} is {\tt false} nothing
-is done.
-
-
-\subsection*{Using someone else's database}
-
-To make them independent from their storage place, the HTML files only
-contain relative paths which are derived from absolute ones like the
-current working directory, {\tt gif_path} or {\tt base_path}. The
-latter two are reference variables which are initialized at the time
-when the {\tt Pure} database is made. Because you need write access
-for the current directory to make HTML files and therefore (probably)
-generate them in your home directory, the absolute {\tt base_path} is
-not correct if you use someone else's database or a database derived
-from it.
-
-In that case you first should set {\tt base_path} to the value of {\em
-your} Isabelle main directory, i.e. the directory that contains the
-subdirectories where standard logics like {\tt FOL} and {\tt HOL} or
-your own logics are stored. If you do not do this, the generated HTML
-files will still be usable but may contain incomplete titles and lack
-some hypertext links.
-
-It's also a good idea to set {\tt gif_path} which points to the
-directory containing two GIF images used in the HTML
-documents. Normally this is the {\tt Tools} subdirectory of Isabelle's
-main directory. While its value in general is still valid, your HTML
-files would depend on files not owned by you. This prevents you from
-changing the location of the HTML files (as they contain relative
-paths) and also causes trouble if the database's maker (re)moves the
-GIFs.
-
-Here's what you should do before invoking {\tt init_html} using
-someone else's \ML{} database:
-
-\begin{ttbox}
-base_path := "/home/smith/isabelle";
-gif_path := "/home/smith/isabelle/Tools";
-init_html();
-\dots
-\end{ttbox}
\section{Terms}
\index{terms|bold}
Terms belong to the \ML\ type \mltydx{term}, which is a concrete datatype
-with six constructors: there are six kinds of term.
+with six constructors:
\begin{ttbox}
type indexname = string * int;
infix 9 $;
@@ -844,7 +870,7 @@
read_cterm : Sign.sg -> string * typ -> cterm
cert_axm : Sign.sg -> string * term -> string * term
read_axm : Sign.sg -> string * string -> string * term
-rep_cterm : cterm -> \{T:typ, t:term, sign:Sign.sg, maxidx:int\}
+rep_cterm : cterm -> {\ttlbrace}T:typ, t:term, sign:Sign.sg, maxidx:int\ttrbrace
\end{ttbox}
\begin{ttdescription}
\item[\ttindexbold{cterm_of} $sign$ $t$] \index{signatures}
@@ -932,7 +958,7 @@
\subsection{Making and inspecting certified types}
\begin{ttbox}
ctyp_of : Sign.sg -> typ -> ctyp
-rep_ctyp : ctyp -> \{T: typ, sign: Sign.sg\}
+rep_ctyp : ctyp -> {\ttlbrace}T: typ, sign: Sign.sg\ttrbrace
\end{ttbox}
\begin{ttdescription}
\item[\ttindexbold{ctyp_of} $sign$ $T$] \index{signatures}
@@ -968,7 +994,7 @@
\item[\ttindexbold{set_oracle} $fn$ $thy$] sets the oracle of theory $thy$ to
be $fn$. It is seldom called explicitly, as there is syntax for oracles in
- theory files. A theory can have at most one oracle.
+ theory files. Any theory node can have at most one oracle.
\end{ttdescription}
A curious feature of {\ML} exceptions is that they are ordinary constructors.