| changeset 58372 | bfd497f2f4c2 |
| parent 39157 | b98909faaea8 |
| child 58889 | 5b7a9633cfa8 |
| 58371:7f30ec82fe40 | 58372:bfd497f2f4c2 |
|---|---|
3 *) |
3 *) |
4 |
4 |
5 header {* Auxiliary lemmas used in program extraction examples *} |
5 header {* Auxiliary lemmas used in program extraction examples *} |
6 |
6 |
7 theory Util |
7 theory Util |
8 imports Main |
8 imports Old_Datatype |
9 begin |
9 begin |
10 |
10 |
11 text {* |
11 text {* |
12 Decidability of equality on natural numbers. |
12 Decidability of equality on natural numbers. |
13 *} |
13 *} |