diff -r d25be0ad1a6c -r 1b02a6c4032f doc-src/TutorialI/tutorial.ind
--- a/doc-src/TutorialI/tutorial.ind	Mon Jul 23 19:06:11 2001 +0200
+++ b/doc-src/TutorialI/tutorial.ind	Tue Jul 24 11:25:54 2001 +0200
@@ -1,20 +1,16 @@
 \begin{theindex}
 
   \item \emph {$\forall \tmspace +\thinmuskip {.1667em}$}, \bold{189}
-  \item \isasymforall, \bold{3}
   \item \ttall, \bold{189}
   \item \emph {$\exists \tmspace +\thinmuskip {.1667em}$}, \bold{189}
-  \item \isasymexists, \bold{3}
   \item \texttt{?}, 5, \bold{189}
   \item \emph {$\varepsilon $}, \bold{189}
-  \item \isasymuniqex, \bold{3}, \bold{189}
+  \item \isasymuniqex, \bold{189}
   \item \ttuniquex, \bold{189}
   \item \emph {$\wedge $}, \bold{189}
   \item \isasymand, \bold{3}
   \item {\texttt {\&}}, \bold{189}
-  \item \texttt {=}, \bold{3}
-  \item \emph {$\DOTSB \mathrel {\smash -}\mathrel {\mkern -3mu}\rightarrow $}, 
-		\bold{189}
+  \item \emph {$\DOTSB \relbar \joinrel \rightarrow $}, \bold{189}
   \item \isasymimp, \bold{3}
   \item \texttt {-->}, \bold{189}
   \item \emph {$\neg $}, \bold{189}
@@ -60,14 +56,13 @@
   \item \emph {$\Rightarrow $}, \bold{3}, \bold{189}
   \item \texttt {=>}, \bold{189}
   \item \texttt {<=}, \bold{189}
-  \item \emph {$\DOTSB \mathrel =\mathrel {\mkern -3mu}\Rightarrow $}, 
-		\bold{189}
+  \item \emph {$\DOTSB \Relbar \joinrel \Rightarrow $}, \bold{189}
   \item \texttt {==>}, \bold{189}
   \item \emph {$\mathopen {[\mkern -3mu[}$}, \bold{10}, \bold{189}
   \item \ttlbr, \bold{189}
   \item \emph {$\mathclose {]\mkern -3mu]}$}, \bold{10}, \bold{189}
   \item \ttrbr, \bold{189}
-  \item \emph {$\lambda $}, \bold{3}, \bold{189}
+  \item \emph {$\lambda $}, \bold{189}
   \item \texttt {\%}, \bold{189}
   \item \texttt {,}, \bold{29}
   \item \texttt {;}, \bold{5}
@@ -138,7 +133,8 @@
   \item \isa {card_Pow} (theorem), \bold{93}
   \item \isa {card_Un_Int} (theorem), \bold{93}
   \item cardinality, 93
-  \item \isa {case} (symbol), \bold{3}, 4, 16, 30, 31
+  \item \isa {case} (symbol), 16, 30, 31
+  \item \isa {case} expressions, 3, 4
   \item case distinction, \bold{17}
   \item case splits, \bold{29}
   \item \isa {case_tac} (method), 17, 85
@@ -154,6 +150,7 @@
   \item composition
     \subitem of functions, \bold{94}
     \subitem of relations, \bold{96}
+  \item conditional expressions, \see{\isa{if} expressions}{1}
   \item congruence rules, \bold{157}
   \item \isa {conjE} (theorem), \bold{55}
   \item \isa {conjI} (theorem), \bold{52}
@@ -202,7 +199,7 @@
   \item \isa {elim!} (attribute), 115
   \item elimination rules, 53--54
   \item \isa {Eps} (constant), 93
-  \item equality
+  \item equality, 3
     \subitem of functions, \bold{93}
     \subitem of records, 143
     \subitem of sets, \bold{90}
@@ -234,11 +231,12 @@
   \item flags, 3, 4, 31
     \subitem setting and resetting, 3
   \item \isa {force} (method), 75, 76
-  \item formulae, \bold{3}
+  \item formulae, 3
   \item forward proof, 76--82
   \item \isa {frule} (method), 67
   \item \isa {frule_tac} (method), 60
   \item \isa {fst} (constant), 21
+  \item function types, 3
   \item functions, 93--95
     \subitem total, 9, 45--50
     \subitem underdefined, 165
@@ -248,6 +246,7 @@
   \item \isa {gcd} (constant), 76--78, 85--87
   \item generalizing for induction, 113
   \item Girard, Jean-Yves, \fnote{55}
+  \item Gordon, Mike, 1
   \item ground terms example, 119--124
 
   \indexspace
@@ -262,10 +261,12 @@
   \item \isa {Id_def} (theorem), \bold{96}
   \item \isa {id_def} (theorem), \bold{94}
   \item identifier, \bold{4}
+  \item identifiers
     \subitem qualified, \bold{2}
   \item identity function, \bold{94}
   \item identity relation, \bold{96}
-  \item \isa {if} (symbol), \bold{3}, 4
+  \item \isa {if} expressions, 3, 4
+  \item if-and-only-if, 3
   \item \isa {iff} (attribute), 73, 74, 86, 114
   \item \isa {iffD1} (theorem), \bold{78}
   \item \isa {iffD2} (theorem), \bold{78}
@@ -324,6 +325,7 @@
 
   \indexspace
 
+  \item $\lambda$ expressions, 3
   \item \isa {LEAST} (symbol), 21, 69
   \item least number operator, \see{\protect\isa{LEAST}}{69}
   \item \isacommand {lemma} (command), 11
@@ -332,7 +334,8 @@
   \item \isa {length_induct}, \bold{172}
   \item \isa {less_than} (constant), 98
   \item \isa {less_than_iff} (theorem), \bold{98}
-  \item \isa {let} (symbol), \bold{3}, 4, 29
+  \item \isa {let} (symbol), 29
+  \item \isa {let} expressions, 3, 4
   \item \isa {lex_prod_def} (theorem), \bold{99}
   \item lexicographic product, \bold{99}, 160
   \item {\texttt{lfp}}
@@ -400,7 +403,7 @@
   \indexspace
 
   \item pairs and tuples, 21, 137--140
-  \item parent theory, \bold{2}
+  \item parent theories, \bold{2}
   \item partial function, 164
   \item pattern, higher-order, \bold{159}
   \item PDL, 102--105
@@ -419,7 +422,7 @@
 
   \indexspace
 
-  \item quantifiers
+  \item quantifiers, 3
     \subitem and inductive definitions, 119--121
     \subitem existential, 66
     \subitem for sets, 92
@@ -543,11 +546,12 @@
   \item tuples, \see{pairs and tuples}{1}
   \item \isacommand {typ} (command), 14
   \item type constraints, \bold{4}
+  \item type constructors, 2
   \item type inference, \bold{3}
-  \item type variables, \bold{3}
+  \item type variables, 3
   \item \isacommand {typedecl} (command), 150
   \item \isacommand {typedef} (command), 151--155
-  \item types, 2
+  \item types, 2--3
     \subitem declaring, 150--151
     \subitem defining, 151--155
   \item \isacommand {types} (command), 22
@@ -577,11 +581,12 @@
   \item variable, \bold{4}
   \item variables
     \subitem schematic, 4
-    \subitem type, \bold{3}
+    \subitem type, 3
   \item \isa {vimage_def} (theorem), \bold{95}
 
   \indexspace
 
+  \item Wenzel, Markus, v
   \item \isa {wf_induct} (theorem), \bold{99}
   \item \isa {while} (constant), 167
   \item \isa {While_Combinator} (theory), 167