doc-src/IsarRef/generic.tex

 \indexisaratt{elimify}
 
 \indexisaratt{RS}\indexisaratt{COMP}
 \indexisaratt{where}
 \indexisaratt{tag}\indexisaratt{untag}
-\indexisaratt{transfer}
 \indexisaratt{export}
 \indexisaratt{unfold}\indexisaratt{fold}
 \begin{matharray}{rcl}
   tag & : & \isaratt \\
   untag & : & \isaratt \\[0.5ex]

   unfold & : & \isaratt \\
   fold & : & \isaratt \\[0.5ex]
   standard & : & \isaratt \\
   elimify & : & \isaratt \\
   export^* & : & \isaratt \\
-  transfer & : & \isaratt \\[0.5ex]
 \end{matharray}
 
 \begin{rail}
   'tag' (nameref+)
   ;

 \item [$export$] lifts a local result out of the current proof context,
   generalizing all fixed variables and discharging all assumptions.  Note that
   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}
 
 
 \section{The Simplifier}