1.1 --- a/doc-src/TutorialI/Datatype/document/ABexpr.tex	Wed Jan 24 11:59:15 2001 +0100
     1.2 +++ b/doc-src/TutorialI/Datatype/document/ABexpr.tex	Wed Jan 24 12:29:10 2001 +0100
     1.3 @@ -27,7 +27,7 @@
     1.4  \noindent
     1.5  Type \isa{aexp} is similar to \isa{expr} in \S\ref{sec:ExprCompiler},
     1.6  except that we have fixed the values to be of type \isa{nat} and that we
     1.7 -have fixed the two binary operations \isa{aexp{\isachardot}Sum} and \isa{Diff}. Boolean
     1.8 +have fixed the two binary operations \isa{Sum} and \isa{Diff}. Boolean
     1.9  expressions can be arithmetic comparisons, conjunctions and negations.
    1.10  The semantics is fixed via two evaluation functions%
    1.11  \end{isamarkuptext}%
    1.12 @@ -100,7 +100,7 @@
    1.13  \[ P@1(x@1)\ \land \dots \land P@n(x@n) \]
    1.14  where each variable $x@i$ is of type $\tau@i$. Induction is started by
    1.15  \begin{isabelle}
    1.16 -\isacommand{apply}\isa{{\isacharparenleft}induct{\isacharunderscore}tac} $x@1$ \isa{and} \dots\ \isa{and} $x@n$\isa{{\isacharparenright}}
    1.17 +\isacommand{apply}\isa{{\isacharparenleft}induct{\isacharunderscore}tac} $x@1$ \isacommand{and} \dots\ \isacommand{and} $x@n$\isa{{\isacharparenright}}
    1.18  \end{isabelle}
    1.19  
    1.20  \begin{exercise}