1.1 --- a/doc-src/TutorialI/Datatype/ABexpr.thy	Fri Sep 01 18:29:52 2000 +0200
     1.2 +++ b/doc-src/TutorialI/Datatype/ABexpr.thy	Fri Sep 01 19:09:44 2000 +0200
     1.3 @@ -26,9 +26,9 @@
     1.4                   | Neg  "'a bexp";
     1.5  
     1.6  text{*\noindent
     1.7 -Type \isa{aexp} is similar to \isa{expr} in \S\ref{sec:ExprCompiler},
     1.8 -except that we have fixed the values to be of type \isa{nat} and that we
     1.9 -have fixed the two binary operations \isa{Sum} and \isa{Diff}. Boolean
    1.10 +Type @{text"aexp"} is similar to @{text"expr"} in \S\ref{sec:ExprCompiler},
    1.11 +except that we have fixed the values to be of type @{typ"nat"} and that we
    1.12 +have fixed the two binary operations @{term"Sum"} and @{term"Diff"}. Boolean
    1.13  expressions can be arithmetic comparisons, conjunctions and negations.
    1.14  The semantics is fixed via two evaluation functions
    1.15  *}
    1.16 @@ -37,8 +37,8 @@
    1.17          evalb :: "'a bexp \\<Rightarrow> ('a \\<Rightarrow> nat) \\<Rightarrow> bool";
    1.18  
    1.19  text{*\noindent
    1.20 -that take an expression and an environment (a mapping from variables \isa{'a} to values
    1.21 -\isa{nat}) and return its arithmetic/boolean
    1.22 +that take an expression and an environment (a mapping from variables @{typ"'a"} to values
    1.23 +@{typ"nat"}) and return its arithmetic/boolean
    1.24  value. Since the datatypes are mutually recursive, so are functions that
    1.25  operate on them. Hence they need to be defined in a single \isacommand{primrec}
    1.26  section:
    1.27 @@ -66,8 +66,8 @@
    1.28  text{*\noindent
    1.29  The first argument is a function mapping variables to expressions, the
    1.30  substitution. It is applied to all variables in the second argument. As a
    1.31 -result, the type of variables in the expression may change from \isa{'a}
    1.32 -to \isa{'b}. Note that there are only arithmetic and no boolean variables.
    1.33 +result, the type of variables in the expression may change from @{typ"'a"}
    1.34 +to @{typ"'b"}. Note that there are only arithmetic and no boolean variables.
    1.35  *}
    1.36  
    1.37  primrec
    1.38 @@ -108,17 +108,17 @@
    1.39  an inductive proof expects a goal of the form
    1.40  \[ P@1(x@1)\ \land \dots \land P@n(x@n) \]
    1.41  where each variable $x@i$ is of type $\tau@i$. Induction is started by
    1.42 -\begin{ttbox}
    1.43 -apply(induct_tac \(x@1\) \texttt{and} \(\dots\) \texttt{and} \(x@n\));
    1.44 -\end{ttbox}
    1.45 +\begin{isabelle}
    1.46 +\isacommand{apply}@{text"(induct_tac"} $x@1$ @{text"and"} \dots\ @{text"and"} $x@n$@{text")"}
    1.47 +\end{isabelle}
    1.48  
    1.49  \begin{exercise}
    1.50 -  Define a function \isa{norma} of type @{typ"'a aexp => 'a aexp"} that
    1.51 -  replaces \isa{IF}s with complex boolean conditions by nested
    1.52 -  \isa{IF}s where each condition is a \isa{Less} --- \isa{And} and
    1.53 -  \isa{Neg} should be eliminated completely. Prove that \isa{norma}
    1.54 -  preserves the value of an expression and that the result of \isa{norma}
    1.55 -  is really normal, i.e.\ no more \isa{And}s and \isa{Neg}s occur in
    1.56 +  Define a function @{text"norma"} of type @{typ"'a aexp => 'a aexp"} that
    1.57 +  replaces @{term"IF"}s with complex boolean conditions by nested
    1.58 +  @{term"IF"}s where each condition is a @{term"Less"} --- @{term"And"} and
    1.59 +  @{term"Neg"} should be eliminated completely. Prove that @{text"norma"}
    1.60 +  preserves the value of an expression and that the result of @{text"norma"}
    1.61 +  is really normal, i.e.\ no more @{term"And"}s and @{term"Neg"}s occur in
    1.62    it.  ({\em Hint:} proceed as in \S\ref{sec:boolex}).
    1.63  \end{exercise}
    1.64  *}