src/HOL/Complex.thy
changeset 55759 fe3d8f585c20
parent 55734 3f5b2745d659
child 56217 dc429a5b13c4
     1.1 --- a/src/HOL/Complex.thy	Wed Feb 26 11:57:55 2014 +0100
     1.2 +++ b/src/HOL/Complex.thy	Wed Feb 26 15:33:52 2014 +0100
     1.3 @@ -623,7 +623,7 @@
     1.4    by (metis im_complex_div_eq_0 im_complex_div_gt_0 le_less)
     1.5  
     1.6  lemma re_complex_div_lt_0: "Re(a / b) < 0 \<longleftrightarrow> Re(a * cnj b) < 0"
     1.7 -  by (smt re_complex_div_eq_0 re_complex_div_gt_0)
     1.8 +  by (metis less_asym neq_iff re_complex_div_eq_0 re_complex_div_gt_0)
     1.9  
    1.10  lemma im_complex_div_lt_0: "Im(a / b) < 0 \<longleftrightarrow> Im(a * cnj b) < 0"
    1.11    by (metis im_complex_div_eq_0 im_complex_div_gt_0 less_asym neq_iff)