doc-src/TutorialI/Ifexpr/Ifexpr.thy

 (*<*)
 theory Ifexpr = Main:;
 (*>*)
 
-subsection{*Case study: boolean expressions*}
+subsection{*Case Study: Boolean Expressions*}
 
 text{*\label{sec:boolex}
 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.
 *}
 
-subsubsection{*How can we model boolean expressions?*}
+subsubsection{*How Can We Model Boolean Expressions?*}
 
 text{*
 We want to represent boolean expressions built up from variables and
 constants by negation and conjunction. The following datatype serves exactly
 that purpose:

 @{term"Const False"}. Variables are represented by terms of the form
 @{term"Var n"}, where @{term"n"} is a natural number (type @{typ"nat"}).
 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{What is 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
 \emph{environment} of type @{typ"nat => bool"}, which maps variables to their
 values:

 "value (Var x)   env = env x"
 "value (Neg b)   env = (\<not> value b env)"
 "value (And b c) env = (value b env \<and> value c env)";
 
 text{*\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
 from constants (@{term"CIF"}), variables (@{term"VIF"}) and conditionals
 (@{term"IF"}):

 "valif (VIF x)    env = env x"
 "valif (IF b t e) env = (if valif b env then valif t env
                                         else valif e env)";
 
 text{*
-\subsubsection{Transformation into and of If-expressions}
+\subsubsection{Transformation Into and of 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"}:
 *}