| author | huffman |
| Thu, 04 Dec 2008 12:32:38 -0800 | |
| changeset 28985 | af325cd29b15 |
| parent 28952 | 15a4b2cf8c34 |
| child 29026 | 5fbaa05f637f |
| permissions | -rw-r--r-- |
|
28952
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28944
diff
changeset
|
1 |
(* Title: HOL/Complex_Main.thy |
|
13984
e055ba9020eb
new theory Complex_Main as basis for analysis developments
paulson
parents:
diff
changeset
|
2 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
e055ba9020eb
new theory Complex_Main as basis for analysis developments
paulson
parents:
diff
changeset
|
3 |
Copyright 2003 University of Cambridge |
|
e055ba9020eb
new theory Complex_Main as basis for analysis developments
paulson
parents:
diff
changeset
|
4 |
*) |
|
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 |
header{*Comprehensive Complex Theory*}
|
|
e055ba9020eb
new theory Complex_Main as basis for analysis developments
paulson
parents:
diff
changeset
|
7 |
|
| 15131 | 8 |
theory Complex_Main |
| 27472 | 9 |
imports |
|
28952
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28944
diff
changeset
|
10 |
Main |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28944
diff
changeset
|
11 |
ContNotDenum |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28944
diff
changeset
|
12 |
Real |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28944
diff
changeset
|
13 |
"~~/src/HOL/Complex/Fundamental_Theorem_Algebra" |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28944
diff
changeset
|
14 |
Log |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28944
diff
changeset
|
15 |
Ln |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28944
diff
changeset
|
16 |
Taylor |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28944
diff
changeset
|
17 |
Integration |
|
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28944
diff
changeset
|
18 |
FrechetDeriv |
| 15131 | 19 |
begin |
|
13984
e055ba9020eb
new theory Complex_Main as basis for analysis developments
paulson
parents:
diff
changeset
|
20 |
|
|
e055ba9020eb
new theory Complex_Main as basis for analysis developments
paulson
parents:
diff
changeset
|
21 |
end |