--- a/doc-src/IsarRef/intro.tex Sat Jul 01 19:58:59 2000 +0200
+++ b/doc-src/IsarRef/intro.tex Sat Jul 01 19:59:24 2000 +0200
@@ -17,8 +17,9 @@
lemma "0 < foo" by (simp add: foo_def);
end
\end{ttbox}
-Note that any Isabelle/Isar command may be retracted by \texttt{undo}. The
-\texttt{help} command prints a list of available language elements.
+Note that any Isabelle/Isar command may be retracted by \texttt{undo}. See
+the Isabelle/Isar Quick Reference (Appendix~{ap:refcard}) for a comprehensive
+overview of available commands and other language elements.
\subsection{Proof~General}
--- 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
--- a/doc-src/IsarRef/refcard.tex Sat Jul 01 19:58:59 2000 +0200
+++ b/doc-src/IsarRef/refcard.tex Sat Jul 01 19:59:24 2000 +0200
@@ -75,7 +75,6 @@
\subsection{Diagnostic commands}
\begin{matharray}{ll}
- \isarkeyword{help} & \text{print help on Isar language elements} \\
\isarkeyword{pr} & \text{print current state} \\
\isarkeyword{thm}~\vec a & \text{print theorems} \\
\isarkeyword{term}~t & \text{print term} \\
--- a/doc-src/IsarRef/syntax.tex Sat Jul 01 19:58:59 2000 +0200
+++ b/doc-src/IsarRef/syntax.tex Sat Jul 01 19:59:24 2000 +0200
@@ -362,19 +362,23 @@
\medskip
-The following options are available to tune the output.
+The following options are available to tune the output. Note that some of
+these coincide with ML flags of the same names (see also \cite{isabelle-ref}).
\begin{descr}
-\item[$show_types = bool$ and $show_sorts = bool$] refer to Isabelle's global
- ML flags of the same names (see also \cite{isabelle-ref}).
+\item[$show_types = bool$ and $show_sorts = bool$] control printing of
+ explicit type and sort constraints
+\item[$long_names = bool$] forces names of types and constants etc.\ to be
+ printed in their fully qualified internal form.
+\item[$eta_contract = bool$] prints terms in $\eta$-contracted form.
\item[$display = bool$] indicates if the text is to be output as multi-line
``display material'', rather than a small piece of text without line breaks
(which is the default).
\item[$quotes = bool$] indicates if the output should be enclosed in double
quotes.
-\item[$mode = name$] adds $name$ to the print mode to be used for
- presentation. Note that the standard setup for {\LaTeX} output is already
- present by default, including the modes ``$latex$'', ``$xsymbols$'',
- ``$symbols$''.
+\item[$mode = name$] adds $name$ to the print mode to be used for presentation
+ (see also \cite{isabelle-ref}). Note that the standard setup for {\LaTeX}
+ output is already present by default, including the modes ``$latex$'',
+ ``$xsymbols$'', ``$symbols$''.
\item[$margin = nat$] changes the margin for pretty printing of display
material.
\end{descr}