--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Complex/Complex_Main.thy Thu May 08 17:44:38 2003 +0200
@@ -0,0 +1,11 @@
+(* 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 = CLim:
+
+end
--- a/src/HOL/Complex/ROOT.ML Thu May 08 15:23:21 2003 +0200
+++ b/src/HOL/Complex/ROOT.ML Thu May 08 17:44:38 2003 +0200
@@ -8,4 +8,4 @@
no_document time_use_thy "Ring_and_Field";
with_path "../Real" use_thy "Real";
with_path "../Hyperreal" use_thy "Hyperreal";
-time_use_thy "CLim";
+time_use_thy "Complex_Main";
--- a/src/HOL/IsaMakefile Thu May 08 15:23:21 2003 +0200
+++ b/src/HOL/IsaMakefile Thu May 08 17:44:38 2003 +0200
@@ -165,6 +165,7 @@
Hyperreal/Star.ML Hyperreal/Star.thy Hyperreal/Transcendental.ML\
Hyperreal/Transcendental.thy Hyperreal/fuf.ML Hyperreal/hypreal_arith.ML \
Hyperreal/hypreal_arith0.ML\
+ Complex/Complex_Main.thy\
Complex/CLim.ML Complex/CLim.thy\
Complex/CSeries.ML Complex/CSeries.thy\
Complex/CStar.ML Complex/CStar.thy\