# HG changeset patch
# User wenzelm
# Date 881609389 -3600
# Node ID 429cba89b4c86343d3e54cfeecf8212ba9a86300
# Parent  25704541008b6f6e579dc4f8908fdb506e6e6d93
\subsection{*Theory inclusion};

diff -r 25704541008b -r 429cba89b4c8 doc-src/Ref/theories.tex
--- a/doc-src/Ref/theories.tex	Mon Dec 08 13:57:19 1997 +0100
+++ b/doc-src/Ref/theories.tex	Mon Dec 08 20:29:49 1997 +0100
@@ -406,6 +406,41 @@
 \hbox{\verb'?a=?b ==> ?b=?a  [!!a b. a=b ==> b=a]'}
 \end{ttdescription}
 
+
+\subsection{*Theory inclusion}
+\begin{ttbox}
+subthy      : theory * theory -> bool
+eq_thy      : theory * theory -> bool
+transfer    : theory -> thm -> thm
+transfer_sg : Sign.sg -> thm -> thm
+\end{ttbox}
+
+Inclusion and equality of theories is determined by unique
+identification stamps that are created when declaring new components.
+Theorems contain a reference to the theory (actually to its signature)
+they have been derived in.  Transferring theorems to super theories
+has no logical significance, but may affect some operations in subtle
+ways (e.g.\ implicit merges of signatures when applying rules, or
+pretty printing of theorems).
+
+\begin{ttdescription}
+
+\item[\ttindexbold{subthy} ($thy@1$, $thy@2$)] determines if $thy@1$
+  is included in $thy@2$ wrt.\ identification stamps.
+
+\item[\ttindexbold{eq_thy} ($thy@1$, $thy@2$)] determines if $thy@1$
+  is exactly the same as $thy@2$.
+
+\item[\ttindexbold{transfer} $thy$ $thm$] transfers theorem $thm$ to
+  theory $thy$, provided the latter includes the theory of $thm$.
+  
+\item[\ttindexbold{transfer_sg} $sign$ $thm$] is similar to
+  \texttt{transfer}, but identifies the super theory via its
+  signature.
+
+\end{ttdescription}
+
+
 \subsection{*Building a theory}
 \label{BuildingATheory}
 \index{theories!constructing|bold}