diff -r e07927b980ec -r 7eb63f63e6c6 doc-src/TutorialI/Ifexpr/Ifexpr.thy
--- a/doc-src/TutorialI/Ifexpr/Ifexpr.thy	Wed Jul 25 18:21:01 2001 +0200
+++ b/doc-src/TutorialI/Ifexpr/Ifexpr.thy	Thu Jul 26 16:43:02 2001 +0200
@@ -4,7 +4,7 @@
 
 subsection{*Case Study: Boolean Expressions*}
 
-text{*\label{sec:boolex}
+text{*\label{sec:boolex}\index{boolean expressions example|(}
 The aim of this case study is twofold: it shows how to model boolean
 expressions and some algorithms for manipulating them, and it demonstrates
 the constructs introduced above.
@@ -120,7 +120,7 @@
 "norm (IF b t e) = normif b (norm t) (norm e)";
 
 text{*\noindent
-Their interplay is a bit tricky, and we leave it to the reader to develop an
+Their interplay is tricky; we leave it to you to develop an
 intuitive understanding. Fortunately, Isabelle can help us to verify that the
 transformation preserves the value of the expression:
 *}
@@ -129,7 +129,7 @@
 
 text{*\noindent
 The proof is canonical, provided we first show the following simplification
-lemma (which also helps to understand what @{term"normif"} does):
+lemma, which also helps to understand what @{term"normif"} does:
 *}
 
 lemma [simp]:
@@ -147,7 +147,7 @@
 of the theorem shown above because of the @{text"[simp]"} attribute.
 
 But how can we be sure that @{term"norm"} really produces a normal form in
-the above sense? We define a function that tests If-expressions for normality
+the above sense? We define a function that tests If-expressions for normality:
 *}
 
 consts normal :: "ifex \<Rightarrow> bool";
@@ -158,7 +158,7 @@
      (case b of CIF b \<Rightarrow> True | VIF x \<Rightarrow> True | IF x y z \<Rightarrow> False))";
 
 text{*\noindent
-and prove @{term"normal(norm b)"}. Of course, this requires a lemma about
+Now we prove @{term"normal(norm b)"}. Of course, this requires a lemma about
 normality of @{term"normif"}:
 *}
 
@@ -186,6 +186,7 @@
   some of the goals as implications (@{text"\<longrightarrow>"}) rather than
   equalities (@{text"="}).)
 \end{exercise}
+\index{boolean expressions example|)}
 *}
 (*<*)
 end