src/HOL/Complex/Complex_Main.thy
changeset 28994 49f602ae24e5
parent 28993 829e684b02ef
parent 28992 c4ae153d78ab
child 28995 d59b8124f1f5
child 29004 a5a91f387791
child 29010 5cd646abf6bc
child 29018 17538bdef546
child 29676 cfa3378decf7
--- a/src/HOL/Complex/Complex_Main.thy	Fri Dec 05 11:26:07 2008 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,22 +0,0 @@
-(*  Title:      HOL/Complex/Complex_Main.thy
-    ID:         $Id$
-    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
-    Copyright   2003  University of Cambridge
-*)
-
-header{*Comprehensive Complex Theory*}
-
-theory Complex_Main
-imports
-  "../Main"
-  "../Real/ContNotDenum"
-  "../Real/Real"
-  Fundamental_Theorem_Algebra
-  "../Hyperreal/Log"
-  "../Hyperreal/Ln"
-  "../Hyperreal/Taylor"
-  "../Hyperreal/Integration"
-  "../Hyperreal/FrechetDeriv"
-begin
-
-end