--- a/src/HOL/UNITY/Union.thy Fri Jun 17 11:35:35 2005 +0200 +++ b/src/HOL/UNITY/Union.thy Fri Jun 17 16:12:49 2005 +0200 @@ -8,7 +8,7 @@ header{*Unions of Programs*} -theory Union = SubstAx + FP: +theory Union imports SubstAx FP begin constdefs