--- a/doc-src/IsarRef/generic.tex Sat Jul 01 19:56:46 2000 +0200
+++ b/doc-src/IsarRef/generic.tex Sat Jul 01 19:58:59 2000 +0200
@@ -300,6 +300,7 @@
\indexisaratt{standard}
\indexisaratt{elimify}
+\indexisaratt{no-vars}
\indexisaratt{RS}\indexisaratt{COMP}
\indexisaratt{where}
@@ -316,6 +317,7 @@
fold & : & \isaratt \\[0.5ex]
standard & : & \isaratt \\
elimify & : & \isaratt \\
+ no_vars & : & \isaratt \\
export^* & : & \isaratt \\
\end{matharray}
@@ -356,6 +358,9 @@
\item [$elimify$] turns an destruction rule into an elimination, just as the
ML function \texttt{make\_elim} (see \cite{isabelle-ref}).
+\item [$no_vars$] replaces schematic variables by free ones; this is mainly
+ for tuning output of pretty printed theorems.
+
\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