--- a/doc-src/IsarRef/intro.tex Sun Aug 22 18:21:36 1999 +0200
+++ b/doc-src/IsarRef/intro.tex Sun Aug 22 21:13:20 1999 +0200
@@ -15,7 +15,7 @@
lemma "0 < foo" by (simp add: foo_def);
end
\end{ttbox}
-Note that \emph{any} Isabelle/Isar command may be retracted by \texttt{undo}.
+Note that any Isabelle/Isar command may be retracted by \texttt{undo}.
Plain TTY-based interaction like this used to be quite feasible with
traditional tactic based theorem proving, but developing Isar documents
@@ -30,7 +30,7 @@
\medskip
-The easiest way to use ProofGeneral is to make it the default Isabelle user
+The easiest way to use Proof~General is to make it the default Isabelle user
interface. Just say something like this in your Isabelle settings file (cf.\
\cite{isabelle-sys}):
\begin{ttbox}
@@ -39,8 +39,8 @@
\end{ttbox}
You may have to change \texttt{\$ISABELLE_HOME/contrib/ProofGeneral} to the
actual installation directory of Proof~General. Now the capital
-\texttt{Isabelle} binary refers to the \texttt{ProofGeneral/isar} interface.
-It's usage is as follows:
+\texttt{Isabelle} executable refers to the \texttt{ProofGeneral/isar}
+interface. It's usage is as follows:
\begin{ttbox}
Usage: interface [OPTIONS] [FILES ...]
@@ -53,12 +53,12 @@
Starts Proof General for Isabelle/Isar with proof documents FILES
(default Scratch.thy).
\end{ttbox}
-The defaults for these options may be changed via the
-\texttt{PROOFGENERAL_OPTIONS} setting. For example, GNU Emacs\footnote{GNU
- Emacs version 20.x required.} with loading of the startup file enabled may
-be configured as follows:\footnote{The interface disables \texttt{.emacs} by
- default to ensure successful startup despite any strange commands that tend
- to occur there.}
+Note that the defaults for these options may be overridden via the
+\texttt{PROOFGENERAL_OPTIONS} setting. For example, GNU
+Emacs\footnote{Version 20.x required.} with loading of the startup file
+enabled may be configured as follows:\footnote{The interface disables
+ \texttt{.emacs} by default to ensure successful startup despite any strange
+ commands that tend to occur there.}
\begin{ttbox}
PROOFGENERAL_OPTIONS="-p emacs -u true"
\end{ttbox}
@@ -68,7 +68,7 @@
\begin{ttbox}
Isabelle \({\langle}isabellehome{\rangle}\)/src/HOL/Isar_examples/BasicLogic.thy
\end{ttbox}
-Users of XEmacs may note the toolbar for navigating forward and backward
+Users of XEmacs may note the tool bar for navigating forward and backward
through the text. Consult the Proof~General documentation \cite{proofgeneral}
for further basic commands, such as \texttt{c-c return} or \texttt{c-c u}.