src/HOL/Library/Library.thy
changeset 15131 c69542757a4d
parent 14706 71590b7733b7
child 15140 322485b816ac
--- a/src/HOL/Library/Library.thy	Mon Aug 16 14:21:54 2004 +0200
+++ b/src/HOL/Library/Library.thy	Mon Aug 16 14:22:27 2004 +0200
@@ -1,18 +1,20 @@
 (*<*)
-theory Library =
-  Accessible_Part +
-  Continuity +
-  FuncSet +
-  List_Prefix +
-  Multiset +
-  NatPair +
-  Nat_Infinity +
-  Nested_Environment +
-  Permutation +
-  Primes +
-  Quotient +
-  While_Combinator +
-  Word +
-  Zorn:
+theory Library
+import
+  Accessible_Part
+  Continuity
+  FuncSet
+  List_Prefix
+  Multiset
+  NatPair
+  Nat_Infinity
+  Nested_Environment
+  Permutation
+  Primes
+  Quotient
+  While_Combinator
+  Word
+  Zorn
+begin
 end
 (*>*)