isabelle: src/HOL/Complex/ROOT.ML@070d176a8e2d (annotated)

13957 10dbf16be15f new session Complex for the complex numbers paulson parents: diff changeset	1	(* Title: HOL/Complex/ROOT.ML
10dbf16be15f new session Complex for the complex numbers paulson parents: diff changeset	2	ID: $Id$
10dbf16be15f new session Complex for the complex numbers paulson parents: diff changeset	3	Author: Jacques Fleuriot
10dbf16be15f new session Complex for the complex numbers paulson parents: diff changeset	4
10dbf16be15f new session Complex for the complex numbers paulson parents: diff changeset	5	The Complex Numbers
10dbf16be15f new session Complex for the complex numbers paulson parents: diff changeset	6	*)
10dbf16be15f new session Complex for the complex numbers paulson parents: diff changeset	7
20809 6c4fd0b4b63a moved theory Infinite_Set to Library; wenzelm parents: 16784 diff changeset	8	no_document use_thy "Infinite_Set";
16784 92ff7c903585 - added cplex package to HOL/Matrix obua parents: 14334 diff changeset	9	with_path "../Real" use_thy "Float";
13957 10dbf16be15f new session Complex for the complex numbers paulson parents: diff changeset	10	with_path "../Hyperreal" use_thy "Hyperreal";
13984 e055ba9020eb new theory Complex_Main as basis for analysis developments paulson parents: 13966 diff changeset	11	time_use_thy "Complex_Main";