1.1 --- a/doc-src/TutorialI/Ifexpr/Ifexpr.thy	Thu Jan 25 11:59:52 2001 +0100
     1.2 +++ b/doc-src/TutorialI/Ifexpr/Ifexpr.thy	Thu Jan 25 15:31:31 2001 +0100
     1.3 @@ -10,7 +10,7 @@
     1.4  the constructs introduced above.
     1.5  *}
     1.6  
     1.7 -subsubsection{*How Can We Model Boolean Expressions?*}
     1.8 +subsubsection{*Modelling Boolean Expressions*}
     1.9  
    1.10  text{*
    1.11  We want to represent boolean expressions built up from variables and
    1.12 @@ -28,7 +28,7 @@
    1.13  For example, the formula $P@0 \land \neg P@1$ is represented by the term
    1.14  @{term"And (Var 0) (Neg(Var 1))"}.
    1.15  
    1.16 -\subsubsection{What is the Value of a Boolean Expression?}
    1.17 +\subsubsection{The Value of a Boolean Expression}
    1.18  
    1.19  The value of a boolean expression depends on the value of its variables.
    1.20  Hence the function @{text"value"} takes an additional parameter, an
    1.21 @@ -66,9 +66,8 @@
    1.22                                          else valif e env)";
    1.23  
    1.24  text{*
    1.25 -\subsubsection{Transformation Into and of If-Expressions}
    1.26 +\subsubsection{Converting Boolean and If-Expressions}
    1.27  
    1.28 -\REMARK{is this the title you wanted?}
    1.29  The type @{typ"boolex"} is close to the customary representation of logical
    1.30  formulae, whereas @{typ"ifex"} is designed for efficiency. It is easy to
    1.31  translate from @{typ"boolex"} into @{typ"ifex"}: