diff -r 45c3c2cf2386 -r 67fb61748d35 doc-src/IsarRef/generic.tex
--- a/doc-src/IsarRef/generic.tex	Wed May 31 11:56:28 2000 +0200
+++ b/doc-src/IsarRef/generic.tex	Wed May 31 14:14:45 2000 +0200
@@ -304,7 +304,6 @@
 \indexisaratt{RS}\indexisaratt{COMP}
 \indexisaratt{where}
 \indexisaratt{tag}\indexisaratt{untag}
-\indexisaratt{transfer}
 \indexisaratt{export}
 \indexisaratt{unfold}\indexisaratt{fold}
 \begin{matharray}{rcl}
@@ -318,7 +317,6 @@
   standard & : & \isaratt \\
   elimify & : & \isaratt \\
   export^* & : & \isaratt \\
-  transfer & : & \isaratt \\[0.5ex]
 \end{matharray}
 
 \begin{rail}
@@ -363,10 +361,6 @@
   proper incremental export is already done as part of the basic Isar
   machinery.  This attribute is mainly for experimentation.
   
-\item [$transfer$] promotes a theorem to the current theory context, which has
-  to enclose the former one.  This is done automatically whenever rules are
-  joined by inference.
-
 \end{descr}