--- a/src/HOL/UNITY/LessThan.ML Thu Aug 20 16:47:52 1998 +0200
+++ b/src/HOL/UNITY/LessThan.ML Thu Aug 20 16:49:47 1998 +0200
@@ -50,10 +50,7 @@
Addsimps [greaterThan_0];
Goalw [greaterThan_def] "greaterThan (Suc k) = greaterThan k - {Suc k}";
-by Safe_tac;
-by (blast_tac (claset() addIs [less_trans]) 1);
-by (asm_simp_tac (simpset() addsimps [le_Suc_eq, not_le_iff_less RS sym]) 1);
-by (asm_simp_tac (simpset() addsimps [not_le_iff_less]) 1);
+by (auto_tac (claset() addEs [nat_neqE], simpset()));
qed "greaterThan_Suc";
Goal "(INT m. greaterThan m) = {}";