--- a/src/ZF/UNITY/Union.thy Fri Jun 17 11:35:35 2005 +0200 +++ b/src/ZF/UNITY/Union.thy Fri Jun 17 16:12:49 2005 +0200 @@ -11,7 +11,7 @@ *) -theory Union = SubstAx + FP: +theory Union imports SubstAx FP begin constdefs