isabelle: src/HOL/Complex/ex/ROOT.ML@93a34d5d1dc5 (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";
17198 ffe8efe856e3 added Complex/ex/BigO_Complex.thy; wenzelm parents: 13966 diff changeset	14
ffe8efe856e3 added Complex/ex/BigO_Complex.thy; wenzelm parents: 13966 diff changeset	15	no_document use_thy "BigO";
ffe8efe856e3 added Complex/ex/BigO_Complex.thy; wenzelm parents: 13966 diff changeset	16	use_thy "BigO_Complex";
19106 6e6b5b1fdc06 * added Library/ASeries (sum of arithmetic series with instantiation to nat and int) kleing parents: 17198 diff changeset	17
19358 9cd12369e753 remame ASeries to Arithmetic_Series kleing parents: 19109 diff changeset	18	use_thy "Arithmetic_Series_Complex";
19106 6e6b5b1fdc06 * added Library/ASeries (sum of arithmetic series with instantiation to nat and int) kleing parents: 17198 diff changeset	19	use_thy "HarmonicSeries";
19109 9804aa8d5756 fixed document kleing parents: 19108 diff changeset	20
9804aa8d5756 fixed document kleing parents: 19108 diff changeset	21	no_document use_thy "NatPair";
19108 6f8c1343341b * denumerability of rationals by Benjamin Porter, based on NatPair (by Stefan Richter) kleing parents: 19106 diff changeset	22	use_thy "DenumRat";
19640 40ec89317425 added Ferrante and Rackoff Algorithm -- by Amine Chaieb; wenzelm parents: 19469 diff changeset	23
40ec89317425 added Ferrante and Rackoff Algorithm -- by Amine Chaieb; wenzelm parents: 19469 diff changeset	24	use_thy "Ferrante_Rackoff_Ex";

author	huffman
	Wed, 23 Aug 2006 21:57:43 +0200
changeset 20407	93a34d5d1dc5
parent 19640	40ec89317425
child 23264	324622260d29
permissions	-rw-r--r--