1.1 --- a/src/HOL/Divides.ML	Thu Aug 20 16:47:52 1998 +0200
     1.2 +++ b/src/HOL/Divides.ML	Thu Aug 20 16:49:47 1998 +0200
     1.3 @@ -243,7 +243,7 @@
     1.4  by (excluded_middle_tac "Suc(na)<n" 1);
     1.5  (* case Suc(na) < n *)
     1.6  by (forward_tac [lessI RS less_trans] 2);
     1.7 -by (asm_simp_tac (simpset() addsimps [mod_less, less_not_refl2 RS not_sym]) 2);
     1.8 +by (asm_simp_tac (simpset() addsimps [mod_less, less_not_refl3]) 2);
     1.9  (* case n <= Suc(na) *)
    1.10  by (asm_full_simp_tac (simpset() addsimps [not_less_iff_le, mod_geq]) 1);
    1.11  by (etac (le_imp_less_or_eq RS disjE) 1);

     2.1 --- a/src/HOL/List.ML	Thu Aug 20 16:47:52 1998 +0200
     2.2 +++ b/src/HOL/List.ML	Thu Aug 20 16:49:47 1998 +0200
     2.3 @@ -168,7 +168,7 @@
     2.4  by (exhaust_tac "ys" 1);
     2.5  by (fast_tac (claset() addIs [less_add_Suc2] 
     2.6  		       addss (simpset() delsimps [length_Suc_conv])
     2.7 -                       addEs [(less_not_refl2 RS not_sym) RSN (2,rev_notE)]) 1);
     2.8 +                       addEs [(less_not_refl3) RSN (2,rev_notE)]) 1);
     2.9  by (Asm_simp_tac 1);
    2.10  qed_spec_mp "append_eq_append_conv";
    2.11  Addsimps [append_eq_append_conv];

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