author nipkow Mon, 18 Jul 1994 12:22:30 +0200 changeset 478 838bd766d536 parent 477 53fc8ad84b33 child 479 db5a95f2952e
 doc-src/Ref/theories.tex file | annotate | diff | comparison | revisions
--- a/doc-src/Ref/theories.tex	Fri Jul 15 13:34:31 1994 +0200
+++ b/doc-src/Ref/theories.tex	Mon Jul 18 12:22:30 1994 +0200
@@ -2,7 +2,7 @@

\chapter{Theories, Terms and Types} \label{theories}
\index{theories|(}\index{signatures|bold}
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}.
@@ -196,12 +196,11 @@
the new theory.

Special applications, such as \ZF's inductive definition package, construct
-theories directly by calling the \ML{} function {\tt extend_theory}.  In
-this situation there is no {\tt.thy} file, only an {\tt.ML} file.  The
-{\tt.ML} file must declare an \ML\ structure having the theory's name.  See
-the file {\tt ZF/ex/LList.ML} for an example.
-Section~\ref{sec:pseudo-theories} below describes a way of linking such
-theories to their parents.
+theories directly by calling \ML\ functions.  In this situation there is no
+{\tt.thy} file, only an {\tt.ML} file.  The {\tt.ML} file must declare an
+\ML\ structure having the theory's name.  See the file {\tt ZF/ex/LList.ML}
+for an example.  Section~\ref{sec:pseudo-theories} below describes a way of
+linking such theories to their parents.

\begin{warn}
Temporary files are written to the current directory, which therefore must
@@ -248,18 +247,11 @@
Poly/\ML{} session, the contents of references are lost unless they are
declared in the current database.  Assignments to references in the {\tt
-
-To avoid losing such information you must declare a new {\tt Readthy}
-structure in the child database:
+To avoid losing this information simply call
\begin{ttbox}
\end{ttbox}
-The assignment copies into the new reference \verb$loaded_thys$ the
-contents of the original reference, which is the list of already loaded
-theories.  You should not omit the declarations even if the parent database
-has no loaded theories, since they allocate new references.
+when building the new database.

\subsection{*Pseudo theories}\label{sec:pseudo-theories}
@@ -337,7 +329,6 @@
\begin{ttbox}
pure_thy       : theory
merge_theories : theory * theory -> theory
-extend_theory  : theory -> string -> $$\cdots$$ -> theory
\end{ttbox}
\begin{ttdescription}
\item[\ttindexbold{pure_thy}] contains just the types, constants, and syntax
@@ -347,12 +338,13 @@
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"} $\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
+%\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
+%extend_theory  : theory -> string -> $$\cdots$$ -> theory
\begin{ttbox}
Attempt to merge different versions of theory: $$T$$
\end{ttbox}
@@ -409,9 +401,7 @@
returns the axioms of~$thy$ and its ancestors.

\item[\ttindexbold{parents_of} $thy$]
-returns the parents of~$thy$.  This list contains zero, one or two
-elements, depending upon whether $thy$ is {\tt pure_thy},
-\hbox{\tt extend_theory $thy$} or \hbox{\tt merge_theories ($thy@1$, $thy@2$)}.
+returns the complete list of ancestors of~$thy$.

\item[\ttindexbold{stamps_of_thy} $thy$]\index{signatures}
returns the \rmindex{stamps} of the signature associated with~$thy$.