src/HOL/Library/Library.thy
author haftmann
Fri Jun 20 21:00:16 2008 +0200 (2008-06-20)
changeset 27298 a5373b60e66c
parent 26348 0f8e23edd357
child 27368 9f90ac19e32b
permissions -rw-r--r--
moved Float.thy to Library
wenzelm@20809
     1
(* $Id$ *)
wenzelm@10253
     2
(*<*)
nipkow@15131
     3
theory Library
nipkow@15140
     4
imports
haftmann@24197
     5
  Abstract_Rat
wenzelm@21256
     6
  AssocList
avigad@16908
     7
  BigO
wenzelm@21256
     8
  Binomial
kleing@24332
     9
  Boolean_Algebra
wenzelm@21256
    10
  Char_ord
haftmann@26170
    11
  Code_Char_chr
haftmann@24994
    12
  Code_Index
haftmann@26170
    13
  Code_Integer
haftmann@24994
    14
  Code_Message
wenzelm@21256
    15
  Coinductive_List
wenzelm@21256
    16
  Commutative_Ring
nipkow@15131
    17
  Continuity
haftmann@26170
    18
  Countable
chaieb@26157
    19
  Dense_Linear_Order
haftmann@23854
    20
  Efficient_Nat
haftmann@26348
    21
  Enum
haftmann@26170
    22
  Eval
haftmann@24281
    23
  Eval_Witness
haftmann@23854
    24
  Executable_Set
haftmann@27298
    25
  "../Real/Float"
wenzelm@21256
    26
  FuncSet
wenzelm@21256
    27
  GCD
haftmann@26170
    28
  Imperative_HOL
wenzelm@21256
    29
  Infinite_Set
wenzelm@26173
    30
  ListVector
nipkow@15131
    31
  Multiset
nipkow@15131
    32
  NatPair
nipkow@15131
    33
  Nat_Infinity
nipkow@15131
    34
  Nested_Environment
kleing@24332
    35
  Numeral_Type
nipkow@15470
    36
  OptionalSugar
haftmann@26232
    37
  Option_ord
nipkow@26272
    38
  Order_Relation
wenzelm@21256
    39
  Parity
nipkow@15131
    40
  Permutation
nipkow@15131
    41
  Primes
nipkow@24615
    42
  Quicksort
nipkow@15131
    43
  Quotient
krauss@21635
    44
  Ramsey
krauss@26192
    45
  RBT
wenzelm@21256
    46
  State_Monad
chaieb@26122
    47
  Univ_Poly
nipkow@15131
    48
  While_Combinator
nipkow@15131
    49
  Word
nipkow@15131
    50
  Zorn
nipkow@15131
    51
begin
wenzelm@10253
    52
end
wenzelm@10253
    53
(*>*)