src/HOL/Library/Library.thy
author haftmann
Thu Jan 08 17:10:41 2009 +0100 (2009-01-08)
changeset 29399 ebcd69a00872
parent 29197 6d4cb27ed19c
child 29504 4c3441f2f619
permissions -rw-r--r--
split of Imperative_HOL theories from HOL-Library
wenzelm@20809
     1
(* $Id$ *)
wenzelm@10253
     2
(*<*)
nipkow@15131
     3
theory Library
nipkow@15140
     4
imports
haftmann@27652
     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
wenzelm@21256
    14
  Coinductive_List
wenzelm@21256
    15
  Commutative_Ring
nipkow@15131
    16
  Continuity
nipkow@29026
    17
  ContNotDenum
haftmann@26170
    18
  Countable
haftmann@23854
    19
  Efficient_Nat
haftmann@26348
    20
  Enum
haftmann@24281
    21
  Eval_Witness
haftmann@23854
    22
  Executable_Set
haftmann@28952
    23
  Float
wenzelm@21256
    24
  FuncSet
huffman@27475
    25
  Infinite_Set
wenzelm@26173
    26
  ListVector
nipkow@15131
    27
  Multiset
nipkow@15131
    28
  Nat_Infinity
nipkow@15131
    29
  Nested_Environment
kleing@24332
    30
  Numeral_Type
nipkow@15470
    31
  OptionalSugar
haftmann@26232
    32
  Option_ord
nipkow@15131
    33
  Permutation
wenzelm@28668
    34
  Pocklington
nipkow@15131
    35
  Primes
nipkow@24615
    36
  Quicksort
nipkow@15131
    37
  Quotient
krauss@21635
    38
  Ramsey
krauss@26192
    39
  RBT
wenzelm@21256
    40
  State_Monad
nipkow@15131
    41
  While_Combinator
nipkow@15131
    42
  Word
huffman@27475
    43
  Zorn
nipkow@15131
    44
begin
wenzelm@10253
    45
end
wenzelm@10253
    46
(*>*)