isabelle: src/HOL/Complex/ROOT.ML@b8bb6a6a2c46 (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
13966 2160abf7cfe7 removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex paulson parents: 13957 diff changeset	8	no_document time_use_thy "Ring_and_Field";
2160abf7cfe7 removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex paulson parents: 13957 diff changeset	9	with_path "../Real" use_thy "Real";
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";