src/HOL/Isar_examples/MutilatedCheckerboard.thy

   "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 in set: tiling);
+  proof induct;
     show "?P {}"; by simp;
 
     fix a t;
     assume "a : A" "t : ?T" "?P t" "a <= - t";
     show "?P (a Un t)";

   "[| d : domino; b < 2 |] ==> EX i j. evnodd d b = {(i, j)}";
 proof -;
   assume b: "b < 2";
   assume "d : domino";
   thus ?thesis (is "?P d");
-  proof (induct d in set: domino);
+  proof induct;
     from b; have b_cases: "b = 0 | b = 1"; by arith;
     fix i j;
     note [simp] = evnodd_empty evnodd_insert mod_Suc;
     from b_cases; show "?P {(i, j), (i, j + 1)}"; by rule auto;
     from b_cases; show "?P {(i, j), (i + 1, j)}"; by rule auto;

 lemma tiling_domino_finite:
   "t : tiling domino ==> finite t" (is "t : ?T ==> ?F t");
 proof -;
   assume "t : ?T";
   thus "?F t";
-  proof (induct t in set: tiling);
+  proof induct;
     show "?F {}"; by (rule Finites.emptyI);
     fix a t; assume "?F t";
     assume "a : domino"; hence "?F a"; by (rule domino_finite);
     thus "?F (a Un t)"; by (rule finite_UnI);
   qed;

   "t : tiling domino ==> card (evnodd t 0) = card (evnodd t 1)"
   (is "t : ?T ==> ?P t");
 proof -;
   assume "t : ?T";
   thus "?P t";
-  proof (induct t in set: tiling);
+  proof induct;
     show "?P {}"; by (simp add: evnodd_def);
 
     fix a t;
     let ?e = evnodd;
     assume "a : domino" "t : ?T"