possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
(* Title: ComplexBin.thy
Author: Jacques D. Fleuriot
Copyright: 2001 University of Edinburgh
Descrition: Binary arithmetic for the complex numbers
This case is reduced to that for the reals.
*)
theory ComplexBin
imports Complex
begin
end