src/HOL/Isar_examples/Puzzle.thy
changeset 8902 a705822f4e2a
parent 8020 2823ce1753a5
child 9870 2374ba026fc6
     1.1 --- a/src/HOL/Isar_examples/Puzzle.thy	Sun May 21 14:44:01 2000 +0200
     1.2 +++ b/src/HOL/Isar_examples/Puzzle.thy	Sun May 21 14:49:28 2000 +0200
     1.3 @@ -23,7 +23,7 @@
     1.4    (is "(!!x. ?H x ==> ?C x) ==> _");
     1.5  proof -;
     1.6    assume asm: "!!x. ?H x ==> ?C x";
     1.7 -  {{;
     1.8 +  {;
     1.9      fix k;
    1.10      have "ALL x. k = f x --> ?C x" (is "?Q k");
    1.11      proof (rule less_induct);
    1.12 @@ -38,7 +38,7 @@
    1.13  	qed;
    1.14        qed;
    1.15      qed;
    1.16 -  }};
    1.17 +  };
    1.18    thus "?C x"; by simp;
    1.19  qed;
    1.20