src/HOL/Library/Library.thy
changeset 15131 c69542757a4d
parent 14706 71590b7733b7
child 15140 322485b816ac
     1.1 --- a/src/HOL/Library/Library.thy	Mon Aug 16 14:21:54 2004 +0200
     1.2 +++ b/src/HOL/Library/Library.thy	Mon Aug 16 14:22:27 2004 +0200
     1.3 @@ -1,18 +1,20 @@
     1.4  (*<*)
     1.5 -theory Library =
     1.6 -  Accessible_Part +
     1.7 -  Continuity +
     1.8 -  FuncSet +
     1.9 -  List_Prefix +
    1.10 -  Multiset +
    1.11 -  NatPair +
    1.12 -  Nat_Infinity +
    1.13 -  Nested_Environment +
    1.14 -  Permutation +
    1.15 -  Primes +
    1.16 -  Quotient +
    1.17 -  While_Combinator +
    1.18 -  Word +
    1.19 -  Zorn:
    1.20 +theory Library
    1.21 +import
    1.22 +  Accessible_Part
    1.23 +  Continuity
    1.24 +  FuncSet
    1.25 +  List_Prefix
    1.26 +  Multiset
    1.27 +  NatPair
    1.28 +  Nat_Infinity
    1.29 +  Nested_Environment
    1.30 +  Permutation
    1.31 +  Primes
    1.32 +  Quotient
    1.33 +  While_Combinator
    1.34 +  Word
    1.35 +  Zorn
    1.36 +begin
    1.37  end
    1.38  (*>*)