doc-src/TutorialI/Datatype/document/ABexpr.tex
changeset 9924 3370f6aa3200
parent 9792 bbefb6ce5cb2
child 10171 59d6633835fa
equal deleted inserted replaced
9923:fe13743ffc8b 9924:3370f6aa3200
     1 %
     1 %
     2 \begin{isabellebody}%
     2 \begin{isabellebody}%
       
     3 \def\isabellecontext{ABexpr}%
     3 %
     4 %
     4 \begin{isamarkuptext}%
     5 \begin{isamarkuptext}%
     5 Sometimes it is necessary to define two datatypes that depend on each
     6 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
     7 other. This is called \textbf{mutual recursion}. As an example consider a
     7 language of arithmetic and boolean expressions where
     8 language of arithmetic and boolean expressions where