equal
deleted
inserted
replaced
4 *) |
4 *) |
5 |
5 |
6 header {* The pigeonhole principle *} |
6 header {* The pigeonhole principle *} |
7 |
7 |
8 theory Pigeonhole |
8 theory Pigeonhole |
9 imports EfficientNat |
9 imports Efficient_Nat |
10 begin |
10 begin |
11 |
11 |
12 text {* |
12 text {* |
13 We formalize two proofs of the pigeonhole principle, which lead |
13 We formalize two proofs of the pigeonhole principle, which lead |
14 to extracted programs of quite different complexity. The original |
14 to extracted programs of quite different complexity. The original |