# HG changeset patch
# User paulson
# Date 903624587 -7200
# Node ID a9f71e87f53e18c3c8fdc7f08ef1e3ff3a5225ff
# Parent  da63d9b35cafc6903552f44693df34b7cc061454
tidied

diff -r da63d9b35caf -r a9f71e87f53e src/HOL/Divides.ML
--- 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);
diff -r da63d9b35caf -r a9f71e87f53e src/HOL/List.ML
--- 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];
diff -r da63d9b35caf -r a9f71e87f53e src/HOL/UNITY/LessThan.ML
--- 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) = {}";