# HG changeset patch
# User wenzelm
# Date 962474364 -7200
# Node ID 8c8399b9ecaa5912d98fa89d613347a57a3a0277
# Parent  96722b04f2aec90eb82d7627d29b0714a2b2a640
removed "help";

diff -r 96722b04f2ae -r 8c8399b9ecaa doc-src/IsarRef/intro.tex
--- 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}
diff -r 96722b04f2ae -r 8c8399b9ecaa doc-src/IsarRef/pure.tex
--- 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
diff -r 96722b04f2ae -r 8c8399b9ecaa doc-src/IsarRef/refcard.tex
--- 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} \\
diff -r 96722b04f2ae -r 8c8399b9ecaa doc-src/IsarRef/syntax.tex
--- 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}