author wenzelm Tue, 04 May 1999 18:27:36 +0200 changeset 6584 5569f2672662 parent 6583 4ac69ed20120 child 6585 d5eae11efa42
tuned;
 doc-src/Tutorial/basics.tex file | annotate | diff | comparison | revisions doc-src/Tutorial/tutorial.tex file | annotate | diff | comparison | revisions
--- a/doc-src/Tutorial/basics.tex	Tue May 04 18:11:35 1999 +0200
+++ b/doc-src/Tutorial/basics.tex	Tue May 04 18:27:36 1999 +0200
@@ -32,11 +32,11 @@
\texttt{.thy}. The general format of a theory file \texttt{T.thy} is
\begin{ttbox}
T = B$$@1$$ + $$\cdots$$ + B$$@n$$ +
-$${<}declarations{>}$$
+$${\langle}declarations{\rangle}$$
end
\end{ttbox}
where \texttt{B}$@1$, \dots, \texttt{B}$@n$ are the names of existing
-theories that \texttt{T} is based on and ${<}declarations{>}$ stands for the
+theories that \texttt{T} is based on and ${\langle}declarations{\rangle}$ stands for the
newly introduced concepts (types, functions etc). The \texttt{B}$@i$ are the
direct \textbf{parent theories}\indexbold{parent theory} of \texttt{T}.
Everything defined in the parent theories (and their parents \dots) is
@@ -56,7 +56,7 @@
\end{warn}

This tutorial is concerned with introducing you to the different linguistic
-constructs that can fill ${<}declarations{>}$ in the above theory template.
+constructs that can fill ${\langle}declarations{\rangle}$ in the above theory template.
A complete grammar of the basic constructs is found in Appendix~A
of~\cite{Isa-Ref-Man}, for reference in times of doubt.

@@ -254,12 +254,13 @@
\section{Getting started}

Assuming you have installed Isabelle, you start it by typing \texttt{isabelle
-  HOL} in a shell window.\footnote{Since you will always want to use HOL when
-  studying this tutorial, you can set the shell variable
-  \texttt{ISABELLE_LOGIC} to \texttt{HOL} once and for all and simply execute
-  \texttt{isabelle}.} This presents you with Isabelle's most basic ASCII
-interface. In addition you need to open an editor window to create theories
-(\texttt{.thy} files) and proof scripts (\texttt{.ML} files). While you are
-developing a proof, we recommend to type each proof command into the ML-file
-first and then enter it into Isabelle by copy-and-paste, thus ensuring that
-you have a complete record of your proof.
+  HOL} in a shell window.\footnote{Simply executing \texttt{isabelle} without
+  an argument starts the default logic, which usually is already \texttt{HOL}.
+  This is controlled by the \texttt{ISABELLE_LOGIC} setting, see \emph{The
+    Isabelle System Manual} for more details.} This presents you with
+Isabelle's most basic ASCII interface.  In addition you need to open an editor
+window to create theories (\texttt{.thy} files) and proof scripts
+(\texttt{.ML} files). While you are developing a proof, we recommend to type
+each proof command into the ML-file first and then enter it into Isabelle by
+copy-and-paste, thus ensuring that you have a complete record of your proof.
+
--- a/doc-src/Tutorial/tutorial.tex	Tue May 04 18:11:35 1999 +0200
+++ b/doc-src/Tutorial/tutorial.tex	Tue May 04 18:27:36 1999 +0200
@@ -55,7 +55,7 @@
This tutorial owes a lot to the constant discussions with and the valuable
feedback from Larry Paulson and the Isabelle group at Munich: Olaf M\"uller,
Wolfgang Naraschewski, David von Oheimb, Leonor Prensa Nieto, Cornelia Pusch
-and Markus Wenzel. Stefan Berghofer and Stefan Merz were also kind enough to
+and Markus Wenzel. Stefan Berghofer and Stephan Merz were also kind enough to
read and comment on a draft version.
\clearfirst