--- a/doc-src/TutorialI/Sets/Functions.thy Wed Jan 10 00:15:33 2001 +0100
+++ b/doc-src/TutorialI/Sets/Functions.thy Wed Jan 10 10:40:34 2001 +0100
@@ -119,17 +119,17 @@
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