--- 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";