author | paulson |
Wed, 10 Jan 2001 11:13:11 +0100 | |
changeset 10849 | de981d0037ed |
parent 10848 | 7b3ee4695fe6 |
child 10850 | e1a793957a8f |
--- a/doc-src/TutorialI/Sets/Functions.thy Wed Jan 10 11:12:45 2001 +0100 +++ b/doc-src/TutorialI/Sets/Functions.thy Wed Jan 10 11:13:11 2001 +0100 @@ -119,19 +119,17 @@ text{* illustrates Union as well as image *} + lemma "f`A \<union> g`A = (\<Union>x\<in>A. {f x, g x})" - apply (blast) - done +by blast lemma "f ` {(x,y). P x y} = {f(x,y) | x y. P x y}" - apply (blast) - done +by blast text{*actually a macro!*} lemma "range f = f`UNIV" - apply (blast) - done +by blast text{*