src/HOL/Complex/Complex_Main.thy
author huffman
Thu Jul 03 17:58:10 2008 +0200 (2008-07-03)
changeset 27472 47bc28e011d5
parent 27368 9f90ac19e32b
child 27541 9e585e99b494
permissions -rw-r--r--
removed nonstandard analysis theories to HOL-NSA
paulson@13984
     1
(*  Title:      HOL/Complex/Complex_Main.thy
paulson@13984
     2
    ID:         $Id$
paulson@13984
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@13984
     4
    Copyright   2003  University of Cambridge
paulson@13984
     5
*)
paulson@13984
     6
paulson@13984
     7
header{*Comprehensive Complex Theory*}
paulson@13984
     8
nipkow@15131
     9
theory Complex_Main
huffman@27472
    10
imports
huffman@27472
    11
  Main
huffman@27472
    12
  Fundamental_Theorem_Algebra
huffman@27472
    13
  "../Hyperreal/Log"
huffman@27472
    14
  "../Hyperreal/Ln"
huffman@27472
    15
  "../Hyperreal/Taylor"
huffman@27472
    16
  "../Hyperreal/Integration"
nipkow@15131
    17
begin
paulson@13984
    18
paulson@13984
    19
end