author | huffman |
Wed, 09 May 2007 18:58:03 +0200 | |
changeset 22891 | ef91c38e7c0b |
parent 22890 | 9449c991cc33 |
child 22892 | c77a1e1c7323 |
src/HOL/Complex/ComplexBin.thy | file | annotate | diff | comparison | revisions |
--- a/src/HOL/Complex/ComplexBin.thy Wed May 09 18:26:40 2007 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,13 +0,0 @@ -(* 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 -