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

src/HOL/Library/Library.thy

author | kleing |

Sun Feb 19 13:21:32 2006 +0100 (2006-02-19) | |

changeset 19106 | 6e6b5b1fdc06 |

parent 18397 | 2d94eb7ff17f |

child 19234 | 054332e39e0a |

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 (*<*)

2 theory Library

3 imports

4 Accessible_Part

5 BigO

6 Continuity

7 EfficientNat

8 ExecutableSet

9 FuncSet

10 Multiset

11 NatPair

12 Nat_Infinity

13 Nested_Environment

14 OptionalSugar

15 Permutation

16 Primes

17 Quotient

18 While_Combinator

19 Word

20 Zorn

21 Char_ord

22 Commutative_Ring

23 Coinductive_List

24 ASeries

25 begin

26 end

27 (*>*)