src/HOL/Isar_examples/Puzzle.thy

--- a/src/HOL/Isar_examples/Puzzle.thy	Sun May 21 14:44:01 2000 +0200
+++ b/src/HOL/Isar_examples/Puzzle.thy	Sun May 21 14:49:28 2000 +0200
@@ -23,7 +23,7 @@
   (is "(!!x. ?H x ==> ?C x) ==> _");
 proof -;
   assume asm: "!!x. ?H x ==> ?C x";
-  {{;
+  {;
     fix k;
     have "ALL x. k = f x --> ?C x" (is "?Q k");
     proof (rule less_induct);
@@ -38,7 +38,7 @@
 	qed;
       qed;
     qed;
-  }};
+  };
   thus "?C x"; by simp;
 qed;