equal
deleted
inserted
replaced
1 % |
1 \begin{isabelle}% |
2 \begin{isabellebody}% |
|
3 % |
2 % |
4 \begin{isamarkuptext}% |
3 \begin{isamarkuptext}% |
5 Sometimes it is necessary to define two datatypes that depend on each |
4 Sometimes it is necessary to define two datatypes that depend on each |
6 other. This is called \textbf{mutual recursion}. As an example consider a |
5 other. This is called \textbf{mutual recursion}. As an example consider a |
7 language of arithmetic and boolean expressions where |
6 language of arithmetic and boolean expressions where |
110 preserves the value of an expression and that the result of \isa{norma} |
109 preserves the value of an expression and that the result of \isa{norma} |
111 is really normal, i.e.\ no more \isa{And}s and \isa{Neg}s occur in |
110 is really normal, i.e.\ no more \isa{And}s and \isa{Neg}s occur in |
112 it. ({\em Hint:} proceed as in \S\ref{sec:boolex}). |
111 it. ({\em Hint:} proceed as in \S\ref{sec:boolex}). |
113 \end{exercise}% |
112 \end{exercise}% |
114 \end{isamarkuptext}% |
113 \end{isamarkuptext}% |
115 \end{isabellebody}% |
114 \end{isabelle}% |
116 %%% Local Variables: |
115 %%% Local Variables: |
117 %%% mode: latex |
116 %%% mode: latex |
118 %%% TeX-master: "root" |
117 %%% TeX-master: "root" |
119 %%% End: |
118 %%% End: |