src/HOL/Complex/ComplexBin.thy
author paulson
Thu Jul 01 12:29:53 2004 +0200 (2004-07-01)
changeset 15013 34264f5e4691
parent 14387 e96d5c42c4b0
child 15131 c69542757a4d
permissions -rw-r--r--
new treatment of binary numerals
paulson@13957
     1
(*  Title:      ComplexBin.thy
paulson@13957
     2
    Author:     Jacques D. Fleuriot
paulson@13957
     3
    Copyright:  2001 University of Edinburgh
paulson@13957
     4
    Descrition: Binary arithmetic for the complex numbers
paulson@13957
     5
                This case is reduced to that for the reals.
paulson@13957
     6
*)
paulson@13957
     7
paulson@14387
     8
theory ComplexBin = Complex:
paulson@13957
     9