isabelle: src/HOL/Complex/ROOT.ML@ef7278f553eb (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	wenzelm
	Wed, 29 Nov 2006 15:44:57 +0100
changeset 21590	ef7278f553eb
parent 21256	47195501ecf7
child 23916	0f8ad1044527
permissions	-rw-r--r--