changeset 29823 | 0ab754d13ccd |
parent 27982 | 2aaa4a5569a6 |
child 32960 | 69916a850301 |
29822:c45845743f04 | 29823:0ab754d13ccd |
---|---|
1 (* Title: HOL/Extraction/Pigeonhole.thy |
1 (* Title: HOL/Extraction/Pigeonhole.thy |
2 ID: $Id$ |
|
3 Author: Stefan Berghofer, TU Muenchen |
2 Author: Stefan Berghofer, TU Muenchen |
4 *) |
3 *) |
5 |
4 |
6 header {* The pigeonhole principle *} |
5 header {* The pigeonhole principle *} |
7 |
6 |