| changeset 28952 | 15a4b2cf8c34 |
| parent 28944 | e27abf0db984 |
| child 29026 | 5fbaa05f637f |
| 28948:1860f016886d | 28952:15a4b2cf8c34 |
|---|---|
1 (* Title: HOL/Complex_Main.thy |
|
2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
3 Copyright 2003 University of Cambridge |
|
4 *) |
|
5 |
|
6 header{*Comprehensive Complex Theory*} |
|
7 |
|
8 theory Complex_Main |
|
9 imports |
|
10 Main |
|
11 ContNotDenum |
|
12 Real |
|
13 "~~/src/HOL/Complex/Fundamental_Theorem_Algebra" |
|
14 Log |
|
15 Ln |
|
16 Taylor |
|
17 Integration |
|
18 FrechetDeriv |
|
19 begin |
|
20 |
|
21 end |