src/HOL/Predicate.thy

--- a/src/HOL/Predicate.thy	Sun Mar 03 20:27:42 2019 +0100
+++ b/src/HOL/Predicate.thy	Tue Mar 05 07:00:21 2019 +0000
@@ -78,11 +78,11 @@
 
 lemma eval_INF [simp]:
   "eval (\<Sqinter>(f ` A)) = \<Sqinter>((eval \<circ> f) ` A)"
-  by simp
+  by (simp add: image_comp)
 
 lemma eval_SUP [simp]:
   "eval (\<Squnion>(f ` A)) = \<Squnion>((eval \<circ> f) ` A)"
-  by simp
+  by (simp add: image_comp)
 
 instantiation pred :: (type) complete_boolean_algebra
 begin
@@ -400,7 +400,7 @@
 
 lemma eval_map [simp]:
   "eval (map f P) = (\<Squnion>x\<in>{x. eval P x}. (\<lambda>y. f x = y))"
-  by (auto simp add: map_def comp_def)
+  by (simp add: map_def comp_def image_comp)
 
 functor map: map
   by (rule ext, rule pred_eqI, auto)+