src/HOL/Complex/ex/ROOT.ML
author wenzelm
Sun Jun 10 21:06:59 2007 +0200 (2007-06-10)
changeset 23301 4c7e6d295980
parent 23264 324622260d29
child 23454 c54975167be9
permissions -rw-r--r--
disabled theories MIR and ReflectedFerrack for smlnj (temporarily);
     1 (*  Title:      HOL/Complex/ex/ROOT.ML
     2     ID:         $Id$
     3 
     4 Miscellaneous examples involving the Reals, Hyperreals, etc.
     5 *)
     6 
     7 use_thy "BinEx";
     8 no_document (with_path "../../NumberTheory" use_thy) "Factorization";
     9 (*These two examples just need the theory Primes.*)
    10 use_thy "Sqrt";
    11 use_thy "Sqrt_Script";
    12 (*This example also needs the theory Factorization.*)
    13 use_thy "NSPrimes";
    14 
    15 no_document use_thy "BigO";
    16 use_thy "BigO_Complex";
    17 
    18 use_thy "Arithmetic_Series_Complex";
    19 use_thy "HarmonicSeries";
    20 
    21 no_document use_thy "NatPair";
    22 use_thy "DenumRat";
    23 
    24 use_thy "Ferrante_Rackoff_Ex";
    25 
    26 if String.isPrefix "smlnj" ml_system then ()  (* FIXME tmp *)
    27 else use_thy "MIR";
    28 
    29 if String.isPrefix "smlnj" ml_system then ()  (* FIXME tmp *)
    30 else use_thy "ReflectedFerrack";