src/HOL/Isar_examples/MutilatedCheckerboard.thy

     qed;
     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]);
+      by (rule tiling_domino_01 [symmetric]);
     finally; have "... < ..."; .; thus False; ..;
   qed;
 qed;
 
 end;