diff -r 4b47d8aaf5af -r 5eebea8f359f doc-src/TutorialI/Ifexpr/Ifexpr.thy
--- a/doc-src/TutorialI/Ifexpr/Ifexpr.thy	Thu Jan 25 11:59:52 2001 +0100
+++ b/doc-src/TutorialI/Ifexpr/Ifexpr.thy	Thu Jan 25 15:31:31 2001 +0100
@@ -10,7 +10,7 @@
 the constructs introduced above.
 *}
 
-subsubsection{*How Can We Model Boolean Expressions?*}
+subsubsection{*Modelling Boolean Expressions*}
 
 text{*
 We want to represent boolean expressions built up from variables and
@@ -28,7 +28,7 @@
 For example, the formula $P@0 \land \neg P@1$ is represented by the term
 @{term"And (Var 0) (Neg(Var 1))"}.
 
-\subsubsection{What is the Value of a Boolean Expression?}
+\subsubsection{The Value of a Boolean Expression}
 
 The value of a boolean expression depends on the value of its variables.
 Hence the function @{text"value"} takes an additional parameter, an
@@ -66,9 +66,8 @@
                                         else valif e env)";
 
 text{*
-\subsubsection{Transformation Into and of If-Expressions}
+\subsubsection{Converting Boolean and If-Expressions}
 
-\REMARK{is this the title you wanted?}
 The type @{typ"boolex"} is close to the customary representation of logical
 formulae, whereas @{typ"ifex"} is designed for efficiency. It is easy to
 translate from @{typ"boolex"} into @{typ"ifex"}: