doc-src/TutorialI/Datatype/document/ABexpr.tex
 changeset 10971 6852682eaf16 parent 10187 0376cccd9118 child 11309 d666f11ca2d4
     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}