# HG changeset patch
# User paulson
# Date 905761064 -7200
# Node ID d98a55f581c5c0f29c168e84e4e2e813e54eab9f
# Parent  0cd451e46a200bc1d39c3602644191c70fabed33
simpler proof

diff -r 0cd451e46a20 -r d98a55f581c5 src/HOL/UNITY/Lift.ML
--- a/src/HOL/UNITY/Lift.ML	Mon Sep 14 10:17:19 1998 +0200
+++ b/src/HOL/UNITY/Lift.ML	Mon Sep 14 10:17:44 1998 +0200
@@ -259,10 +259,10 @@
 by (etac (leI RS le_anti_sym RS sym) 1);
 by (REPEAT_FIRST (eresolve_tac mov_metrics));
 by (ALLGOALS metric_simp_tac);
+by (asm_simp_tac (simpset() addsimps [less_diff_conv, trans_le_add1]) 1);
 by (auto_tac
-    (claset() addEs [diff_less_Suc_diff RS less_not_refl3 RSN (2, rev_notE)]
-              addIs [diff_le_Suc_diff, diff_less_Suc_diff],
-	      simpset() addsimps [trans_le_add1]));
+    (claset() addEs [diff_less_Suc_diff RS less_not_refl3 RSN (2, rev_notE)],
+	      simpset()));
 qed "E_thm12b";