src/HOL/Isar_examples/MutilatedCheckerboard.thy

     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)";
       proof (rule card_Diff1_less);
-	show "finite (?e ?t' 0)";
-          by (rule finite_subset, rule fin) force;
+	from _ fin; show "finite (?e ?t' 0)";
+          by (rule finite_subset) 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)";