(* 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