tuned proof;
authorwenzelm
Thu Oct 18 19:12:58 2012 +0200 (2012-10-18)
changeset 49930defce6616890
parent 49926 a9f5a7496258
child 49931 85780e6f8fd2
tuned proof;
src/HOL/Isar_Examples/Drinker.thy
     1.1 --- a/src/HOL/Isar_Examples/Drinker.thy	Thu Oct 18 15:47:01 2012 +0200
     1.2 +++ b/src/HOL/Isar_Examples/Drinker.thy	Thu Oct 18 19:12:58 2012 +0200
     1.3 @@ -28,7 +28,7 @@
     1.4        with `\<not> (\<exists>x. \<not> P x)` show ?thesis by contradiction
     1.5      qed
     1.6    qed
     1.7 -  with `\<not> (\<forall>x. P x)` show ?thesis ..
     1.8 +  with `\<not> (\<forall>x. P x)` show ?thesis by contradiction
     1.9  qed
    1.10  
    1.11  theorem Drinker's_Principle: "\<exists>x. drunk x \<longrightarrow> (\<forall>x. drunk x)"