isabelle: src/HOL/Complex/ROOT.ML@7fa19d17f488 (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
21590 ef7278f553eb tuned spaces/comments; wenzelm parents: 21256 diff changeset	5	The Complex Numbers.
13957 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";
21256 47195501ecf7 moved theories Parity, GCD, Binomial to Library; wenzelm parents: 20809 diff changeset	9	no_document use_thy "Parity";
47195501ecf7 moved theories Parity, GCD, Binomial to Library; wenzelm parents: 20809 diff changeset	10
47195501ecf7 moved theories Parity, GCD, Binomial to Library; wenzelm parents: 20809 diff changeset	11	with_path "../Real" use_thy "Float";
13957 10dbf16be15f new session Complex for the complex numbers paulson parents: diff changeset	12	with_path "../Hyperreal" use_thy "Hyperreal";
21590 ef7278f553eb tuned spaces/comments; wenzelm parents: 21256 diff changeset	13	use_thy "Complex_Main";

author	haftmann
	Wed, 13 Dec 2006 15:45:33 +0100
changeset 21821	7fa19d17f488
parent 21590	ef7278f553eb
child 23916	0f8ad1044527
permissions	-rw-r--r--