src/HOL/Complex/Complex_Main.thy
author paulson
Thu, 08 May 2003 17:44:38 +0200
changeset 13984 e055ba9020eb
child 15131 c69542757a4d
permissions -rw-r--r--
new theory Complex_Main as basis for analysis developments
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
13984
e055ba9020eb new theory Complex_Main as basis for analysis developments
paulson
parents:
diff changeset
     1
(*  Title:      HOL/Complex/Complex_Main.thy
e055ba9020eb new theory Complex_Main as basis for analysis developments
paulson
parents:
diff changeset
     2
    ID:         $Id$
e055ba9020eb new theory Complex_Main as basis for analysis developments
paulson
parents:
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
e055ba9020eb new theory Complex_Main as basis for analysis developments
paulson
parents:
diff changeset
     4
    Copyright   2003  University of Cambridge
e055ba9020eb new theory Complex_Main as basis for analysis developments
paulson
parents:
diff changeset
     5
*)
e055ba9020eb new theory Complex_Main as basis for analysis developments
paulson
parents:
diff changeset
     6
e055ba9020eb new theory Complex_Main as basis for analysis developments
paulson
parents:
diff changeset
     7
header{*Comprehensive Complex Theory*}
e055ba9020eb new theory Complex_Main as basis for analysis developments
paulson
parents:
diff changeset
     8
e055ba9020eb new theory Complex_Main as basis for analysis developments
paulson
parents:
diff changeset
     9
theory Complex_Main = CLim:
e055ba9020eb new theory Complex_Main as basis for analysis developments
paulson
parents:
diff changeset
    10
e055ba9020eb new theory Complex_Main as basis for analysis developments
paulson
parents:
diff changeset
    11
end