src/HOL/Library/Library.thy
author skalberg
Mon Mar 29 15:35:04 2004 +0200 (2004-03-29)
changeset 14494 48ae8d678d88
parent 14365 3d4df8c166ae
child 14706 71590b7733b7
permissions -rw-r--r--
Added bitvector library (Word) to HOL/Library and a theory using it (Adder)
to HOL/ex.
wenzelm@10253
     1
(*<*)
wenzelm@10253
     2
theory Library =
wenzelm@10332
     3
  Quotient +
oheimb@11349
     4
  Nat_Infinity +
wenzelm@10616
     5
  List_Prefix +
wenzelm@10943
     6
  Nested_Environment +
wenzelm@10253
     7
  Accessible_Part +
oheimb@11349
     8
  Continuity +
wenzelm@10253
     9
  Multiset +
wenzelm@11055
    10
  Permutation +
paulson@14127
    11
  NatPair +
wenzelm@11368
    12
  Primes +
skalberg@14494
    13
  Word +
nipkow@10984
    14
  While_Combinator:
wenzelm@10253
    15
end
wenzelm@10253
    16
(*>*)