src/HOL/UNITY/FP.thy

--- a/src/HOL/UNITY/FP.thy	Sat Feb 08 14:46:22 2003 +0100
+++ b/src/HOL/UNITY/FP.thy	Sat Feb 08 16:05:33 2003 +0100
@@ -56,4 +56,7 @@
 lemma Diff_FP: "A - (FP F) = (UN act: Acts F. A - {s. act``{s} <= {s}})"
 by (simp add: Diff_eq Compl_FP)
 
+lemma totalize_FP [simp]: "FP (totalize F) = FP F"
+by (simp add: FP_def)
+
 end