src/HOL/ex/Puzzle.thy
changeset 17388 495c799df31d
parent 16417 9bc16273c2d4
child 23813 5440f9f5522c
     1.1 --- a/src/HOL/ex/Puzzle.thy	Wed Sep 14 22:04:38 2005 +0200
     1.2 +++ b/src/HOL/ex/Puzzle.thy	Wed Sep 14 22:08:08 2005 +0200
     1.3 @@ -8,6 +8,8 @@
     1.4  Proof due to Herbert Ehler
     1.5  *)
     1.6  
     1.7 +header {* A question from ``Bundeswettbewerb Mathematik'' *}
     1.8 +
     1.9  theory Puzzle imports Main begin
    1.10  
    1.11  consts f :: "nat => nat"