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
Thu, 18 Oct 2012 19:12:58 +0200
changeset 49930 defce6616890
parent 49926 a9f5a7496258
child 49931 85780e6f8fd2
tuned proof;
src/HOL/Isar_Examples/Drinker.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Isar_Examples/Drinker.thy	Thu Oct 18 15:47:01 2012 +0200
+++ b/src/HOL/Isar_Examples/Drinker.thy	Thu Oct 18 19:12:58 2012 +0200
@@ -28,7 +28,7 @@
       with `\<not> (\<exists>x. \<not> P x)` show ?thesis by contradiction
     qed
   qed
-  with `\<not> (\<forall>x. P x)` show ?thesis ..
+  with `\<not> (\<forall>x. P x)` show ?thesis by contradiction
 qed
 
 theorem Drinker's_Principle: "\<exists>x. drunk x \<longrightarrow> (\<forall>x. drunk x)"
isabelle