src/HOL/List.ML
changeset 5355 a9f71e87f53e
parent 5318 72bf8039b53f
child 5425 157c6663dedd
     1.1 --- a/src/HOL/List.ML	Thu Aug 20 16:47:52 1998 +0200
     1.2 +++ b/src/HOL/List.ML	Thu Aug 20 16:49:47 1998 +0200
     1.3 @@ -168,7 +168,7 @@
     1.4  by (exhaust_tac "ys" 1);
     1.5  by (fast_tac (claset() addIs [less_add_Suc2] 
     1.6  		       addss (simpset() delsimps [length_Suc_conv])
     1.7 -                       addEs [(less_not_refl2 RS not_sym) RSN (2,rev_notE)]) 1);
     1.8 +                       addEs [(less_not_refl3) RSN (2,rev_notE)]) 1);
     1.9  by (Asm_simp_tac 1);
    1.10  qed_spec_mp "append_eq_append_conv";
    1.11  Addsimps [append_eq_append_conv];