--- a/src/HOL/ex/Puzzle.thy Wed Sep 14 22:04:38 2005 +0200
+++ b/src/HOL/ex/Puzzle.thy Wed Sep 14 22:08:08 2005 +0200
@@ -8,6 +8,8 @@
Proof due to Herbert Ehler
*)
+header {* A question from ``Bundeswettbewerb Mathematik'' *}
+
theory Puzzle imports Main begin
consts f :: "nat => nat"