src/HOL/UNITY/Project.thy

--- a/src/HOL/UNITY/Project.thy	Wed Oct 27 13:02:23 1999 +0200
+++ b/src/HOL/UNITY/Project.thy	Wed Oct 27 13:03:32 1999 +0200
@@ -19,8 +19,7 @@
   extending :: "['c program => 'c set, 'a*'b => 'c, 'a program, 
 		 'c program set, 'c program set, 'a program set] => bool"
   "extending C h F X' Y' Y ==
-     ALL G. F Join project h (C G) G : Y & extend h F Join G : X' &
-            Disjoint UNIV (extend h F) G
+     ALL G. F Join project h (C G) G : Y & extend h F Join G : X'
             --> extend h F Join G : Y'"
 
 end