# HG changeset patch
# User paulson
# Date 1052408678 -7200
# Node ID e055ba9020eb6fde87811a4c7a589bed6a1e85f6
# Parent  afc0dadddaa498c224819b0f0e47aee9f9500eb9
new theory Complex_Main as basis for analysis developments

diff -r afc0dadddaa4 -r e055ba9020eb src/HOL/Complex/Complex_Main.thy
--- /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
diff -r afc0dadddaa4 -r e055ba9020eb src/HOL/Complex/ROOT.ML
--- 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";
diff -r afc0dadddaa4 -r e055ba9020eb src/HOL/IsaMakefile
--- 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\