src/ZF/UNITY/FP.thy
changeset 12195 ed2893765a08
parent 11479 697dcaaf478f
child 14092 68da54626309
--- a/src/ZF/UNITY/FP.thy	Wed Nov 14 23:22:43 2001 +0100
+++ b/src/ZF/UNITY/FP.thy	Thu Nov 15 15:07:16 2001 +0100
@@ -14,7 +14,7 @@
 
 constdefs   
   FP_Orig :: i=>i
-    "FP_Orig(F) == Union({A:condition. ALL B:condition. F : stable(A Int B)})"
+    "FP_Orig(F) == Union({A:Pow(state). ALL B. F : stable(A Int B)})"
 
   FP :: i=>i
     "FP(F) == {s:state. F : stable({s})}"