src/HOL/Isar_examples/MutilatedCheckerboard.thy

 
 consts
   tiling :: "'a set set => 'a set set";
 
 inductive "tiling A"
-  intrs
+  intros
     empty: "{} : tiling A"
     Un:    "a : A ==> t : tiling A ==> a <= - t
               ==> a Un t : tiling A";
 
 

 
 consts 
   domino  :: "(nat * nat) set set";
 
 inductive domino
-  intrs
+  intros
     horiz:  "{(i, j), (i, j + 1)} : domino"
     vertl:  "{(i, j), (i + 1, j)} : domino";
 
 lemma dominoes_tile_row:
   "{i} <*> below (2 * n) : tiling domino"

 qed;
 
 lemma domino_finite: "d: domino ==> finite d";
 proof (induct set: domino);
   fix i j :: nat;
-  show "finite {(i, j), (i, j + 1)}"; by (intro Finites.intrs);
-  show "finite {(i, j), (i + 1, j)}"; by (intro Finites.intrs);
+  show "finite {(i, j), (i, j + 1)}"; by (intro Finites.intros);
+  show "finite {(i, j), (i + 1, j)}"; by (intro Finites.intros);
 qed;
 
 
 subsection {* Tilings of dominoes *};