isabelle: src/HOL/Complex/Complex_Main.thy@ec46381f149d (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
26118 6f94eb10adad Now imports Funamental_Theorem_Algebra chaieb parents: 22983 diff changeset	10	imports Fundamental_Theorem_Algebra CLim "../Hyperreal/Hyperreal"
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

author	wenzelm
	Wed, 07 May 2008 12:38:55 +0200
changeset 26840	ec46381f149d
parent 26118	6f94eb10adad
child 27368	9f90ac19e32b
permissions	-rw-r--r--