now using "by" for one-line proofs
authorpaulson
Wed, 10 Jan 2001 11:13:11 +0100
changeset 10849 de981d0037ed
parent 10848 7b3ee4695fe6
child 10850 e1a793957a8f
now using "by" for one-line proofs
doc-src/TutorialI/Sets/Functions.thy
--- 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{*