diff -r 6417de2029b0 -r b254d5ad6dd4 doc-src/TutorialI/Ifexpr/document/Ifexpr.tex
--- a/doc-src/TutorialI/Ifexpr/document/Ifexpr.tex	Fri Jan 12 16:05:12 2001 +0100
+++ b/doc-src/TutorialI/Ifexpr/document/Ifexpr.tex	Fri Jan 12 16:07:20 2001 +0100
@@ -2,7 +2,7 @@
 \begin{isabellebody}%
 \def\isabellecontext{Ifexpr}%
 %
-\isamarkupsubsection{Case study: boolean expressions%
+\isamarkupsubsection{Case Study: Boolean Expressions%
 }
 %
 \begin{isamarkuptext}%
@@ -12,7 +12,7 @@
 the constructs introduced above.%
 \end{isamarkuptext}%
 %
-\isamarkupsubsubsection{How can we model boolean expressions?%
+\isamarkupsubsubsection{How Can We Model Boolean Expressions?%
 }
 %
 \begin{isamarkuptext}%
@@ -30,7 +30,7 @@
 For example, the formula $P@0 \land \neg P@1$ is represented by the term
 \isa{And\ {\isacharparenleft}Var\ {\isadigit{0}}{\isacharparenright}\ {\isacharparenleft}Neg\ {\isacharparenleft}Var\ {\isadigit{1}}{\isacharparenright}{\isacharparenright}}.
 
-\subsubsection{What is the value of a boolean expression?}
+\subsubsection{What is the Value of a Boolean Expression?}
 
 The value of a boolean expression depends on the value of its variables.
 Hence the function \isa{value} takes an additional parameter, an
@@ -45,7 +45,7 @@
 {\isachardoublequote}value\ {\isacharparenleft}And\ b\ c{\isacharparenright}\ env\ {\isacharequal}\ {\isacharparenleft}value\ b\ env\ {\isasymand}\ value\ c\ env{\isacharparenright}{\isachardoublequote}%
 \begin{isamarkuptext}%
 \noindent
-\subsubsection{If-expressions}
+\subsubsection{If-Expressions}
 
 An alternative and often more efficient (because in a certain sense
 canonical) representation are so-called \emph{If-expressions} built up
@@ -64,8 +64,9 @@
 {\isachardoublequote}valif\ {\isacharparenleft}IF\ b\ t\ e{\isacharparenright}\ env\ {\isacharequal}\ {\isacharparenleft}if\ valif\ b\ env\ then\ valif\ t\ env\isanewline
 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ else\ valif\ e\ env{\isacharparenright}{\isachardoublequote}%
 \begin{isamarkuptext}%
-\subsubsection{Transformation into and of If-expressions}
+\subsubsection{Transformation Into and of If-Expressions}
 
+\REMARK{is this the title you wanted?}
 The type \isa{boolex} is close to the customary representation of logical
 formulae, whereas \isa{ifex} is designed for efficiency. It is easy to
 translate from \isa{boolex} into \isa{ifex}:%