src/HOL/Isar_examples/MutilatedCheckerboard.thy

   tiling :: "'a set set => 'a set set";
 
 inductive "tiling A"
   intrs
     empty: "{} : tiling A"
-    Un:    "[| a : A;  t : tiling A;  a <= - t |] ==> a Un t : tiling A";
-
-
-text "The union of two disjoint tilings is a tiling";
+    Un:    "[| a : A;  t : tiling A;  a <= - t |]
+              ==> a Un t : tiling A";
+
+
+text "The union of two disjoint tilings is a tiling.";
 
 lemma tiling_Un:
-  "t : tiling A --> u : tiling A --> t Int u = {} --> t Un u : tiling A";
+  "t : tiling A --> u : tiling A --> t Int u = {}
+    --> t Un u : tiling A";
 proof;
   assume "t : tiling A" (is "_ : ?T");
   thus "u : ?T --> t Int u = {} --> t Un u : ?T" (is "?P t");
   proof (induct t set: tiling);
     show "?P {}"; by simp;

 inductive domino
   intrs
     horiz:  "{(i, j), (i, j + 1)} : domino"
     vertl:  "{(i, j), (i + 1, j)} : domino";
 
-lemma dominoes_tile_row: "{i} Times below (2 * n) : tiling domino"
+lemma dominoes_tile_row:
+  "{i} Times below (2 * n) : tiling domino"
   (is "?P n" is "?B n : ?T");
 proof (induct n);
   show "?P 0"; by (simp add: below_0 tiling.empty);
 
   fix n; assume hyp: "?P n";

       by (rule evnodd_finite, rule tiling_domino_finite, rule t);
 
     note [simp] = evnodd_iff evnodd_empty evnodd_insert evnodd_Diff;
     have "card (?e ?t'' 0) < card (?e ?t' 0)";
     proof -;
-      have "card (?e ?t' 0 - {(2 * m + 1, 2 * n + 1)}) < card (?e ?t' 0)";
+      have "card (?e ?t' 0 - {(2 * m + 1, 2 * n + 1)})
+        < card (?e ?t' 0)";
       proof (rule card_Diff1_less);
-	show "finite (?e ?t' 0)"; by (rule finite_subset, rule fin) force;
+	show "finite (?e ?t' 0)";
+          by (rule finite_subset, rule fin) force;
 	show "(2 * m + 1, 2 * n + 1) : ?e ?t' 0"; by simp;
       qed;
       thus ?thesis; by simp;
     qed;
     also; have "... < card (?e ?t 0)";

       have "(0, 0) : ?e ?t 0"; by simp;
       with fin; have "card (?e ?t 0 - {(0, 0)}) < card (?e ?t 0)";
         by (rule card_Diff1_less);
       thus ?thesis; by simp;
     qed;
-    also; from t; have "... = card (?e ?t 1)"; by (rule tiling_domino_01);
+    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; ..;
   qed;