# HG changeset patch
# User huffman
# Date 1178729883 -7200
# Node ID ef91c38e7c0b9a1aa7a33e697caa5725053b8d89
# Parent  9449c991cc33efffce13ce5c30f7c8eccb4b6ee6
remove empty, unused theory

diff -r 9449c991cc33 -r ef91c38e7c0b src/HOL/Complex/ComplexBin.thy
--- 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
-