src/HOL/Complex_Main.thy
author chaieb
Fri, 30 Jan 2009 12:48:56 +0000
changeset 29693 708dcf7dec9f
parent 29304 5c71a6da989d
child 29879 4425849f5db7
permissions -rw-r--r--
moved upwards in thy graph, real related theorems moved to Transcendental.thy
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
29304
5c71a6da989d tuned header and description of boot files;
wenzelm
parents: 29197
diff changeset
     1
header {* Comprehensive Complex Theory *}
13984
e055ba9020eb new theory Complex_Main as basis for analysis developments
paulson
parents:
diff changeset
     2
15131
c69542757a4d New theory header syntax.
nipkow
parents: 13984
diff changeset
     3
theory Complex_Main
27472
47bc28e011d5 removed nonstandard analysis theories to HOL-NSA
huffman
parents: 27368
diff changeset
     4
imports
28952
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 28944
diff changeset
     5
  Main
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 28944
diff changeset
     6
  Real
29197
6d4cb27ed19c adapted HOL source structure to distribution layout
haftmann
parents: 29026
diff changeset
     7
  Fundamental_Theorem_Algebra
28952
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 28944
diff changeset
     8
  Log
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 28944
diff changeset
     9
  Ln
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 28944
diff changeset
    10
  Taylor
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 28944
diff changeset
    11
  Integration
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 28944
diff changeset
    12
  FrechetDeriv
15131
c69542757a4d New theory header syntax.
nipkow
parents: 13984
diff changeset
    13
begin
13984
e055ba9020eb new theory Complex_Main as basis for analysis developments
paulson
parents:
diff changeset
    14
e055ba9020eb new theory Complex_Main as basis for analysis developments
paulson
parents:
diff changeset
    15
end