# HG changeset patch
# User nipkow
# Date 762538907 -3600
# Node ID 933ec96c522e205c1a01ba7db695bb71e0bf6d37
# Parent  dc87495814d5cd3b4e491dbd5568b4ce07ede225
update towards LNCS

diff -r dc87495814d5 -r 933ec96c522e doc-src/Ref/theories.tex
--- a/doc-src/Ref/theories.tex	Tue Mar 01 16:00:53 1994 +0100
+++ b/doc-src/Ref/theories.tex	Tue Mar 01 17:21:47 1994 +0100
@@ -5,22 +5,22 @@
 \index{reading!axioms|see{{\tt extend_theory} and {\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 \ttindex{theory}.
+and merging existing theories.  They have the \ML\ type \ttindex{theory}.
 Theory operations signal errors by raising exception \ttindex{THEORY},
 returning a message and a list of theories.
 
 Signatures, which contain information about sorts, types, constants and
-syntax, have the \ML{} type~\ttindexbold{Sign.sg}.  For identification,
-each signature carries a unique list of {\bf stamps}, which are~\ML{}
+syntax, have the \ML\ type~\ttindexbold{Sign.sg}.  For identification,
+each signature carries a unique list of {\bf stamps}, which are \ML\
 references (to strings).  The strings serve as human-readable names; the
 references serve as unique identifiers.  Each primitive signature has a
 single stamp.  When two signatures are merged, their lists of stamps are
 also merged.  Every theory carries a unique signature.
 
 Terms and types are the underlying representation of logical syntax.  Their
-\ML{} definitions are irrelevant to naive Isabelle users.  Programmers who wish
-to extend Isabelle may need to know such details, say to code a tactic that
-looks for subgoals of a particular form.  Terms and types may be
+\ML\ definitions are irrelevant to naive Isabelle users.  Programmers who
+wish to extend Isabelle may need to know such details, say to code a tactic
+that looks for subgoals of a particular form.  Terms and types may be
 `certified' to be well-formed with respect to a given signature.
 
 \section{Defining Theories}
@@ -28,32 +28,25 @@
 
 Theories can be defined either using concrete syntax or by calling certain
 \ML-functions (see \S\ref{BuildingATheory}).  Appendix~\ref{TheorySyntax}
-presents the concrete syntax for theories.
-This grammar employs the
-following conventions: 
+presents the concrete syntax for theories following convention that
 \begin{itemize}
-\item Identifiers such as {\it theoryDef} denote nonterminal symbols.
-\item Text in {\tt typewriter font} denotes terminal symbols.
-\item $id$ is an Isabelle identifier.
-\item $string$ is an ML string, with its quotation marks.
-\item $nat$ is for a natural number.
-\item $tfree$ is an Isabelle type variable, i.e.\ an identifier starting with
-  a prime.
-\item $text$ stands for arbitrary ML text.
+\item {\tt typewriter font} denotes terminal symbols;
+\item $id$, $tid$, $nat$, $string$ and $text$ are the lexical classes of
+  identifiers, type identifiers, natural numbers, \ML\ strings (with their
+  quotation marks) and arbitrary \ML\ text. The first three are fully defined
+  in the {\it Defining Logics} chapter of {\it Isabelle's Object Logics}.
 \end{itemize}
 The different parts of a theory definition are interpreted as follows:
 \begin{description} 
 \item[{\it theoryDef}] A theory has a name $id$ and is an extension of the
-  union of theories {\it name}, the {\em parent theories}, with new classes,
-  types, constants, syntax and axioms.  The basic theory, which contains only
-  the meta-logic, is called {\tt Pure}.
+  union of theories with name {\it name}, the {\bf parent
+    theories}\indexbold{theories!parent}, with new classes, types, constants,
+  syntax and axioms.  The basic theory, which contains only the meta-logic,
+  is called {\tt Pure}.
 
-  If {\it name} is a string, then theory {\it name} is {\em not} used in
-  building the base of theory $id$. Strings stand for ML-files rather than
-  theory-files and document the dependence of $id$ on additional files. This
-  enables all required files, namely those corresponding to {\it name}s, to
-  be loaded automatically when theory $id$ is (re)built. See
-  Chapter~\ref{LoadingTheories} for details.
+  Normally each {\it name\/} is an identifier, the precise name of the parent
+  theory. Strings can be used to document additional dependencies; see
+  \S\ref{LoadingTheories} for details.
 \item[$classes$] {\tt$id$ < $id@1$ \dots\ $id@n$} declares $id$ as a subclass
   of existing classes $id@1\dots id@n$.  This rules out cyclic class
   structures.  Isabelle automatically computes the transitive closure of
@@ -68,54 +61,56 @@
   singleton set {\tt\{}$id${\tt\}}.
 \item[$type$] is either the declaration of a new type (constructor) or type
   synonym $name$. Only binary type constructors can have infix status and
-  symbolic names, e.g.\ {\tt ('a,'b)"+"}. Type constructors of $n$ arguments
-  are declared by {\tt ($\alpha@1$,\dots,$\alpha@n$)$name$}.  Type
-  synonyms\indexbold{type!synonym} are defined as in ML, except that the
-  right-hand side must be enclosed in quotation marks.
+  symbolic names, e.g.\ {\tt ('a,'b)"*"}. Type constructors of $n$ arguments
+  are declared by $(\alpha@1,\dots,\alpha@n)name$.  A {\bf type
+    synonym}\indexbold{type!synonym} is simply an abbreviation
+  $(\alpha@1,\dots,\alpha@n)name = \mbox{\tt"}\tau\mbox{\tt"}$ and follows
+  the same rules as in \ML, except that $name$ can be a string and $\tau$
+  must be enclosed in quotation marks.
 \item[$infix$] declares a type or constant to be an infix operator of
   precedence $nat$ associating to the left ({\tt infixl}) or right ({\tt
     infixr}).
 \item[$arities$] Each $name$ must be an existing type constructor which is
   given the additional arity $arity$.
 \item[$constDecl$] Each new constant $name$ is declared to be of type
-  $string$.  For display purposes they can be annotated with $mixfix$
-  declarations.
+  $string$.  For display purposes $mixfix$ annotations can be attached.
 \item[$mixfix$] There are three forms of syntactic annotations:
   \begin{itemize}
   \item A mixfix template given as a $string$ of the form
     {\tt"}\dots{\tt\_}\dots{\tt\_}\dots{\tt"} where the $i$-th underscore
     indicates the position where the $i$-th argument should go. The minimal
     precedence of each argument is given by a list of natural numbers, the
-    precedence of the construct by the following natural number; precedences
-    are optional.
+    precedence of the whole construct by the following natural number;
+    precedences are optional.
 
   \item Binary constants can be given infix status.
 
   \item A constant $f$ {\tt::} $(\tau@1\To\tau@2)\To\tau@3$ can be given {\em
-    binder} status: {\tt binder} $Q$ $p$ causes $Q\,x.F(x)$ to be treated
+    binder\/} status: {\tt binder} $Q$ $p$ causes $Q\,x.F(x)$ to be treated
   like $f(F)$; $p$ is the precedence of the construct.
   \end{itemize}
 \item[$trans$] Specifies syntactic translation rules, that is parse 
   rules ({\tt =>}), print rules ({\tt <=}), or both ({\tt ==}).
 \item[$rule$] A rule consists of a name $id$ and a formula $string$.  Rule
   names must be distinct.
-\item[$ml$] This final part of a theory consists of ML code, 
+\item[$ml$] This final part of a theory consists of \ML\ code, 
   typically for parse and print translations.
 \end{description}
 The $mixfix$, $trans$ and $ml$ sections are explained in more detail in 
-the {\it Defining Logics} chapter of the {\it Logics} manual.
+the {\it Defining Logics} chapter of {\it Isabelle's Object Logics}.
 
 
-\subsection{Classes and types}
+\subsection{*Classes and arities}
+\index{*classes!context conditions}
 \index{*arities!context conditions}
 
-Type declarations are subject to the following two well-formedness
+Classes and arities are subject to the following two well-formedness
 conditions:
 \begin{itemize}
 \item There are no two declarations $ty :: (\vec{r})c$ and $ty :: (\vec{s})c$
   with $\vec{r} \neq \vec{s}$.  For example
 \begin{ttbox}
-types ty 1
+types 'a ty
 arities ty :: ({\ttlbrace}logic{\ttrbrace}) logic
         ty :: ({\ttlbrace}{\ttrbrace})logic
 \end{ttbox}
@@ -128,7 +123,7 @@
 types represented by $s$.  For example
 \begin{ttbox}
 classes term < logic
-types ty 1
+types 'a ty
 arities ty :: ({\ttlbrace}logic{\ttrbrace})logic
         ty :: ({\ttlbrace}{\ttrbrace})term
 \end{ttbox}
@@ -139,48 +134,54 @@
 
 \section{Loading Theories}
 \label{LoadingTheories}
+\index{theories!loading|(}
+
 \subsection{Reading a new theory}
 
 Each theory definition must reside in a separate file.  Let the file {\it
   tf}{\tt.thy} contain the definition of a theory called $TF$ with parent
 theories $TB@1$ \dots $TB@n$.  Calling \ttindexbold{use_thy}~{\tt"}{\it
-  TF\/}{\tt"} reads file {\it tf}{\tt.thy}, writes an intermediate {\ML}-file
-{\tt.}{\it tf}{\tt.thy.ML}, and reads the latter file. \indexbold{automatic
-loading}  Any of the parent theories that have not been loaded yet are read now
-by recursive {\tt use_thy} calls until either an already loaded theory or {\tt
-  Pure} is reached.  Therefore one can read a complete logic by just one {\tt
-use_thy} call if all theories are linked appropriately.  Afterwards an {\ML}
+  TF\/}{\tt"} reads file {\it tf}{\tt.thy}, writes an intermediate \ML-file
+{\tt.}{\it tf}{\tt.thy.ML}, and reads the latter file. Any of the parent
+theories that have not been loaded yet are read now by recursive {\tt
+  use_thy} calls until either an already loaded theory or {\tt Pure} is
+reached.  Therefore one can read a complete logic by just one {\tt use_thy}
+call if all theories are linked appropriately.  Afterwards an \ML\ 
 structure~$TF$ containing a component {\tt thy} for the new theory and
 components $r@1$ \dots $r@n$ for the rules is declared; it also contains the
 definitions of the {\tt ML} section if any. Unless
-\ttindexbold{delete_tmpfiles} is set to {\tt false}, {\tt.}{\it tf}{\tt.thy.ML}
-is deleted if no errors occurred. Finally the file {\it tf}{\tt.ML} is read, if
-it exists; this file normally contains proofs involving the new theory.
+\ttindexbold{delete_tmpfiles} is set to {\tt false}, {\tt.}{\it
+  tf}{\tt.thy.ML} is deleted if no errors occurred. Finally the file {\it
+  tf}{\tt.ML} is read, if it exists; this file normally contains proofs
+involving the new theory.
 
 
-\subsection{Filenames and paths}
-\indexbold{filenames}
+\subsection{Theory names, file names and search paths}
+\indexbold{theories!names of}
+\indexbold{files!names of}
+\indexbold{search path}
 
 \begin{warn}
   The files defining the theory must have the lower case name of the theory
-  with {\tt".thy"} or {\tt".ML"} appended.  On the other hand
-  \ttindex{use_thy}'s parameter has to be the exact theory name.
+  with {\tt.thy} or {\tt.ML} appended.  On the other hand \ttindex{use_thy}'s
+  parameter has to be the exact theory name.
 \end{warn}
 Optionally the name can be preceded by a path to specify the directory where
 the files can be found.  If no path is provided the reference variable
 \ttindexbold{loadpath} is used which contains a list of paths that are
-searched in the given order.  After the {\tt".thy"}-file for a theory has
-been found, the same path is used to locate the (optional) {\tt".ML"}-file.
+searched in the given order.  After the {\tt.thy}-file for a theory has
+been found, the same path is used to locate the (optional) {\tt.ML}-file.
 
-It is also possible to provide only a {\tt".ML"}-file, with no
-{\tt".thy"}-file.  In this case the {\tt".ML"}-file must declare an \ML{}
-structure having the theory's name.  If both the {\tt".thy"}-file and a
-structure declaration in the {\tt".ML"}-file exist, then the latter
+It is also possible to provide only a {\tt.ML}-file, with no
+{\tt.thy}-file.  In this case the {\tt.ML}-file must declare an \ML\
+structure having the theory's name.  If both the {\tt.thy}-file and a
+structure declaration in the {\tt.ML}-file exist, then the latter
 declaration is used.  See {\tt ZF/ex/llist.ML} for an example.
 
 
 \subsection{Reloading a theory}
-\index{reloading a theory}
+\indexbold{theories!reloading}
+\index{*update|(}
 
 \ttindex{use_thy} keeps track of all loaded theories and stores information
 about their files.  If it finds that the theory to be loaded was already read
@@ -190,75 +191,77 @@
   use_thy} stops if they are equal. In case the files have been moved, {\tt
   use_thy} searches them the same way a new theory would be searched for.
 After all these tests have been passed, the theory is reloaded and all
-theories that depend on it (those that have its name in their {\it
-  theoryDef}) are marked as out-of-date.
+its children are marked as out-of-date.
 \begin{warn}
   Changing a theory on disk often makes it necessary to reload all theories
-  that (indirectly) depend on it. However, {\tt use_thy} reads only one
-  theory, even if some of the parents are out of date. In this case
-  \ttindexbold{update}{\tt()} should be used.  This function reloads {\em all}
+  that directly or indirectly depend on it. However, {\tt use_thy} reads only
+  one theory, even if some of the parent theories are out of date. In this
+  case {\tt update()} should be used.  This function reloads {\em all\/}
   modified theories and their descendants in the correct order.
 \end{warn}
 
 
-\subsection{Pseudo theories}
-\indexbold{pseudo theories}
+\subsection{*Pseudo theories}
+\indexbold{theories!pseudo}
 
-There is a problem with \ttindex{update}: objects created in \ML-files that
-do not belong to a theory (see explanation of {\it theoryDef} in
-\ref{DefiningTheories}).  These files are read manually between {\tt use_thy}
-calls and define objects used in different theories.  As {\tt update} only
-knows about the theories there still exist objects with references to the old
-theory version after the new one has been read.  This (most probably) will
-produce the fatal error
-\begin{center} \tt
-Attempt to merge different versions of theory: $T$
-\end{center}
+Any automatic reloading facility requires complete knowledge of all
+dependencies. Sometimes theories depend on objects created in \ML-files
+without associated {\tt.thy}-file. Unless such dependencies are documented,
+{\tt update} fails to reload these \ML-files and the system is left in a
+state where some objects, e.g.\ theorems, still refer to old versions of
+theories. This may lead to the error
+\begin{ttbox}
+Attempt to merge different versions of theory: \(T\)
+\end{ttbox}
+Therefore there is a way to link theories and {\em orphaned\/} \ML-files,
+i.e.\ those without associated {\tt.thy}-file.
 
-Therefore there is a way to link theories and the $orphaned$ \ML-files. The
-link from a theory to an \ML-file has been mentioned in
-Chapter~\ref{DefiningTheories} (strings in {\it theoryDef}).  But to make this
-work and to establish a link in the opposite direction we need to create a
-{\it pseudo theory}.  Let's assume we have an \ML-file named {\tt orphan.ML}
-that depends on theory $A$ and is itself used in theory $B$.  To link the
-three we have to create the file {\tt orphan.thy} containing the line
+Let us assume we have an orphaned \ML-file named {\tt orphan.ML} and a theory
+$B$ which depends on {\tt orphan.ML} (for example, {\tt b.ML} uses theorems
+that are proved in {\tt orphan.ML}). Then {\tt b.thy} should mention this
+dependence:
 \begin{ttbox}
-orphan = A
+B = ... + "orphan" + ...
 \end{ttbox}
-and add {\tt "orphan"} to the list of $B$'s parents.
-% Creating {\tt orphan.thy} is necessary because of two reasons: First it
-% enables automatic loading of $orphan$'s parents and second it creates the
-% \ML{}-object {\tt orphan} that is needed by {\tt use_thy} (though it is not
-% added to the base of theory $B$).
-Creating {\tt orphan.thy} enables automatic loading of $orphan$'s parents.
-If {\tt orphan.ML} depended on no theory then {\tt Pure} should have been
-used instead of {\tt A}.
+Although {\tt orphan} is {\em not\/} used in building the base of theory $B$
+(strings stand for \ML-files rather than {\tt.thy}-files and merely document
+additional dependencies), {\tt orphan.ML} is loaded automatically when $B$ is
+(re)built.
+
+If {\tt orphan.ML} depends on theories $A@1\dots A@n$, this should be recorded
+by creating a {\bf pseudo theory} in the file {\tt orphan.thy}:
+\begin{ttbox}
+orphan = A1 + \(...\) + An
+\end{ttbox}
+The resulting theory is never used but guarantees that {\tt update} reloads
+theory {\it orphan} whenever it reloads one of the $A@i$.
 
 For an extensive example of how this technique can be used to link over 30
-files and read them by just two {\tt use_thy} calls have a look at the ZF
-logic.
+files and load them by just two {\tt use_thy} calls, consult the ZF source
+files.
+\index{theories!loading|)}
 
 
 \subsection{Removing a theory}
-\index{removing theories}
+\indexbold{theories!removing}
 
-If a previously read file is removed the \ttindex{update} function will keep
-on complaining about a missing file.  The theory is not automatically removed
-from the internal list to preserve the links to other theories in case one
-forgot to adjust the {\tt loadpath} after moving a file.  To manually remove a
-theory use \ttindexbold{unlink_thy}.
+If a previously read file is removed, {\tt update} will keep on complaining
+about a missing file.  The theory is not automatically removed from the
+internal list to preserve the links to other theories in case one forgot to
+adjust the {\tt loadpath} after moving a file.  To remove a theory manually
+use \ttindexbold{unlink_thy}.  \index{*update|)}
 
 
 \subsection{Using Poly/\ML}
 \index{Poly/\ML}
 \index{reference variables}
 
-As the functions for reading theories depend on reference variables one has to
-take into consideration the way Poly/\ML{} handles them.  They are only saved
-together with the state if they were declared in the current database.  E.g.
-changes made to a reference variable declared in the $Pure$ database are $not$
-saved if made while using a child database.  Therefore a new {\tt Readthy}
-structure has to be created by
+As the functions for reading theories depend on reference variables one has
+to take into account the way Poly/\ML\ handles them.  They are only saved
+together with the state if they were declared in the current database.  For
+example, changes made to a reference variable declared in the {\tt Pure}
+database are {\em not\/} saved if made while using a child database.
+Therefore a new {\tt Readthy} structure has to be created by
 \begin{ttbox}
 structure Readthy = ReadthyFUN (structure ThySyn = ThySyn);
 Readthy.loaded_thys := !loaded_thys;
@@ -295,22 +298,83 @@
 \hbox{\tt\frenchspacing ?a=?b ==> ?b=?a  [!!a b. a=b ==> b=a]}
 \end{description}
 
+%\subsection{Building a theory}
+%\label{BuildingATheory}
+%\index{theories!constructing|bold}
+%\begin{ttbox} 
+%pure_thy: theory
+%merge_theories: theory * theory -> theory
+%extend_theory: theory -> string
+%        -> (class * class list) list 
+%           * sort
+%           * (string list * int)list
+%           * (string list * (sort list * class))list
+%           * (string list * string)list * sext option
+%        -> (string*string)list -> theory
+%\end{ttbox}
+%Type \ttindex{class} is a synonym for {\tt string}; type \ttindex{sort} is
+%a synonym for \hbox{\tt class list}.
+%\begin{description}
+%\item[\ttindexbold{pure_thy}] contains just the types, constants, and syntax
+%  of the meta-logic.  There are no axioms: meta-level inferences are carried
+%  out by \ML\ functions.
+%\item[\ttindexbold{merge_theories} ($thy@1$, $thy@2$)] merges the two
+%  theories $thy@1$ and $thy@2$.  The resulting theory contains all types,
+%  constants and axioms of the constituent theories; its default sort is the
+%  union of the default sorts of the constituent theories.
+%\item [\ttindexbold{extend_theory} $thy$ {\tt"}$T${\tt"}
+%      ($classes$, $default$, $types$, $arities$, $consts$, $sextopt$) $rules$]
+%\hfill\break   %%% include if line is just too short
+%is the \ML-equivalent of the following theory definition:
+%\begin{ttbox}
+%\(T\) = \(thy\) +
+%classes \(c\) < \(c@1\),\(\dots\),\(c@m\)
+%        \dots
+%default {\(d@1,\dots,d@r\)}
+%types   \(tycon@1\),\dots,\(tycon@i\) \(n\)
+%        \dots
+%arities \(tycon@1'\),\dots,\(tycon@j'\) :: (\(s@1\),\dots,\(s@n\))\(c\)
+%        \dots
+%consts  \(b@1\),\dots,\(b@k\) :: \(\tau\)
+%        \dots
+%rules   \(name\) \(rule\)
+%        \dots
+%end
+%\end{ttbox}
+%where
+%\begin{tabular}[t]{l@{~=~}l}
+%$classes$ & \tt[("$c$",["$c@1$",\dots,"$c@m$"]),\dots] \\
+%$default$ & \tt["$d@1$",\dots,"$d@r$"]\\
+%$types$   & \tt[([$tycon@1$,\dots,$tycon@i$], $n$),\dots] \\
+%$arities$ & \tt[([$tycon'@1$,\dots,$tycon'@j$], ([$s@1$,\dots,$s@n$],$c$)),\dots]
+%\\
+%$consts$  & \tt[([$b@1$,\dots,$b@k$],$\tau$),\dots] \\
+%$rules$   & \tt[("$name$",$rule$),\dots]
+%\end{tabular}
+%
+%If theories are defined as in \S\ref{DefiningTheories}, new syntax is added
+%as mixfix annotations to constants.  Using {\tt extend_theory}, new syntax can
+%be added via $sextopt$ which is either {\tt None}, or {\tt Some($sext$)}.  The
+%latter case is not documented.
+%
+%$T$ identifies the theory internally.  When a theory is redeclared, say to
+%change an incorrect axiom, bindings to the old axiom may persist.  Isabelle
+%ensures that the old and new theories are not involved in the same proof.
+%Attempting to combine different theories having the same name $T$ yields the
+%fatal error
+%\begin{ttbox}
+%Attempt to merge different versions of theory: \(T\)
+%\end{ttbox}
+%\end{description}
+
 \subsection{Building a theory}
 \label{BuildingATheory}
 \index{theories!constructing|bold}
 \begin{ttbox} 
 pure_thy: theory
 merge_theories: theory * theory -> theory
-extend_theory: theory -> string
-        -> (class * class list) list 
-           * sort
-           * (string list * int)list
-           * (string list * (sort list * class))list
-           * (string list * string)list * sext option
-        -> (string*string)list -> theory
+extend_theory: theory -> string -> \(\cdots\) -> theory
 \end{ttbox}
-Type \ttindex{class} is a synonym for {\tt string}; type \ttindex{sort} is
-a synonym for \hbox{\tt class list}.
 \begin{description}
 \item[\ttindexbold{pure_thy}] contains just the types, constants, and syntax
   of the meta-logic.  There are no axioms: meta-level inferences are carried
@@ -319,49 +383,15 @@
   theories $thy@1$ and $thy@2$.  The resulting theory contains all types,
   constants and axioms of the constituent theories; its default sort is the
   union of the default sorts of the constituent theories.
-\item [\ttindexbold{extend_theory} $thy$ {\tt"}$T${\tt"}
-      ($classes$, $default$, $types$, $arities$, $consts$, $sextopt$) $rules$]
-\hfill\break   %%% include if line is just too short
-is the \ML-equivalent of the following theory definition:
+\item [\ttindexbold{extend_theory} $thy$ {\tt"}$T${\tt"} $\cdots$] extends
+  the theory $thy$ with new types, constants, etc.  $T$ identifies the theory
+  internally.  When a theory is redeclared, say to change an incorrect axiom,
+  bindings to the old axiom may persist.  Isabelle ensures that the old and
+  new theories are not involved in the same proof.  Attempting to combine
+  different theories having the same name $T$ yields the fatal error
 \begin{ttbox}
-\(T\) = \(thy\) +
-classes \(c\) < \(c@1\),\(\dots\),\(c@m\)
-        \dots
-default {\(d@1,\dots,d@r\)}
-types   \(tycon@1\),\dots,\(tycon@i\) \(n\)
-        \dots
-arities \(tycon@1'\),\dots,\(tycon@j'\) :: (\(s@1\),\dots,\(s@n\))\(c\)
-        \dots
-consts  \(b@1\),\dots,\(b@k\) :: \(\tau\)
-        \dots
-rules   \(name\) \(rule\)
-        \dots
-end
+Attempt to merge different versions of theory: \(T\)
 \end{ttbox}
-where
-\begin{tabular}[t]{l@{~=~}l}
-$classes$ & \tt[("$c$",["$c@1$",\dots,"$c@m$"]),\dots] \\
-$default$ & \tt["$d@1$",\dots,"$d@r$"]\\
-$types$   & \tt[([$tycon@1$,\dots,$tycon@i$], $n$),\dots] \\
-$arities$ & \tt[([$tycon'@1$,\dots,$tycon'@j$], ([$s@1$,\dots,$s@n$],$c$)),\dots]
-\\
-$consts$  & \tt[([$b@1$,\dots,$b@k$],$\tau$),\dots] \\
-$rules$   & \tt[("$name$",$rule$),\dots]
-\end{tabular}
-
-If theories are defined as in \S\ref{DefiningTheories}, new syntax is added
-as mixfix annotations to constants.  Using {\tt extend_theory}, new syntax can
-be added via $sextopt$ which is either {\tt None}, or {\tt Some($sext$)}.  The
-latter case is not documented.
-
-$T$ identifies the theory internally.  When a theory is redeclared, say to
-change an incorrect axiom, bindings to the old axiom may persist.  Isabelle
-ensures that the old and new theories are not involved in the same proof.
-Attempting to combine different theories having the same name $T$ yields the
-fatal error
-\begin{center} \tt
-Attempt to merge different versions of theory: $T$
-\end{center}
 \end{description}
 
 
@@ -400,7 +430,7 @@
 
 \section{Terms}
 \index{terms|bold}
-Terms belong to the \ML{} type \ttindexbold{term}, which is a concrete datatype
+Terms belong to the \ML\ type \ttindexbold{term}, which is a concrete datatype
 with six constructors: there are six kinds of term.
 \begin{ttbox}
 type indexname = string * int;
@@ -445,7 +475,7 @@
 is the {\bf application} of~$t$ to~$u$.  
 \end{description}
 Application is written as an infix operator in order to aid readability.
-For example, here is an \ML{} pattern to recognize first-order formula of
+For example, here is an \ML\ pattern to recognize first-order formula of
 the form~$A\imp B$, binding the subformulae to~$A$ and~$B$:
 \begin{ttbox} 
 Const("Trueprop",_) $ (Const("op -->",_) $ A $ B)
@@ -462,18 +492,18 @@
 binding using de Bruijn indexes.} Meta-rules such as {\tt forall_elim} take
 certified terms as arguments.
 
-Certified terms belong to the abstract type \ttindexbold{Sign.cterm}.
+Certified terms belong to the abstract type \ttindexbold{cterm}.
 Elements of the type can only be created through the certification process.
 In case of error, Isabelle raises exception~\ttindex{TERM}\@.
 
 \subsection{Printing terms}
 \index{printing!terms|bold}
 \begin{ttbox} 
-Sign.string_of_cterm :      Sign.cterm -> string
+     string_of_cterm :           cterm -> string
 Sign.string_of_term  : Sign.sg -> term -> string
 \end{ttbox}
 \begin{description}
-\item[\ttindexbold{Sign.string_of_cterm} $ct$] 
+\item[\ttindexbold{string_of_cterm} $ct$] 
 displays $ct$ as a string.
 
 \item[\ttindexbold{Sign.string_of_term} $sign$ $t$] 
@@ -482,21 +512,20 @@
 
 \subsection{Making and inspecting certified terms}
 \begin{ttbox} 
-Sign.cterm_of   : Sign.sg -> term -> Sign.cterm
-Sign.read_cterm : Sign.sg -> string * typ -> Sign.cterm
-Sign.rep_cterm  : Sign.cterm -> \{T:typ, t:term, 
-                                 sign: Sign.sg, maxidx:int\}
+cterm_of   : Sign.sg -> term -> cterm
+read_cterm : Sign.sg -> string * typ -> cterm
+rep_cterm  : cterm -> \{T:typ, t:term, sign:Sign.sg, maxidx:int\}
 \end{ttbox}
 \begin{description}
-\item[\ttindexbold{Sign.cterm_of} $sign$ $t$] \index{signatures}
+\item[\ttindexbold{cterm_of} $sign$ $t$] \index{signatures}
 certifies $t$ with respect to signature~$sign$.
 
-\item[\ttindexbold{Sign.read_cterm} $sign$ ($s$, $T$)] 
+\item[\ttindexbold{read_cterm} $sign$ ($s$, $T$)] 
 reads the string~$s$ using the syntax of~$sign$, creating a certified term.
 The term is checked to have type~$T$; this type also tells the parser what
 kind of phrase to parse.
 
-\item[\ttindexbold{Sign.rep_cterm} $ct$] 
+\item[\ttindexbold{rep_cterm} $ct$] 
 decomposes $ct$ as a record containing its type, the term itself, its
 signature, and the maximum subscript of its unknowns.  The type and maximum
 subscript are computed during certification.
@@ -505,7 +534,7 @@
 
 \section{Types}
 \index{types|bold}
-Types belong to the \ML{} type \ttindexbold{typ}, which is a concrete
+Types belong to the \ML\ type \ttindexbold{typ}, which is a concrete
 datatype with three constructors.  Types are classified by sorts, which are
 lists of classes.  A class is represented by a string.
 \begin{ttbox}
@@ -541,16 +570,16 @@
 \section{Certified types}
 \index{types!certified|bold}
 Certified types, which are analogous to certified terms, have type 
-\ttindexbold{Sign.ctyp}.
+\ttindexbold{ctyp}.
 
 \subsection{Printing types}
 \index{printing!types|bold}
 \begin{ttbox} 
-Sign.string_of_ctyp :      Sign.ctyp -> string
+     string_of_ctyp :           ctyp -> string
 Sign.string_of_typ  : Sign.sg -> typ -> string
 \end{ttbox}
 \begin{description}
-\item[\ttindexbold{Sign.string_of_ctyp} $cT$] 
+\item[\ttindexbold{string_of_ctyp} $cT$] 
 displays $cT$ as a string.
 
 \item[\ttindexbold{Sign.string_of_typ} $sign$ $T$] 
@@ -560,14 +589,14 @@
 
 \subsection{Making and inspecting certified types}
 \begin{ttbox} 
-Sign.ctyp_of  : Sign.sg -> typ -> Sign.ctyp
-Sign.rep_ctyp : Sign.ctyp -> \{T: typ, sign: Sign.sg\}
+ctyp_of  : Sign.sg -> typ -> ctyp
+rep_ctyp : ctyp -> \{T: typ, sign: Sign.sg\}
 \end{ttbox}
 \begin{description}
-\item[\ttindexbold{Sign.ctyp_of} $sign$ $T$] \index{signatures}
+\item[\ttindexbold{ctyp_of} $sign$ $T$] \index{signatures}
 certifies $T$ with respect to signature~$sign$.
 
-\item[\ttindexbold{Sign.rep_ctyp} $cT$] 
+\item[\ttindexbold{rep_ctyp} $cT$] 
 decomposes $cT$ as a record containing the type itself and its signature.
 \end{description}