src/HOL/Library/Library.thy
author nipkow
Wed Jan 26 16:39:44 2005 +0100 (2005-01-26)
changeset 15470 7e12ad2f6672
parent 15324 c27165172e30
child 15731 29ae73d8a84e
permissions -rw-r--r--
added OptionalSugar
     1 (*<*)
     2 theory Library
     3 imports
     4   Accessible_Part
     5   Continuity
     6   EfficientNat
     7   FuncSet
     8   List_Prefix
     9   Multiset
    10   NatPair
    11   Nat_Infinity
    12   Nested_Environment
    13   OptionalSugar
    14   Permutation
    15   Primes
    16   Quotient
    17   While_Combinator
    18   Word
    19   Zorn
    20 begin
    21 end
    22 (*>*)