--- a/doc-src/Ref/introduction.tex Wed Mar 10 13:44:55 1999 +0100
+++ b/doc-src/Ref/introduction.tex Wed Mar 10 16:31:33 1999 +0100
@@ -71,8 +71,8 @@
isabelle Foo
\end{ttbox}
-More details about the \texttt{isabelle} command may be found in the
-\emph{System Manual}.
+More details about the \texttt{isabelle} command may be found in \emph{The
+ Isabelle System Manual}.
\medskip Saving the state is not enough. Record, on a file, the
top-level commands that generate your theories and proofs. Such a
@@ -135,11 +135,12 @@
performs {\tt use~"$file$"} and prints the total execution time.
\end{ttdescription}
-The $dir$ and $file$ specifications of the \texttt{cd} and
-\texttt{use} commands may contain path variables that are expanded
-appropriately, e.g.\ \texttt{\$ISABELLE_HOME} or \texttt{\~\relax}
-(which abbreviates \texttt{\$HOME}). Section~\ref{LoadingTheories}
-describes commands for loading theory files.
+The $dir$ and $file$ specifications of the \texttt{cd} and \texttt{use}
+commands may contain path variables (e.g.\ \texttt{\$ISABELLE_HOME}) that are
+expanded appropriately. Note that \texttt{\~\relax} abbreviates
+\texttt{\$HOME}, and \texttt{\~\relax\~\relax} abbreviates
+\texttt{\$ISABELLE_HOME}. Section~\ref{LoadingTheories} describes commands
+for loading theory files.
\section{Setting flags}
@@ -189,6 +190,7 @@
\index{types!printing of}\index{sorts!printing of}
\begin{ttbox}
show_hyps : bool ref \hfill{\bf initially true}
+show_tags : bool ref \hfill{\bf initially false}
show_brackets : bool ref \hfill{\bf initially false}
show_types : bool ref \hfill{\bf initially false}
show_sorts : bool ref \hfill{\bf initially false}
@@ -209,6 +211,9 @@
\item[reset \ttindexbold{show_hyps};] makes Isabelle show each
meta-level hypothesis as a dot.
+\item[set \ttindexbold{show_tags};] makes Isabelle show tags of theorems
+ (which are basically just comments that may be attached by some tools).
+
\item[set \ttindexbold{show_brackets};] makes Isabelle show full
bracketing. In particular, this reveals the grouping of infix
operators.