src/HOL/Library/Library.thy
author paulson
Thu Jul 24 16:37:04 2003 +0200 (2003-07-24)
changeset 14127 40a4768c8e0b
parent 11368 9c1995c73383
child 14266 08b34c902618
permissions -rw-r--r--
new theory NatPair of the injection from nat*nat -> nat
     1 (*<*)
     2 theory Library =
     3   Quotient +
     4   Ring_and_Field + Ring_and_Field_Example +
     5   Nat_Infinity +
     6   Rational_Numbers +
     7   List_Prefix +
     8   Nested_Environment +
     9   Accessible_Part +
    10   Continuity +
    11   Multiset +
    12   Permutation +
    13   NatPair +
    14   Primes +
    15   While_Combinator:
    16 end
    17 (*>*)