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/)
wenzelm@10253
     1
(*<*)
nipkow@15131
     2
theory Library
nipkow@15140
     3
imports
nipkow@15131
     4
  Accessible_Part
avigad@16908
     5
  BigO
nipkow@15131
     6
  Continuity
berghofe@15324
     7
  EfficientNat
berghofe@17633
     8
  ExecutableSet
nipkow@15131
     9
  FuncSet
nipkow@15131
    10
  Multiset
nipkow@15131
    11
  NatPair
nipkow@15131
    12
  Nat_Infinity
nipkow@15131
    13
  Nested_Environment
nipkow@15470
    14
  OptionalSugar
nipkow@15131
    15
  Permutation
nipkow@15131
    16
  Primes
nipkow@15131
    17
  Quotient
nipkow@15131
    18
  While_Combinator
nipkow@15131
    19
  Word
nipkow@15131
    20
  Zorn
nipkow@15731
    21
  Char_ord
wenzelm@17516
    22
  Commutative_Ring
wenzelm@18397
    23
  Coinductive_List
kleing@19106
    24
  ASeries
nipkow@15131
    25
begin
wenzelm@10253
    26
end
wenzelm@10253
    27
(*>*)