src/HOL/Isar_examples/MutilatedCheckerboard.thy

     qed;
   qed;
 qed;
 
 
-subsection {* Basic properties of below *};
+subsection {* Basic properties of ``below'' *};
 
 constdefs
   below :: "nat => nat set"
   "below n == {i. i < n}";
 

   by (simp add: below_def less_Suc_eq) blast;
 
 lemmas Sigma_Suc = Sigma_Suc1 Sigma_Suc2;
 
 
-subsection {* Basic properties of evnodd *};
+subsection {* Basic properties of ``evnodd'' *};
 
 constdefs
   evnodd :: "(nat * nat) set => nat => (nat * nat) set"
   "evnodd A b == A Int {(i, j). (i + j) mod 2 = b}";
 

       fix b; assume "b < 2";
       have "EX i j. ?e a b = {(i, j)}"; by (rule domino_singleton);
       thus "?thesis b";
       proof (elim exE);
 	have "?e (a Un t) b = ?e a b Un ?e t b"; by (rule evnodd_Un);
-	also; fix i j; assume e: "?e a b = {(i, j)}";
+	also; fix i j; assume "?e a b = {(i, j)}";
 	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);
 	  show "finite (?e t b)";
             by (rule evnodd_finite, rule tiling_domino_finite);

     also; from t; have "... = card (?e ?t 1)";
       by (rule tiling_domino_01);
     also; have "?e ?t 1 = ?e ?t'' 1"; by simp;
     also; from t''; have "card ... = card (?e ?t'' 0)";
       by (rule tiling_domino_01 [RS sym]);
-    finally; show False; ..;
+    finally; have "... < ..."; .; thus False; ..;
   qed;
 qed;
 
 end;