# HG changeset patch
# User wenzelm
# Date 1307376338 -7200
# Node ID 7860ffc5ec08fd3a396ff4a1290739568472df30
# Parent  34ed34804d90ea033fc755d946d6f7cdeee6b507
modernized and re-unified Thm.transfer;

diff -r 34ed34804d90 -r 7860ffc5ec08 doc-src/IsarImplementation/Thy/Logic.thy
--- a/doc-src/IsarImplementation/Thy/Logic.thy	Mon Jun 06 17:51:14 2011 +0200
+++ b/doc-src/IsarImplementation/Thy/Logic.thy	Mon Jun 06 18:05:38 2011 +0200
@@ -634,6 +634,7 @@
   \begin{mldecls}
   @{index_ML_type thm} \\
   @{index_ML proofs: "int Unsynchronized.ref"} \\
+  @{index_ML Thm.transfer: "theory -> thm -> thm"} \\
   @{index_ML Thm.assume: "cterm -> thm"} \\
   @{index_ML Thm.forall_intr: "cterm -> thm -> thm"} \\
   @{index_ML Thm.forall_elim: "cterm -> thm -> thm"} \\
@@ -682,6 +683,13 @@
   records full proof terms.  Officially named theorems that contribute
   to a result are recorded in any case.
 
+  \item @{ML Thm.transfer}~@{text "thy thm"} transfers the given
+  theorem to a \emph{larger} theory, see also \secref{sec:context}.
+  This formal adjustment of the background context has no logical
+  significance, but is occasionally required for formal reasons, e.g.\
+  when theorems that are imported from more basic theories are used in
+  the current situation.
+
   \item @{ML Thm.assume}, @{ML Thm.forall_intr}, @{ML
   Thm.forall_elim}, @{ML Thm.implies_intr}, and @{ML Thm.implies_elim}
   correspond to the primitive inferences of \figref{fig:prim-rules}.
diff -r 34ed34804d90 -r 7860ffc5ec08 doc-src/IsarImplementation/Thy/document/Logic.tex
--- a/doc-src/IsarImplementation/Thy/document/Logic.tex	Mon Jun 06 17:51:14 2011 +0200
+++ b/doc-src/IsarImplementation/Thy/document/Logic.tex	Mon Jun 06 18:05:38 2011 +0200
@@ -705,6 +705,7 @@
   \begin{mldecls}
   \indexdef{}{ML type}{thm}\verb|type thm| \\
   \indexdef{}{ML}{proofs}\verb|proofs: int Unsynchronized.ref| \\
+  \indexdef{}{ML}{Thm.transfer}\verb|Thm.transfer: theory -> thm -> thm| \\
   \indexdef{}{ML}{Thm.assume}\verb|Thm.assume: cterm -> thm| \\
   \indexdef{}{ML}{Thm.forall\_intr}\verb|Thm.forall_intr: cterm -> thm -> thm| \\
   \indexdef{}{ML}{Thm.forall\_elim}\verb|Thm.forall_elim: cterm -> thm -> thm| \\
@@ -752,6 +753,13 @@
   records full proof terms.  Officially named theorems that contribute
   to a result are recorded in any case.
 
+  \item \verb|Thm.transfer|~\isa{thy\ thm} transfers the given
+  theorem to a \emph{larger} theory, see also \secref{sec:context}.
+  This formal adjustment of the background context has no logical
+  significance, but is occasionally required for formal reasons, e.g.\
+  when theorems that are imported from more basic theories are used in
+  the current situation.
+
   \item \verb|Thm.assume|, \verb|Thm.forall_intr|, \verb|Thm.forall_elim|, \verb|Thm.implies_intr|, and \verb|Thm.implies_elim|
   correspond to the primitive inferences of \figref{fig:prim-rules}.
 
diff -r 34ed34804d90 -r 7860ffc5ec08 doc-src/Ref/theories.tex
--- a/doc-src/Ref/theories.tex	Mon Jun 06 17:51:14 2011 +0200
+++ b/doc-src/Ref/theories.tex	Mon Jun 06 18:05:38 2011 +0200
@@ -1,25 +1,5 @@
 
-\chapter{Theories, Terms and Types} \label{theories}
-\index{theories|(}
-
-\section{Basic operations on theories}\label{BasicOperationsOnTheories}
-
-\subsection{*Theory inclusion}
-\begin{ttbox}
-transfer    : theory -> thm -> thm
-\end{ttbox}
-
-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{transfer} $thy$ $thm$] transfers theorem $thm$ to
-  theory $thy$, provided the latter includes the theory of $thm$.
-  
-\end{ttdescription}
-
+\chapter{Terms}
 
 \section{*Variable binding}
 \begin{ttbox}
@@ -58,9 +38,6 @@
 
 \end{ttdescription}
 
-\index{theories|)}
-
-
 %%% Local Variables: 
 %%% mode: latex
 %%% TeX-master: "ref"