| changeset 16417 | 9bc16273c2d4 |
| parent 11704 | 3c50a2cd6f00 |
| child 16563 | a92f96951355 |
| 16416:6061ae1f90f2 | 16417:9bc16273c2d4 |
|---|---|
7 the TFL package. |
7 the TFL package. |
8 *) |
8 *) |
9 |
9 |
10 header {* Primitive Recursive Functions *} |
10 header {* Primitive Recursive Functions *} |
11 |
11 |
12 theory Primrec = Main: |
12 theory Primrec imports Main begin |
13 |
13 |
14 text {* |
14 text {* |
15 Proof adopted from |
15 Proof adopted from |
16 |
16 |
17 Nora Szasz, A Machine Checked Proof that Ackermann's Function is not |
17 Nora Szasz, A Machine Checked Proof that Ackermann's Function is not |