isabelle: src/HOL/Complex/ex/ROOT.ML@42f2f90b51a6 (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
23301 4c7e6d295980 disabled theories MIR and ReflectedFerrack for smlnj (temporarily); wenzelm parents: 23264 diff changeset	24	if String.isPrefix "smlnj" ml_system then () (* FIXME tmp *)
4c7e6d295980 disabled theories MIR and ReflectedFerrack for smlnj (temporarily); wenzelm parents: 23264 diff changeset	25	else use_thy "MIR";
4c7e6d295980 disabled theories MIR and ReflectedFerrack for smlnj (temporarily); wenzelm parents: 23264 diff changeset	26
4c7e6d295980 disabled theories MIR and ReflectedFerrack for smlnj (temporarily); wenzelm parents: 23264 diff changeset	27	if String.isPrefix "smlnj" ml_system then () (* FIXME tmp *)
4c7e6d295980 disabled theories MIR and ReflectedFerrack for smlnj (temporarily); wenzelm parents: 23264 diff changeset	28	else use_thy "ReflectedFerrack";

author	paulson
	Wed, 04 Jul 2007 13:56:26 +0200
changeset 23563	42f2f90b51a6
parent 23454	c54975167be9
child 24216	2e2d81b4f184
permissions	-rw-r--r--