author | wenzelm |
Thu, 18 Oct 2012 19:12:58 +0200 | |
changeset 49930 | defce6616890 |
parent 49926 | a9f5a7496258 |
child 49931 | 85780e6f8fd2 |
--- 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)"