--- a/src/HOL/Divides.ML Thu Aug 20 16:47:52 1998 +0200
+++ b/src/HOL/Divides.ML Thu Aug 20 16:49:47 1998 +0200
@@ -243,7 +243,7 @@
by (excluded_middle_tac "Suc(na)<n" 1);
(* case Suc(na) < n *)
by (forward_tac [lessI RS less_trans] 2);
-by (asm_simp_tac (simpset() addsimps [mod_less, less_not_refl2 RS not_sym]) 2);
+by (asm_simp_tac (simpset() addsimps [mod_less, less_not_refl3]) 2);
(* case n <= Suc(na) *)
by (asm_full_simp_tac (simpset() addsimps [not_less_iff_le, mod_geq]) 1);
by (etac (le_imp_less_or_eq RS disjE) 1);
--- a/src/HOL/List.ML Thu Aug 20 16:47:52 1998 +0200
+++ b/src/HOL/List.ML Thu Aug 20 16:49:47 1998 +0200
@@ -168,7 +168,7 @@
by (exhaust_tac "ys" 1);
by (fast_tac (claset() addIs [less_add_Suc2]
addss (simpset() delsimps [length_Suc_conv])
- addEs [(less_not_refl2 RS not_sym) RSN (2,rev_notE)]) 1);
+ addEs [(less_not_refl3) RSN (2,rev_notE)]) 1);
by (Asm_simp_tac 1);
qed_spec_mp "append_eq_append_conv";
Addsimps [append_eq_append_conv];
--- 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) = {}";