src/HOL/Library/Library.thy
author krauss
Mon Dec 04 15:15:59 2006 +0100 (2006-12-04)
changeset 21635 32f3e1127de2
parent 21256 47195501ecf7
child 22359 94a794672c8b
permissions -rw-r--r--
added Ramsey.thy to Library imports, to include it in the daily builds
wenzelm@20809
     1
(* $Id$ *)
wenzelm@10253
     2
(*<*)
nipkow@15131
     3
theory Library
nipkow@15140
     4
imports
wenzelm@21256
     5
  AssocList
avigad@16908
     6
  BigO
wenzelm@21256
     7
  Binomial
wenzelm@21256
     8
  Char_ord
wenzelm@21256
     9
  Coinductive_List
wenzelm@21256
    10
  Commutative_Ring
nipkow@15131
    11
  Continuity
berghofe@15324
    12
  EfficientNat
wenzelm@21256
    13
  ExecutableRat
berghofe@17633
    14
  ExecutableSet
wenzelm@21256
    15
  FuncSet
wenzelm@21256
    16
  GCD
wenzelm@21256
    17
  Infinite_Set
haftmann@20400
    18
  MLString
nipkow@15131
    19
  Multiset
nipkow@15131
    20
  NatPair
nipkow@15131
    21
  Nat_Infinity
nipkow@15131
    22
  Nested_Environment
nipkow@15470
    23
  OptionalSugar
wenzelm@21256
    24
  Parity
nipkow@15131
    25
  Permutation
nipkow@15131
    26
  Primes
nipkow@15131
    27
  Quotient
krauss@21635
    28
  Ramsey
wenzelm@21256
    29
  State_Monad
nipkow@15131
    30
  While_Combinator
nipkow@15131
    31
  Word
nipkow@15131
    32
  Zorn
nipkow@15131
    33
begin
wenzelm@10253
    34
end
wenzelm@10253
    35
(*>*)