src/HOL/HOLCF/IOA/Storage/Correctness.thy

   sim_relation :: "((nat * bool) * (nat set * bool)) set" where
   "sim_relation = {qua. let c = fst qua; a = snd qua ;
                             k = fst c;   b = snd c;
                             used = fst a; c = snd a
                         in
-                        (! l:used. l < k) & b=c}"
+                        (\<forall>l\<in>used. l < k) \<and> b=c}"
 
 declare split_paired_Ex [simp del]
 
 
 (* Idea: instead of impl_con_lemma do not rewrite impl_ioa, but derive