# HG changeset patch
# User berghofe
# Date 1170866763 -3600
# Node ID 9785397cc344de3b6f9b2d643398c423287777df
# Parent  aac2ac7c32fdffbd514f45d0f5e1592acc868e5f
Adapted to changes in Finite_Set theory.

diff -r aac2ac7c32fd -r 9785397cc344 src/HOL/Isar_examples/MutilatedCheckerboard.thy
--- a/src/HOL/Isar_examples/MutilatedCheckerboard.thy	Wed Feb 07 17:45:03 2007 +0100
+++ b/src/HOL/Isar_examples/MutilatedCheckerboard.thy	Wed Feb 07 17:46:03 2007 +0100
@@ -186,8 +186,8 @@
   using d
 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)
+  show "finite {(i, j), (i, j + 1)}" by (intro finite.intros)
+  show "finite {(i, j), (i + 1, j)}" by (intro finite.intros)
 qed
 
 
@@ -198,7 +198,7 @@
   shows "finite t"  (is "?F t")
   using t
 proof induct
-  show "?F {}" by (rule Finites.emptyI)
+  show "?F {}" by (rule finite.emptyI)
   fix a t assume "?F t"
   assume "a : domino" then have "?F a" by (rule domino_finite)
   then show "?F (a Un t)" by (rule finite_UnI)