doc-src/TutorialI/Sets/Functions.thy

 
 
 text{*
 illustrates Union as well as image
 *}
-lemma "f``A \<union> g``A = (\<Union>x\<in>A. {f x, g x})"
+lemma "f`A \<union> g`A = (\<Union>x\<in>A. {f x, g x})"
   apply (blast)
   done
 
-lemma "f `` {(x,y). P x y} = {f(x,y) | x y. P x y}"
+lemma "f ` {(x,y). P x y} = {f(x,y) | x y. P x y}"
   apply (blast)
   done
 
 text{*actually a macro!*}
 
-lemma "range f = f``UNIV"
+lemma "range f = f`UNIV"
   apply (blast)
   done
 
 
 text{*