Complex/complex_real.ml

   1 (* ========================================================================= *)
   2 (* Trivial restriction of complex Groebner bases to reals.                   *)
   3 (* ========================================================================= *)
   4
   5 let GROBNER_REAL_ARITH =
   6   let trans_conv = GEN_REWRITE_CONV TOP_SWEEP_CONV
   7      [GSYM CX_INJ; CX_POW; CX_MUL; CX_ADD; CX_NEG; CX_SUB] in
   8   fun tm -> let th = trans_conv tm in
   9             EQ_MP (SYM th) (COMPLEX_ARITH(rand(concl th)));;