author paulson Wed, 10 Jan 2001 11:07:11 +0100 changeset 10844 0c0e7de7e9c5 parent 10843 f2e4e383dbca child 10845 3696bc935bbd
now using "by" for one-line proofs
--- a/doc-src/TutorialI/Rules/Blast.thy	Wed Jan 10 11:06:07 2001 +0100
+++ b/doc-src/TutorialI/Rules/Blast.thy	Wed Jan 10 11:07:11 2001 +0100
@@ -3,8 +3,7 @@

lemma "((\<exists>x. \<forall>y. p(x)=p(y)) = ((\<exists>x. q(x))=(\<forall>y. p(y))))   =
((\<exists>x. \<forall>y. q(x)=q(y)) = ((\<exists>x. p(x))=(\<forall>y. q(y))))"
-apply blast
-done
+by blast

text{*\noindent Until now, we have proved everything using only induction and
simplification.  Substantial proofs require more elaborate types of
@@ -16,13 +15,11 @@
(\<forall>x. cyclist(x) \<longrightarrow> industrious(x)) \<and>
(\<forall>x. \<not>healthy(x) \<and> cyclist(x) \<longrightarrow> \<not>honest(x))
\<longrightarrow> (\<forall>x. grocer(x) \<longrightarrow> \<not>cyclist(x))";
-apply blast
-done
+by blast

lemma "(\<Union>i\<in>I. A(i)) \<inter> (\<Union>j\<in>J. B(j)) =
(\<Union>i\<in>I. \<Union>j\<in>J. A(i) \<inter> B(j))"
-apply blast
-done
+by blast

text {*
@{thm[display] mult_is_0}