src/HOL/Complex/ex/ROOT.ML
author kleing
Sun Feb 19 13:21:32 2006 +0100 (2006-02-19)
changeset 19106 6e6b5b1fdc06
parent 17198 ffe8efe856e3
child 19108 6f8c1343341b
permissions -rw-r--r--
* added Library/ASeries (sum of arithmetic series with instantiation to nat and int)
* added Complex/ex/ASeries_Complex (instantiation of the above for reals)
* added Complex/ex/HarmonicSeries (should really be in something like Complex/Library)

(these are contributions by Benjamin Porter, numbers 68 and 34 of
http://www.cs.ru.nl/~freek/100/)
     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 "ASeries_Complex";
    19 use_thy "HarmonicSeries";