src/ZF/UNITY/Comp.thy

--- a/src/ZF/UNITY/Comp.thy	Fri Jun 17 11:35:35 2005 +0200
+++ b/src/ZF/UNITY/Comp.thy	Fri Jun 17 16:12:49 2005 +0200
@@ -16,7 +16,7 @@
 
 header{*Composition*}
 
-theory Comp = Union + Increasing:
+theory Comp imports Union Increasing begin
 
 constdefs