# HG changeset patch
# User nipkow
# Date 915553714 -3600
# Node ID e80bcb98df7893658421f17b6b6e3c770e7ee59d
# Parent  d30d1dd2082da4aa2c5eb1bff4905a180eb01dbe
1 proof now automatic.

diff -r d30d1dd2082d -r e80bcb98df78 src/HOL/UNITY/Lift.ML
--- a/src/HOL/UNITY/Lift.ML	Tue Jan 05 17:28:14 1999 +0100
+++ b/src/HOL/UNITY/Lift.ML	Tue Jan 05 17:28:34 1999 +0100
@@ -329,13 +329,6 @@
 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]));
-(*trans_tac (or decision procedures) could do the rest*)
-by (dres_inst_tac [("w1","Min")] (zle_iff_zadd RS iffD1) 2);
-by (dres_inst_tac [("z1","Max")] (zle_iff_zadd RS iffD1) 1);
-by (ALLGOALS (clarify_tac (claset() addSDs [zless_iff_Suc_zadd RS iffD1])));
-by (REPEAT_FIRST (eres_inst_tac [("P", "?x+?y = ?z")] rev_mp));
-by (REPEAT_FIRST (etac ssubst));
-by (auto_tac (claset(), simpset() addsimps [zadd_int]));
 qed "metric_eq_0D";
 
 AddDs [metric_eq_0D];