# HG changeset patch
# User wenzelm
# Date 1350580378 -7200
# Node ID defce6616890af80ad44cdab458a68dc711b7e7c
# Parent  a9f5a74962581df9416594d21e0ddfce82f71f18
tuned proof;

diff -r a9f5a7496258 -r defce6616890 src/HOL/Isar_Examples/Drinker.thy
--- 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)"