changeset 16417 | 9bc16273c2d4 |
parent 11418 | 53a402c10ba9 |
16416:6061ae1f90f2 | 16417:9bc16273c2d4 |
---|---|
1 (*<*) |
1 (*<*) |
2 theory fakenat = Main:; |
2 theory fakenat imports Main begin; |
3 (*>*) |
3 (*>*) |
4 |
4 |
5 text{*\noindent |
5 text{*\noindent |
6 The type \tydx{nat} of natural |
6 The type \tydx{nat} of natural |
7 numbers is predefined to have the constructors \cdx{0} and~\cdx{Suc}. It behaves as if it were declared like this: |
7 numbers is predefined to have the constructors \cdx{0} and~\cdx{Suc}. It behaves as if it were declared like this: |