src/HOL/Isar_examples/MutilatedCheckerboard.thy
changeset 9941 fe05af7ec816
parent 9906 5c027cca6262
child 10007 64bf7da1994a
     1.1 --- a/src/HOL/Isar_examples/MutilatedCheckerboard.thy	Tue Sep 12 19:03:13 2000 +0200
     1.2 +++ b/src/HOL/Isar_examples/MutilatedCheckerboard.thy	Tue Sep 12 22:13:23 2000 +0200
     1.3 @@ -154,7 +154,7 @@
     1.4  
     1.5    have "?B (Suc m) = ?t Un ?B m"; by (simp add: Sigma_Suc);
     1.6    also; have "... : ?T";
     1.7 -  proof (rule tiling_Un [rulified]);
     1.8 +  proof (rule tiling_Un [rule_format]);
     1.9      show "?t : ?T"; by (rule dominoes_tile_row);
    1.10      from hyp; show "?B m : ?T"; .;
    1.11      show "?t Int ?B m = {}"; by blast;