--- a/src/HOL/ex/Mutil.ML Thu Mar 20 19:12:20 1997 +0100
+++ b/src/HOL/ex/Mutil.ML Mon Mar 24 10:27:28 1997 +0100
@@ -57,8 +57,8 @@
\ {(i, n1+n1), (i, Suc(n1+n1))}" 1);
by (Fast_tac 2);
by (asm_simp_tac (!simpset addsimps [domino.horiz]) 1);
-by (fast_tac (!claset addIs [equalityI, lessI] addEs [less_irrefl, less_asym]
- addDs [below_less_iff RS iffD1]) 1);
+by (fast_tac (!claset addEs [less_asym]
+ addSDs [below_less_iff RS iffD1]) 1);
qed "dominoes_tile_row";
goal thy "(below m) Times below(n + n) : tiling domino";