src/HOL/NatDef.ML
changeset 6115 c70bce7deb0f
parent 6109 82b50115564c
child 7030 53934985426a
     1.1 --- a/src/HOL/NatDef.ML	Wed Jan 13 12:08:51 1999 +0100
     1.2 +++ b/src/HOL/NatDef.ML	Wed Jan 13 12:16:34 1999 +0100
     1.3 @@ -418,8 +418,6 @@
     1.4  by (simp_tac (simpset() addsimps [le_eq_less_or_eq]) 1);
     1.5  qed "le_refl";
     1.6  
     1.7 -AddIffs [le_refl];
     1.8 -
     1.9  
    1.10  Goal "[| i <= j; j < k |] ==> i < (k::nat)";
    1.11  by (blast_tac (claset() addSDs [le_imp_less_or_eq]