doc-src/IsarRef/generic.tex
changeset 9005 67fb61748d35
parent 8904 0bb77c5b86cc
child 9232 96722b04f2ae
     1.1 --- a/doc-src/IsarRef/generic.tex	Wed May 31 11:56:28 2000 +0200
     1.2 +++ b/doc-src/IsarRef/generic.tex	Wed May 31 14:14:45 2000 +0200
     1.3 @@ -304,7 +304,6 @@
     1.4  \indexisaratt{RS}\indexisaratt{COMP}
     1.5  \indexisaratt{where}
     1.6  \indexisaratt{tag}\indexisaratt{untag}
     1.7 -\indexisaratt{transfer}
     1.8  \indexisaratt{export}
     1.9  \indexisaratt{unfold}\indexisaratt{fold}
    1.10  \begin{matharray}{rcl}
    1.11 @@ -318,7 +317,6 @@
    1.12    standard & : & \isaratt \\
    1.13    elimify & : & \isaratt \\
    1.14    export^* & : & \isaratt \\
    1.15 -  transfer & : & \isaratt \\[0.5ex]
    1.16  \end{matharray}
    1.17  
    1.18  \begin{rail}
    1.19 @@ -363,10 +361,6 @@
    1.20    proper incremental export is already done as part of the basic Isar
    1.21    machinery.  This attribute is mainly for experimentation.
    1.22    
    1.23 -\item [$transfer$] promotes a theorem to the current theory context, which has
    1.24 -  to enclose the former one.  This is done automatically whenever rules are
    1.25 -  joined by inference.
    1.26 -
    1.27  \end{descr}
    1.28  
    1.29