# HG changeset patch # User wenzelm # Date 1337772815 -7200 # Node ID e462d33ca9605153af22412eccff8a10770eba55 # Parent dba9409a3a5bf2ba51e52a2e8d9c7f098c77db52 tuned proof; diff -r dba9409a3a5b -r e462d33ca960 src/HOL/Isar_Examples/Drinker.thy --- 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 "\ (\x. P x)" shows "\x. \ P x" - using assms -proof (rule contrapos_np) - assume a: "\ (\x. \ P x)" - show "\x. P x" +proof (rule classical) + assume "\ (\x. \ P x)" + have "\x. P x" proof fix x show "P x" proof (rule classical) assume "\ P x" then have "\x. \ P x" .. - with a show ?thesis by contradiction + with `\ (\x. \ P x)` show ?thesis by contradiction qed qed + with `\ (\x. P x)` show ?thesis .. qed theorem Drinker's_Principle: "\x. drunk x \ (\x. drunk x)"