changeset 5648 | fe887910e32e |
parent 4776 | 1f9362e769c1 |
child 13796 | 19f50fa807ae |
--- a/src/HOL/UNITY/FP.thy Wed Oct 14 15:47:22 1998 +0200 +++ b/src/HOL/UNITY/FP.thy Thu Oct 15 11:35:07 1998 +0200 @@ -12,10 +12,10 @@ constdefs - FP_Orig :: "('a * 'a)set set => 'a set" - "FP_Orig Acts == Union{A. ALL B. stable Acts (A Int B)}" + FP_Orig :: "'a program => 'a set" + "FP_Orig F == Union{A. ALL B. F : stable (A Int B)}" - FP :: "('a * 'a)set set => 'a set" - "FP Acts == {s. stable Acts {s}}" + FP :: "'a program => 'a set" + "FP F == {s. F : stable {s}}" end