src/HOL/UNITY/FP.thy
changeset 13812 91713a1915ee
parent 13798 4c1a53627500
child 15481 fc075ae929e4
     1.1 --- a/src/HOL/UNITY/FP.thy	Sat Feb 08 14:46:22 2003 +0100
     1.2 +++ b/src/HOL/UNITY/FP.thy	Sat Feb 08 16:05:33 2003 +0100
     1.3 @@ -56,4 +56,7 @@
     1.4  lemma Diff_FP: "A - (FP F) = (UN act: Acts F. A - {s. act``{s} <= {s}})"
     1.5  by (simp add: Diff_eq Compl_FP)
     1.6  
     1.7 +lemma totalize_FP [simp]: "FP (totalize F) = FP F"
     1.8 +by (simp add: FP_def)
     1.9 +
    1.10  end