isabelle: src/HOL/Complex/Complex_Main.thy@99f6da3bbbf7 (annotated)

13984 e055ba9020eb new theory Complex_Main as basis for analysis developments paulson parents: diff changeset	1	(* Title: HOL/Complex/Complex_Main.thy
e055ba9020eb new theory Complex_Main as basis for analysis developments paulson parents: diff changeset	2	ID: $Id$
e055ba9020eb new theory Complex_Main as basis for analysis developments paulson parents: diff changeset	3	Author: Lawrence C Paulson, Cambridge University Computer Laboratory
e055ba9020eb new theory Complex_Main as basis for analysis developments paulson parents: diff changeset	4	Copyright 2003 University of Cambridge
e055ba9020eb new theory Complex_Main as basis for analysis developments paulson parents: diff changeset	5	*)
e055ba9020eb new theory Complex_Main as basis for analysis developments paulson parents: diff changeset	6
e055ba9020eb new theory Complex_Main as basis for analysis developments paulson parents: diff changeset	7	header{Comprehensive Complex Theory}
e055ba9020eb new theory Complex_Main as basis for analysis developments paulson parents: diff changeset	8
15131 c69542757a4d New theory header syntax. nipkow parents: 13984 diff changeset	9	theory Complex_Main
27472 47bc28e011d5 removed nonstandard analysis theories to HOL-NSA huffman parents: 27368 diff changeset	10	imports
27541 9e585e99b494 tuned import haftmann parents: 27472 diff changeset	11	"../Main"
27472 47bc28e011d5 removed nonstandard analysis theories to HOL-NSA huffman parents: 27368 diff changeset	12	Fundamental_Theorem_Algebra
47bc28e011d5 removed nonstandard analysis theories to HOL-NSA huffman parents: 27368 diff changeset	13	"../Hyperreal/Log"
47bc28e011d5 removed nonstandard analysis theories to HOL-NSA huffman parents: 27368 diff changeset	14	"../Hyperreal/Ln"
47bc28e011d5 removed nonstandard analysis theories to HOL-NSA huffman parents: 27368 diff changeset	15	"../Hyperreal/Taylor"
47bc28e011d5 removed nonstandard analysis theories to HOL-NSA huffman parents: 27368 diff changeset	16	"../Hyperreal/Integration"
15131 c69542757a4d New theory header syntax. nipkow parents: 13984 diff changeset	17	begin
13984 e055ba9020eb new theory Complex_Main as basis for analysis developments paulson parents: diff changeset	18
e055ba9020eb new theory Complex_Main as basis for analysis developments paulson parents: diff changeset	19	end

author	wenzelm
	Thu, 13 Nov 2008 21:32:36 +0100
changeset 28749	99f6da3bbbf7
parent 27541	9e585e99b494
child 28866	30cd9d89a0fb
permissions	-rw-r--r--