src/HOL/Isar_examples/Puzzle.thy

--- a/src/HOL/Isar_examples/Puzzle.thy	Fri Jun 17 11:35:35 2005 +0200
+++ b/src/HOL/Isar_examples/Puzzle.thy	Fri Jun 17 16:12:49 2005 +0200
@@ -1,7 +1,7 @@
 
 header {* An old chestnut *}
 
-theory Puzzle = Main:
+theory Puzzle imports Main begin
 
 text_raw {*
  \footnote{A question from ``Bundeswettbewerb Mathematik''.  Original