isabelle: src/HOL/Complex/ex/ROOT.ML@0bd9eedaa301 (annotated)

13966 2160abf7cfe7 removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex paulson parents: 13957 diff changeset	1	(* Title: HOL/Complex/ex/ROOT.ML
13957 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
13966 2160abf7cfe7 removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex paulson parents: 13957 diff changeset	4	Miscellaneous examples involving the Reals, Hyperreals, etc.
13957 10dbf16be15f new session Complex for the complex numbers paulson parents: diff changeset	5	*)
10dbf16be15f new session Complex for the complex numbers paulson parents: diff changeset	6
13966 2160abf7cfe7 removal of the image HOL-Real and merging of HOL-Real-ex with HOL-Complex-ex paulson parents: 13957 diff changeset	7	use_thy "BinEx";
13957 10dbf16be15f new session Complex for the complex numbers paulson parents: diff changeset	8	no_document (with_path "../../NumberTheory" use_thy) "Factorization";
10dbf16be15f new session Complex for the complex numbers paulson parents: diff changeset	9	(These two examples just need the theory Primes.)
10dbf16be15f new session Complex for the complex numbers paulson parents: diff changeset	10	use_thy "Sqrt";
10dbf16be15f new session Complex for the complex numbers paulson parents: diff changeset	11	use_thy "Sqrt_Script";
10dbf16be15f new session Complex for the complex numbers paulson parents: diff changeset	12	(This example also needs the theory Factorization.)
10dbf16be15f new session Complex for the complex numbers paulson parents: diff changeset	13	use_thy "NSPrimes";

author	nipkow
	Mon, 22 Nov 2004 11:53:56 +0100
changeset 15305	0bd9eedaa301
parent 13966	2160abf7cfe7
child 17198	ffe8efe856e3
permissions	-rw-r--r--