changeset 1465 | 5d7a7e439cec |
parent 1266 | 3ae9fe3c0f68 |
child 1673 | d22110ddd0af |
1464:a608f83e3421 | 1465:5d7a7e439cec |
---|---|
1 (* Title: HOL/ex/puzzle.ML |
1 (* Title: HOL/ex/puzzle.ML |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Tobias Nipkow |
3 Author: Tobias Nipkow |
4 Copyright 1993 TU Muenchen |
4 Copyright 1993 TU Muenchen |
5 |
5 |
6 For puzzle.thy. A question from "Bundeswettbewerb Mathematik" |
6 For puzzle.thy. A question from "Bundeswettbewerb Mathematik" |
7 |
7 |
8 Proof due to Herbert Ehler |
8 Proof due to Herbert Ehler |