diff -r 55c0f9a8df78 -r 59961d32b1ae doc-src/TutorialI/basics.tex
--- a/doc-src/TutorialI/basics.tex	Fri Jan 26 15:02:04 2001 +0100
+++ b/doc-src/TutorialI/basics.tex	Fri Jan 26 15:50:28 2001 +0100
@@ -8,12 +8,14 @@
 HOL, which abbreviates Higher-Order Logic. We introduce HOL step by step
 following the equation
 \[ \mbox{HOL} = \mbox{Functional Programming} + \mbox{Logic}. \]
-We assume that the reader is familiar with the basic concepts of both fields.
-For excellent introductions to functional programming consult the textbooks
-by Bird and Wadler~\cite{Bird-Wadler} or Paulson~\cite{paulson-ml2}.  Although
-this tutorial initially concentrates on functional programming, do not be
-misled: HOL can express most mathematical concepts, and functional
-programming is just one particularly simple and ubiquitous instance.
+We do not assume that the reader is familiar with mathematical logic but that
+(s)he is used to logical and set theoretic notation.  In contrast, we do assume
+that the reader is familiar with the basic concepts of functional programming.
+For excellent introductions consult the textbooks by Bird and
+Wadler~\cite{Bird-Wadler} or Paulson~\cite{paulson-ml2}.  Although this
+tutorial initially concentrates on functional programming, do not be
+misled: HOL can express most mathematical concepts, and functional programming
+is just one particularly simple and ubiquitous instance.
 
 Isabelle~\cite{paulson-isa-book} is implemented in ML~\cite{SML}.
 This has influenced some of HOL's concrete syntax but is otherwise
@@ -233,7 +235,7 @@
 \end{itemize}
 
 For the sake of readability the usual mathematical symbols are used throughout
-the tutorial. Their ASCII-equivalents are shown in table~\ref{tab:ascii} in
+the tutorial. Their \textsc{ascii}-equivalents are shown in table~\ref{tab:ascii} in
 the appendix.
 
 
@@ -278,7 +280,7 @@
   General}~\cite{Aspinall:TACAS:2000,proofgeneral}.
 
 Some interfaces (including the shell level) offer special fonts with
-mathematical symbols. For those that do not, remember that ASCII-equivalents
+mathematical symbols. For those that do not, remember that \textsc{ascii}-equivalents
 are shown in table~\ref{tab:ascii} in the appendix.
 
 Finally, a word about semicolons.\indexbold{$Isar@\texttt{;}} 
@@ -295,7 +297,7 @@
   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
+basic \textsc{ascii} interface.  In addition you need to open an editor window to
 create theory files.  While you are developing a theory, we recommend to
 type each command into the file first and then enter it into Isabelle by
 copy-and-paste, thus ensuring that you have a complete record of your theory.