# HG changeset patch
# User nipkow
# Date 916321151 -3600
# Node ID 6f049245afadfc4e4f0fcda0b2f3e32cb4bf377f
# Parent  2d9e609abcdbaa83f5b0c08ff34b0f11336e8c25
Removed superfluous arith rules from metric_simps

diff -r 2d9e609abcdb -r 6f049245afad src/HOL/UNITY/Lift.ML
--- a/src/HOL/UNITY/Lift.ML	Thu Jan 14 14:29:52 1999 +0100
+++ b/src/HOL/UNITY/Lift.ML	Thu Jan 14 14:39:11 1999 +0100
@@ -48,11 +48,7 @@
 
 
 val metric_simps =
-    [metric_def, vimage_def, order_less_imp_not_less, order_less_imp_triv, 
-     order_less_imp_not_eq, order_less_imp_not_eq2,
-     not_zless_zless1_eq, zless_not_sym RS not_zless_zless1_eq,
-     zless_zadd1_contra, zless_zadd1_contra',
-     zless_not_refl2, zless_not_refl3];
+    [metric_def, vimage_def];
 
 
 Addsimps [Lprg_def RS def_prg_Init];
@@ -323,8 +319,6 @@
 by (etac rev_mp 1);
 (*force simplification of "metric..." while in conclusion part*)
 by (asm_simp_tac (simpset() addsimps metric_simps) 1);
-by (auto_tac (claset() addIs [zleI, zle_anti_sym], 
-	      simpset() addsimps zcompare_rls@[zadd_int, integ_of_Min]));
 qed "metric_eq_0D";
 
 AddDs [metric_eq_0D];