1.1 --- a/doc-src/Intro/advanced.tex	Thu Nov 25 19:09:43 1993 +0100
     1.2 +++ b/doc-src/Intro/advanced.tex	Fri Nov 26 12:31:48 1993 +0100
     1.3 @@ -274,7 +274,7 @@
     1.4  
     1.5  \medskip
     1.6  Again, there is a simpler way of conducting this proof.  The
     1.7 -\ttindex{goalw} command starts unfolds definitions in the premises, as well
     1.8 +\ttindex{goalw} command unfolds definitions in the premises as well
     1.9  as the conclusion:
    1.10  \begin{ttbox}
    1.11  val [major,minor] = goalw FOL.thy [not_def]
    1.12 @@ -564,9 +564,14 @@
    1.13  \begin{ttbox} 
    1.14      If :: "[o,o,o] => o"       ("if _ then _ else _" [100,0,0] 99)
    1.15  \end{ttbox}
    1.16 -defines a conditional whose first argument cannot be a conditional because it
    1.17 -must have a precedence of at least 100.  Precedences only apply to
    1.18 -mixfix syntax: we may write $If(If(P,Q,R),S,T)$.
    1.19 +defines concrete syntax for a
    1.20 +conditional whose first argument cannot have the form $if~P~then~Q~else~R$
    1.21 +because it must have a precedence of at least~100.  Since expressions put in
    1.22 +parentheses have maximal precedence, we may of course write 
    1.23 +\begin{quote}
    1.24 +\it  if (if P then Q else R) then S else T
    1.25 +\end{quote}
    1.26 +Conditional expressions can also be written using the constant {\tt If}.
    1.27  
    1.28  Binary type constructors, like products and sums, may also be declared as
    1.29  infixes.  The type declaration below introduces a type constructor~$*$ with
    1.30 @@ -1189,11 +1194,6 @@
    1.31  {\out rev(a : b : c : d : Nil, d : c : b : a : Nil)}
    1.32  {\out No subgoals!}
    1.33  \end{ttbox}
    1.34 -Although Isabelle is much slower than a {\sc Prolog} system, many
    1.35 -Isabelle tactics exploit logic programming techniques.  For instance, the
    1.36 -simplification tactics prove subgoals of the form $t=\Var{x}$, rewriting~$t$
    1.37 -and placing the normalised result in~$\Var{x}$.
    1.38 -% Local Variables: 
    1.39 -% mode: latex
    1.40 -% TeX-master: t
    1.41 -% End: 
    1.42 +Although Isabelle is much slower than a {\sc Prolog} system, Isabelle
    1.43 +tactics can exploit logic programming techniques.  
    1.44 +