equal
deleted
inserted
replaced
1 \begin{isabelle}% |
1 % |
|
2 \begin{isabellebody}% |
2 % |
3 % |
3 \begin{isamarkuptext}% |
4 \begin{isamarkuptext}% |
4 So far, all datatypes had the property that on the right-hand side of their |
5 So far, all datatypes had the property that on the right-hand side of their |
5 definition they occurred only at the top-level, i.e.\ directly below a |
6 definition they occurred only at the top-level, i.e.\ directly below a |
6 constructor. This is not the case any longer for the following model of terms |
7 constructor. This is not the case any longer for the following model of terms |
119 |
120 |
120 Of course, you may also combine mutual and nested recursion. For example, |
121 Of course, you may also combine mutual and nested recursion. For example, |
121 constructor \isa{Sum} in \S\ref{sec:datatype-mut-rec} could take a list of |
122 constructor \isa{Sum} in \S\ref{sec:datatype-mut-rec} could take a list of |
122 expressions as its argument: \isa{Sum "'a aexp list"}.% |
123 expressions as its argument: \isa{Sum "'a aexp list"}.% |
123 \end{isamarkuptext}% |
124 \end{isamarkuptext}% |
124 \end{isabelle}% |
125 \end{isabellebody}% |
125 %%% Local Variables: |
126 %%% Local Variables: |
126 %%% mode: latex |
127 %%% mode: latex |
127 %%% TeX-master: "root" |
128 %%% TeX-master: "root" |
128 %%% End: |
129 %%% End: |