src/HOL/Complex/Complex_Main.thy
author nipkow
Wed, 18 Aug 2004 11:09:40 +0200
changeset 15140 322485b816ac
parent 15131 c69542757a4d
child 22655 83878e551c8c
permissions -rw-r--r--
import -> imports
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
15131
c69542757a4d New theory header syntax.
nipkow
parents: 13984
diff changeset
     9
theory Complex_Main
15140
322485b816ac import -> imports
nipkow
parents: 15131
diff changeset
    10
imports CLim
15131
c69542757a4d New theory header syntax.
nipkow
parents: 13984
diff changeset
    11
begin
13984
e055ba9020eb new theory Complex_Main as basis for analysis developments
paulson
parents:
diff changeset
    12
e055ba9020eb new theory Complex_Main as basis for analysis developments
paulson
parents:
diff changeset
    13
end