src/HOL/UNITY/FP.ML

     "(!!B. stable Acts (A Int B)) ==> A <= FP Acts";
 by (simp_tac (simpset() addsimps [FP_equivalence, prem RS FP_Orig_weakest]) 1);
 qed "FP_weakest";
 
 Goalw [FP_def, stable_def, constrains_def]
-    "Compl (FP Acts) = (UN act:Acts. Compl{s. act^^{s} <= {s}})";
+    "-(FP Acts) = (UN act:Acts. -{s. act^^{s} <= {s}})";
 by (Blast_tac 1);
 qed "Compl_FP";
 
 Goal "A - (FP Acts) = (UN act:Acts. A - {s. act^^{s} <= {s}})";
 by (simp_tac (simpset() addsimps [Diff_eq, Compl_FP]) 1);