isabelle: src/HOL/Complex/ex/ROOT.ML@dbb34a03af5a (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
24216 2e2d81b4f184 simultaneous use_thys; wenzelm parents: 23454 diff changeset	4	Miscellaneous examples.
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
24216 2e2d81b4f184 simultaneous use_thys; wenzelm parents: 23454 diff changeset	7	no_document use_thys [
2e2d81b4f184 simultaneous use_thys; wenzelm parents: 23454 diff changeset	8	"../../NumberTheory/Factorization",
2e2d81b4f184 simultaneous use_thys; wenzelm parents: 23454 diff changeset	9	"BigO",
2e2d81b4f184 simultaneous use_thys; wenzelm parents: 23454 diff changeset	10	"NatPair"
2e2d81b4f184 simultaneous use_thys; wenzelm parents: 23454 diff changeset	11	];
17198 ffe8efe856e3 added Complex/ex/BigO_Complex.thy; wenzelm parents: 13966 diff changeset	12
24216 2e2d81b4f184 simultaneous use_thys; wenzelm parents: 23454 diff changeset	13	use_thys [
2e2d81b4f184 simultaneous use_thys; wenzelm parents: 23454 diff changeset	14	"BinEx",
2e2d81b4f184 simultaneous use_thys; wenzelm parents: 23454 diff changeset	15	"Sqrt",
2e2d81b4f184 simultaneous use_thys; wenzelm parents: 23454 diff changeset	16	"Sqrt_Script",
2e2d81b4f184 simultaneous use_thys; wenzelm parents: 23454 diff changeset	17	"NSPrimes",
2e2d81b4f184 simultaneous use_thys; wenzelm parents: 23454 diff changeset	18	"BigO_Complex",
19106 6e6b5b1fdc06 * added Library/ASeries (sum of arithmetic series with instantiation to nat and int) kleing parents: 17198 diff changeset	19
24216 2e2d81b4f184 simultaneous use_thys; wenzelm parents: 23454 diff changeset	20	"Arithmetic_Series_Complex",
2e2d81b4f184 simultaneous use_thys; wenzelm parents: 23454 diff changeset	21	"HarmonicSeries",
19109 9804aa8d5756 fixed document kleing parents: 19108 diff changeset	22
24631 c7da302a0346 reactivated tests in smlnj; wenzelm parents: 24216 diff changeset	23	"DenumRat",
c7da302a0346 reactivated tests in smlnj; wenzelm parents: 24216 diff changeset	24
c7da302a0346 reactivated tests in smlnj; wenzelm parents: 24216 diff changeset	25	"MIR",
c7da302a0346 reactivated tests in smlnj; wenzelm parents: 24216 diff changeset	26	"ReflectedFerrack"
24216 2e2d81b4f184 simultaneous use_thys; wenzelm parents: 23454 diff changeset	27	];
19640 40ec89317425 added Ferrante and Rackoff Algorithm -- by Amine Chaieb; wenzelm parents: 19469 diff changeset	28

author	haftmann
	Sat, 29 Sep 2007 08:58:56 +0200
changeset 24751	dbb34a03af5a
parent 24631	c7da302a0346
permissions	-rw-r--r--