# HG changeset patch
# User boehmes
# Date 1393425232 -3600
# Node ID fe3d8f585c20e060ca793be7c50a6b6eb21df134
# Parent  385f7573f8f5b5ccebc9d05f4b3598fd56ef91bb
replaced smt-based proof with metis proof that requires no external tool

diff -r 385f7573f8f5 -r fe3d8f585c20 src/HOL/Complex.thy
--- a/src/HOL/Complex.thy	Wed Feb 26 11:57:55 2014 +0100
+++ b/src/HOL/Complex.thy	Wed Feb 26 15:33:52 2014 +0100
@@ -623,7 +623,7 @@
   by (metis im_complex_div_eq_0 im_complex_div_gt_0 le_less)
 
 lemma re_complex_div_lt_0: "Re(a / b) < 0 \<longleftrightarrow> Re(a * cnj b) < 0"
-  by (smt re_complex_div_eq_0 re_complex_div_gt_0)
+  by (metis less_asym neq_iff re_complex_div_eq_0 re_complex_div_gt_0)
 
 lemma im_complex_div_lt_0: "Im(a / b) < 0 \<longleftrightarrow> Im(a * cnj b) < 0"
   by (metis im_complex_div_eq_0 im_complex_div_gt_0 less_asym neq_iff)