src/HOL/UNITY/Union.thy
changeset 44928 7ef6505bde7f
parent 36866 426d5781bb25
child 45605 a89b4bc311a5
     1.1 --- a/src/HOL/UNITY/Union.thy	Wed Sep 14 10:55:07 2011 +0200
     1.2 +++ b/src/HOL/UNITY/Union.thy	Wed Sep 14 10:08:52 2011 -0400
     1.3 @@ -246,7 +246,7 @@
     1.4  by (simp add: invariant_def, blast)
     1.5  
     1.6  lemma FP_JN: "FP (\<Squnion>i \<in> I. F i) = (\<Inter>i \<in> I. FP (F i))"
     1.7 -by (simp add: FP_def JN_stable INTER_def)
     1.8 +by (simp add: FP_def JN_stable INTER_eq)
     1.9  
    1.10  
    1.11  subsection{*Progress: transient, ensures*}