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})}"