src/HOL/UNITY/FP.thy
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