--- a/doc-src/IsarRef/pure.tex Sat Jul 01 19:58:59 2000 +0200
+++ b/doc-src/IsarRef/pure.tex Sat Jul 01 19:59:24 2000 +0200
@@ -1173,7 +1173,6 @@
\indexisarcmd{pr}\indexisarcmd{thm}\indexisarcmd{term}\indexisarcmd{prop}\indexisarcmd{typ}
\indexisarcmd{print-facts}\indexisarcmd{print-binds}
\begin{matharray}{rcl}
- \isarcmd{help}^* & : & \isarkeep{\cdot} \\
\isarcmd{pr}^* & : & \isarkeep{\cdot} \\
\isarcmd{thm}^* & : & \isarkeep{theory~|~proof} \\
\isarcmd{term}^* & : & \isarkeep{theory~|~proof} \\
@@ -1204,8 +1203,6 @@
\end{rail}
\begin{descr}
-\item [$\isarkeyword{help}$] prints a list of available language elements.
- Note that methods and attributes depend on the current theory context.
\item [$\isarkeyword{pr}~n$] prints the current proof state (if present),
including the proof context, current facts and goals. The optional argument
$n$ affects the implicit limit of goals to be displayed, which is initially