author | ballarin |
Thu, 11 Dec 2008 18:30:26 +0100 | |
changeset 29223 | e09c53289830 |
parent 29026 | 5fbaa05f637f |
child 29197 | 6d4cb27ed19c |
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 |
Real |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28944
diff
changeset
|
12 |
"~~/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
|
13 |
Log |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28944
diff
changeset
|
14 |
Ln |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28944
diff
changeset
|
15 |
Taylor |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28944
diff
changeset
|
16 |
Integration |
15a4b2cf8c34
made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents:
28944
diff
changeset
|
17 |
FrechetDeriv |
15131 | 18 |
begin |
13984
e055ba9020eb
new theory Complex_Main as basis for analysis developments
paulson
parents:
diff
changeset
|
19 |
|
e055ba9020eb
new theory Complex_Main as basis for analysis developments
paulson
parents:
diff
changeset
|
20 |
end |