src/HOL/Library/Library.thy
author paulson
Tue Jan 27 15:39:51 2004 +0100 (2004-01-27)
changeset 14365 3d4df8c166ae
parent 14266 08b34c902618
child 14494 48ae8d678d88
permissions -rw-r--r--
replacing HOL/Real/PRat, PNat by the rational number development
of Markus Wenzel
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 +
nipkow@10984
    13
  While_Combinator:
wenzelm@10253
    14
end
wenzelm@10253
    15
(*>*)