src/HOL/UNITY/Union.thy

      "[| F \<in> invariant A; G \<in> invariant A |]   
       ==> F\<squnion>G \<in> invariant A"
 by (simp add: invariant_def, blast)
 
 lemma FP_JN: "FP (\<Squnion>i \<in> I. F i) = (\<Inter>i \<in> I. FP (F i))"
-by (simp add: FP_def JN_stable INTER_def)
+by (simp add: FP_def JN_stable INTER_eq)
 
 
 subsection{*Progress: transient, ensures*}
 
 lemma JN_transient: