--- a/src/HOL/Isar_Examples/Mutilated_Checkerboard.thy Wed Dec 28 15:08:12 2011 +0100
+++ b/src/HOL/Isar_Examples/Mutilated_Checkerboard.thy Wed Dec 28 20:03:13 2011 +0100
@@ -128,7 +128,7 @@
let ?a = "{i} <*> {2 * n + 1} Un {i} <*> {2 * n}"
have "?B (Suc n) = ?a Un ?B n"
by (auto simp add: Sigma_Suc Un_assoc)
- moreover have "... : ?T"
+ also have "... : ?T"
proof (rule tiling.Un)
have "{(i, 2 * n), (i, 2 * n + 1)} : domino"
by (rule domino.horiz)
@@ -137,7 +137,7 @@
show "?B n : ?T" by (rule Suc)
show "?a <= - ?B n" by blast
qed
- ultimately show ?case by simp
+ finally show ?case .
qed
lemma dominoes_tile_matrix:
@@ -150,13 +150,13 @@
case (Suc m)
let ?t = "{m} <*> below (2 * n)"
have "?B (Suc m) = ?t Un ?B m" by (simp add: Sigma_Suc)
- moreover have "... : ?T"
+ also have "... : ?T"
proof (rule tiling_Un)
show "?t : ?T" by (rule dominoes_tile_row)
show "?B m : ?T" by (rule Suc)
show "?t Int ?B m = {}" by blast
qed
- ultimately show ?case by simp
+ finally show ?case .
qed
lemma domino_singleton:
@@ -219,8 +219,8 @@
have "EX i j. ?e a b = {(i, j)}" by (rule domino_singleton)
then show ?thesis by (blast intro: that)
qed
- moreover have "... Un ?e t b = insert (i, j) (?e t b)" by simp
- moreover have "card ... = Suc (card (?e t b))"
+ also have "... Un ?e t b = insert (i, j) (?e t b)" by simp
+ also have "card ... = Suc (card (?e t b))"
proof (rule card_insert_disjoint)
from `t \<in> tiling domino` have "finite t"
by (rule tiling_domino_finite)
@@ -229,7 +229,7 @@
from e have "(i, j) : ?e a b" by simp
with at show "(i, j) ~: ?e t b" by (blast dest: evnoddD)
qed
- ultimately show "?thesis b" by simp
+ finally show "?thesis b" .
qed
then have "card (?e (a Un t) 0) = Suc (card (?e t 0))" by simp
also from hyp have "card (?e t 0) = card (?e t 1)" .