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