1
(* Title: ComplexBin.thy
2
Author: Jacques D. Fleuriot
3
Copyright: 2001 University of Edinburgh
4
Descrition: Binary arithmetic for the complex numbers
5
This case is reduced to that for the reals.
6
*)
7
8
theory ComplexBin
9
import Complex
10
begin
11
12
end
13