isabelle: src/HOL/Complex/ROOT.ML@b6be1d1b66c5 (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";
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";
13984 e055ba9020eb new theory Complex_Main as basis for analysis developments paulson parents: 13966 diff changeset	13	time_use_thy "Complex_Main";

author	haftmann
	Wed, 22 Nov 2006 10:20:15 +0100
changeset 21455	b6be1d1b66c5
parent 21256	47195501ecf7
child 21590	ef7278f553eb
permissions	-rw-r--r--