(* 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 import Complex begin end