src/HOL/Complex_Main.thy
author haftmann
Sat, 19 Dec 2015 17:03:17 +0100
changeset 61891 76189756ff65
parent 60758 d8d85a8172b5
child 63570 1826a90b9cbc
permissions -rw-r--r--
documentation on last state of the art concerning interpretation
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
60758
d8d85a8172b5 isabelle update_cartouches;
wenzelm
parents: 58889
diff changeset
     1
section \<open>Comprehensive Complex Theory\<close>
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
51527
bd62e7ff103b move Ln.thy and Log.thy to Transcendental.thy
hoelzl
parents: 51522
diff changeset
     6
  Real
29879
4425849f5db7 Moved FTA into Lib and cleaned it up a little.
nipkow
parents: 29304
diff changeset
     7
  Complex
51527
bd62e7ff103b move Ln.thy and Log.thy to Transcendental.thy
hoelzl
parents: 51522
diff changeset
     8
  Transcendental
28952
15a4b2cf8c34 made repository layout more coherent with logical distribution structure; stripped some $Id$s
haftmann
parents: 28944
diff changeset
     9
  Taylor
35292
e4a431b6d9b7 Replaced Integration by Multivariate-Analysis/Real_Integration
hoelzl
parents: 33269
diff changeset
    10
  Deriv
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