more robust syntax for definition/abbreviation/notation;
(* 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 ComplexBinimports Complexbeginend