summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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/)

* 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$

4 Miscellaneous examples involving the Reals, Hyperreals, etc.

5 *)

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";

15 no_document use_thy "BigO";

16 use_thy "BigO_Complex";

18 use_thy "ASeries_Complex";

19 use_thy "HarmonicSeries";