equal
deleted
inserted
replaced
1 \begin{isabelle}% |
1 % |
|
2 \begin{isabellebody}% |
2 % |
3 % |
3 \begin{isamarkuptext}% |
4 \begin{isamarkuptext}% |
4 \noindent |
5 \noindent |
5 The type \isaindexbold{nat}\index{*0|bold}\index{*Suc|bold} of natural |
6 The type \isaindexbold{nat}\index{*0|bold}\index{*Suc|bold} of natural |
6 numbers is predefined and behaves like% |
7 numbers is predefined and behaves like% |
7 \end{isamarkuptext}% |
8 \end{isamarkuptext}% |
8 \isacommand{datatype}\ nat\ {\isacharequal}\ \isadigit{0}\ {\isacharbar}\ Suc\ nat\end{isabelle}% |
9 \isacommand{datatype}\ nat\ {\isacharequal}\ \isadigit{0}\ {\isacharbar}\ Suc\ nat\end{isabellebody}% |
9 %%% Local Variables: |
10 %%% Local Variables: |
10 %%% mode: latex |
11 %%% mode: latex |
11 %%% TeX-master: "root" |
12 %%% TeX-master: "root" |
12 %%% End: |
13 %%% End: |