Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned proof;
authorwenzelm
Wed, 23 May 2012 13:33:35 +0200
changeset 47960 e462d33ca960
parent 47959 dba9409a3a5b
child 47961 e0a85be4fca0
tuned proof;
src/HOL/Isar_Examples/Drinker.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Isar_Examples/Drinker.thy	Wed May 23 13:32:29 2012 +0200
+++ b/src/HOL/Isar_Examples/Drinker.thy	Wed May 23 13:33:35 2012 +0200
@@ -17,18 +17,18 @@
 lemma de_Morgan:
   assumes "\<not> (\<forall>x. P x)"
   shows "\<exists>x. \<not> P x"
-  using assms
-proof (rule contrapos_np)
-  assume a: "\<not> (\<exists>x. \<not> P x)"
-  show "\<forall>x. P x"
+proof (rule classical)
+  assume "\<not> (\<exists>x. \<not> P x)"
+  have "\<forall>x. P x"
   proof
     fix x show "P x"
     proof (rule classical)
       assume "\<not> P x"
       then have "\<exists>x. \<not> P x" ..
-      with a show ?thesis by contradiction
+      with `\<not> (\<exists>x. \<not> P x)` show ?thesis by contradiction
     qed
   qed
+  with `\<not> (\<forall>x. P x)` show ?thesis ..
 qed
 
 theorem Drinker's_Principle: "\<exists>x. drunk x \<longrightarrow> (\<forall>x. drunk x)"
isabelle