# HG changeset patch
# User wenzelm
# Date 936361319 -7200
# Node ID d09f39cd3b6e2311853c56bd7485b370881ed3fe
# Parent  f43d3670a3cd07ee0c7a652af4debf9686c593c3
from hyp;

diff -r f43d3670a3cd -r d09f39cd3b6e src/HOL/Isar_examples/MutilatedCheckerboard.thy
--- a/src/HOL/Isar_examples/MutilatedCheckerboard.thy	Fri Sep 03 13:55:46 1999 +0200
+++ b/src/HOL/Isar_examples/MutilatedCheckerboard.thy	Fri Sep 03 14:21:59 1999 +0200
@@ -126,7 +126,7 @@
     have "{(i, 2 * n), (i, 2 * n + 1)} : domino"; by (rule domino.horiz);
     also; have "{(i, 2 * n), (i, 2 * n + 1)} = ??a"; by blast;
     finally; show "... : domino"; .;
-    show "??B n : ??T"; by (rule hyp);
+    from hyp; show "??B n : ??T"; .;
     show "??a <= - ??B n"; by force;
   qed;
   finally; show "??P (Suc n)"; .;
@@ -144,7 +144,7 @@
   also; have "... : ??T";
   proof (rule tiling_Un [rulify]);
     show "??t : ??T"; by (rule dominoes_tile_row);
-    show "??B m : ??T"; by (rule hyp);
+    from hyp; show "??B m : ??T"; .;
     show "??t Int ??B m = {}"; by blast;
   qed;
   finally; show "??P (Suc m)"; .;
@@ -220,7 +220,7 @@
       qed;
     qed;
     hence "card (??e (a Un t) 0) = Suc (card (??e t 0))"; by simp;
-    also; have "card (??e t 0) = card (??e t 1)"; by (rule hyp);
+    also; from hyp; have "card (??e t 0) = card (??e t 1)"; .;
     also; from card_suc; have "Suc ... = card (??e (a Un t) 1)"; by simp;
     finally; show "??P (a Un t)"; .;
   qed;