diff -r 9577530e8a5a -r 9529d31f39e0 doc-src/TutorialI/basics.tex
--- a/doc-src/TutorialI/basics.tex	Fri Jul 13 18:07:01 2001 +0200
+++ b/doc-src/TutorialI/basics.tex	Fri Jul 13 18:08:26 2001 +0200
@@ -165,8 +165,8 @@
 \textbf{Formulae}\indexbold{formula} are terms of type \isaindexbold{bool}.
 There are the basic constants \isaindexbold{True} and \isaindexbold{False} and
 the usual logical connectives (in decreasing order of priority):
-\indexboldpos{\isasymnot}{$HOL0not}, \indexboldpos{\isasymand}{$HOL0and},
-\indexboldpos{\isasymor}{$HOL0or}, and \indexboldpos{\isasymimp}{$HOL0imp},
+\indexboldpos{\protect\isasymnot}{$HOL0not}, \indexboldpos{\protect\isasymand}{$HOL0and},
+\indexboldpos{\protect\isasymor}{$HOL0or}, and \indexboldpos{\protect\isasymimp}{$HOL0imp},
 all of which (except the unary \isasymnot) associate to the right. In
 particular \isa{A \isasymimp~B \isasymimp~C} means \isa{A \isasymimp~(B
   \isasymimp~C)} and is thus logically equivalent to \isa{A \isasymand~B
@@ -181,11 +181,13 @@
 \isa{\isasymnot($t@1$ = $t@2$)}.
 
 Quantifiers are written as
-\isa{\isasymforall{}x.~$P$}\indexbold{$HOL0All@\isasymforall} and
-\isa{\isasymexists{}x.~$P$}\indexbold{$HOL0Ex@\isasymexists}.  There is
-even \isa{\isasymuniqex{}x.~$P$}\index{$HOL0ExU@\isasymuniqex|bold}, which
-means that there exists exactly one \isa{x} that satisfies \isa{$P$}.  Nested
-quantifications can be abbreviated: \isa{\isasymforall{}x~y~z.~$P$} means
+\isa{\isasymforall{}x.~$P$}\index{$HOL0All@\isasymforall|bold} and
+\isa{\isasymexists{}x.~$P$}\index{$HOL0Ex@\isasymexists|bold}. 
+There is even
+\isa{\isasymuniqex{}x.~$P$}\index{$HOL0ExU@\isasymuniqex|bold}, which
+means that there exists exactly one \isa{x} that satisfies \isa{$P$}. 
+Nested quantifications can be abbreviated:
+\isa{\isasymforall{}x~y~z.~$P$} means
 \isa{\isasymforall{}x.\isasymforall{}y.\isasymforall{}z.~$P$}.
 
 Despite type inference, it is sometimes necessary to attach explicit