# HG changeset patch
# User wenzelm
# Date 936214539 -7200
# Node ID 132e8ed29bd82edab3942ce417ec7f63a9ed0eb6
# Parent  27887c52b9c8d1332ef270ab5c2897f47feecb85
tuned;

diff -r 27887c52b9c8 -r 132e8ed29bd8 src/HOL/Isar_examples/MutilatedCheckerboard.thy
--- a/src/HOL/Isar_examples/MutilatedCheckerboard.thy	Wed Sep 01 21:35:20 1999 +0200
+++ b/src/HOL/Isar_examples/MutilatedCheckerboard.thy	Wed Sep 01 21:35:39 1999 +0200
@@ -167,7 +167,7 @@
 
 lemma domino_finite: "d: domino ==> finite d";
 proof (induct set: domino);
-  fix i j;
+  fix i j :: nat;
   show "finite {(i, j), (i, j + 1)}"; by (intro Finites.intrs);
   show "finite {(i, j), (i + 1, j)}"; by (intro Finites.intrs);
 qed;
@@ -210,8 +210,7 @@
 	have "??e (a Un t) b = ??e a b Un ??e t b"; by (rule evnodd_Un);
 	also; fix i j; assume "??e a b = {(i, j)}";
 	also; have "... Un ??e t b = insert (i, j) (??e t b)"; by simp;
-	finally; have "card (??e (a Un t) b) = card (insert (i, j) (??e t b))"; by simp;
-	also; have "... = Suc (card (??e t b))";
+	also; have "card ... = Suc (card (??e t b))";
 	proof (rule card_insert_disjoint);
 	  show "finite (??e t b)"; by (rule evnodd_finite, rule tiling_domino_finite);
 	  have "(i, j) : ??e a b"; by asm_simp;