src/HOL/Isar_examples/MutilatedCheckerboard.thy

 next
   case (Suc n)
   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)
-  also have "... : ?T"
+  moreover have "... : ?T"
   proof (rule tiling.Un)
     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 Suc)
     show "?a <= - ?B n" by blast
   qed
-  finally show ?case .
+  ultimately show ?case by simp
 qed
 
 lemma dominoes_tile_matrix:
   "below m <*> below (2 * n) : tiling domino"
   (is "?B m : ?T")

   show ?case by (simp add: below_0 tiling.empty)
 next
   case (Suc m)
   let ?t = "{m} <*> below (2 * n)"
   have "?B (Suc m) = ?t Un ?B m" by (simp add: Sigma_Suc)
-  also have "... : ?T"
+  moreover 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
-  finally show ?case .
+  ultimately show ?case by simp
 qed
 
 lemma domino_singleton:
   assumes d: "d : domino" and "b < 2"
   shows "EX i j. evnodd d b = {(i, j)}"  (is "?P d")

     proof -
       from `a \<in> domino` and `b < 2`
       have "EX i j. ?e a b = {(i, j)}" by (rule domino_singleton)
       then show ?thesis by (blast intro: that)
     qed
-    also have "... Un ?e t b = insert (i, j) (?e t b)" by simp
-    also have "card ... = Suc (card (?e t b))"
+    moreover have "... Un ?e t b = insert (i, j) (?e t b)" by simp
+    moreover 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)
       then show "finite (?e t b)"
         by (rule evnodd_finite)
       from e have "(i, j) : ?e a b" by simp
       with at show "(i, j) ~: ?e t b" by (blast dest: evnoddD)
     qed
-    finally show "?thesis b" .
+    ultimately show "?thesis b" by simp
   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)" .
   also from card_suc have "Suc ... = card (?e (a Un t) 1)"
     by simp