# HG changeset patch
# User wenzelm
# Date 1132159835 -3600
# Node ID 6e2fd2d276d3aaa71929f4d4988144fea7473cb6
# Parent  ef29685acef07b07ac5cb0c1be7d39689aa5b708
tuned;

diff -r ef29685acef0 -r 6e2fd2d276d3 src/HOL/Isar_examples/MutilatedCheckerboard.thy
--- a/src/HOL/Isar_examples/MutilatedCheckerboard.thy	Wed Nov 16 17:49:16 2005 +0100
+++ b/src/HOL/Isar_examples/MutilatedCheckerboard.thy	Wed Nov 16 17:50:35 2005 +0100
@@ -186,14 +186,11 @@
 lemma domino_finite:
   assumes "d: domino"
   shows "finite d"
-proof -
-  from `d: domino`
-  show ?thesis
-  proof induct
-    fix i j :: nat
-    show "finite {(i, j), (i, j + 1)}" by (intro Finites.intros)
-    show "finite {(i, j), (i + 1, j)}" by (intro Finites.intros)
-  qed
+  using prems
+proof induct
+  fix i j :: nat
+  show "finite {(i, j), (i, j + 1)}" by (intro Finites.intros)
+  show "finite {(i, j), (i + 1, j)}" by (intro Finites.intros)
 qed