src/HOL/Integ/IntDef.ML
changeset 6115 c70bce7deb0f
parent 6079 4f7975c74cdf
child 6674 32892a8ecb15
     1.1 --- a/src/HOL/Integ/IntDef.ML	Wed Jan 13 12:08:51 1999 +0100
     1.2 +++ b/src/HOL/Integ/IntDef.ML	Wed Jan 13 12:16:34 1999 +0100
     1.3 @@ -533,8 +533,6 @@
     1.4  by (simp_tac (simpset() addsimps [integ_le_less]) 1);
     1.5  qed "zle_refl";
     1.6  
     1.7 -AddIffs [le_refl];
     1.8 -
     1.9  Goalw [zle_def] "z < w ==> z <= (w::int)";
    1.10  by (blast_tac (claset() addEs [zless_asym]) 1);
    1.11  qed "zless_imp_zle";