# HG changeset patch
# User paulson
# Date 859195648 -3600
# Node ID 9b47fc57ab7a4c845ee3e2620d00ed38ee4438ee
# Parent  9d07ba9eebc2838153b0588f0953f49a4f9f156a
Deleted unnecessary rules

diff -r 9d07ba9eebc2 -r 9b47fc57ab7a src/HOL/ex/Mutil.ML
--- 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";