src/HOL/Set.thy

--- a/src/HOL/Set.thy	Wed Aug 22 12:31:57 2018 +0200
+++ b/src/HOL/Set.thy	Wed Aug 22 12:32:57 2018 +0000
@@ -981,6 +981,9 @@
 lemma range_composition: "range (\<lambda>x. f (g x)) = f ` range g"
   by auto
 
+lemma range_constant [simp]: "range (\<lambda>_. x) = {x}"
+  by (simp add: image_constant)
+
 lemma range_eq_singletonD: "range f = {a} \<Longrightarrow> f x = a"
   by auto