src/HOL/Complex/ex/ROOT.ML
author wenzelm
Sun, 10 Jun 2007 21:06:59 +0200
changeset 23301 4c7e6d295980
parent 23264 324622260d29
child 23454 c54975167be9
permissions -rw-r--r--
disabled theories MIR and ReflectedFerrack for smlnj (temporarily);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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";
23301
4c7e6d295980 disabled theories MIR and ReflectedFerrack for smlnj (temporarily);
wenzelm
parents: 23264
diff changeset
    25
4c7e6d295980 disabled theories MIR and ReflectedFerrack for smlnj (temporarily);
wenzelm
parents: 23264
diff changeset
    26
if String.isPrefix "smlnj" ml_system then ()  (* FIXME tmp *)
4c7e6d295980 disabled theories MIR and ReflectedFerrack for smlnj (temporarily);
wenzelm
parents: 23264
diff changeset
    27
else use_thy "MIR";
4c7e6d295980 disabled theories MIR and ReflectedFerrack for smlnj (temporarily);
wenzelm
parents: 23264
diff changeset
    28
4c7e6d295980 disabled theories MIR and ReflectedFerrack for smlnj (temporarily);
wenzelm
parents: 23264
diff changeset
    29
if String.isPrefix "smlnj" ml_system then ()  (* FIXME tmp *)
4c7e6d295980 disabled theories MIR and ReflectedFerrack for smlnj (temporarily);
wenzelm
parents: 23264
diff changeset
    30
else use_thy "ReflectedFerrack";