equal
deleted
inserted
replaced
|
1 % |
|
2 \begin{isabellebody}% |
|
3 \def\isabellecontext{fakenat}% |
|
4 % |
|
5 \isadelimtheory |
|
6 % |
|
7 \endisadelimtheory |
|
8 % |
|
9 \isatagtheory |
|
10 % |
|
11 \endisatagtheory |
|
12 {\isafoldtheory}% |
|
13 % |
|
14 \isadelimtheory |
|
15 % |
|
16 \endisadelimtheory |
|
17 % |
|
18 \begin{isamarkuptext}% |
|
19 \noindent |
|
20 The type \tydx{nat} of natural |
|
21 numbers is predefined to have the constructors \cdx{0} and~\cdx{Suc}. It behaves as if it were declared like this:% |
|
22 \end{isamarkuptext}% |
|
23 \isamarkuptrue% |
|
24 \isacommand{datatype}\isamarkupfalse% |
|
25 \ nat\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}\ {\isaliteral{7C}{\isacharbar}}\ Suc\ nat% |
|
26 \isadelimtheory |
|
27 % |
|
28 \endisadelimtheory |
|
29 % |
|
30 \isatagtheory |
|
31 % |
|
32 \endisatagtheory |
|
33 {\isafoldtheory}% |
|
34 % |
|
35 \isadelimtheory |
|
36 % |
|
37 \endisadelimtheory |
|
38 \end{isabellebody}% |
|
39 %%% Local Variables: |
|
40 %%% mode: latex |
|
41 %%% TeX-master: "root" |
|
42 %%% End: |