author | huffman |
Mon, 01 Dec 2008 15:36:48 -0800 | |
changeset 28944 | e27abf0db984 |
parent 28866 | 30cd9d89a0fb |
permissions | -rw-r--r-- |
(* Title: HOL/Complex/Complex_Main.thy ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 2003 University of Cambridge *) header{*Comprehensive Complex Theory*} theory Complex_Main imports "../Main" "../Real/ContNotDenum" "../Real/Real" Fundamental_Theorem_Algebra "../Hyperreal/Log" "../Hyperreal/Ln" "../Hyperreal/Taylor" "../Hyperreal/Integration" "../Hyperreal/FrechetDeriv" begin end