tuned proof;
authorwenzelm
Wed May 23 13:33:35 2012 +0200 (2012-05-23)
changeset 47960e462d33ca960
parent 47959 dba9409a3a5b
child 47961 e0a85be4fca0
tuned proof;
src/HOL/Isar_Examples/Drinker.thy
     1.1 --- a/src/HOL/Isar_Examples/Drinker.thy	Wed May 23 13:32:29 2012 +0200
     1.2 +++ b/src/HOL/Isar_Examples/Drinker.thy	Wed May 23 13:33:35 2012 +0200
     1.3 @@ -17,18 +17,18 @@
     1.4  lemma de_Morgan:
     1.5    assumes "\<not> (\<forall>x. P x)"
     1.6    shows "\<exists>x. \<not> P x"
     1.7 -  using assms
     1.8 -proof (rule contrapos_np)
     1.9 -  assume a: "\<not> (\<exists>x. \<not> P x)"
    1.10 -  show "\<forall>x. P x"
    1.11 +proof (rule classical)
    1.12 +  assume "\<not> (\<exists>x. \<not> P x)"
    1.13 +  have "\<forall>x. P x"
    1.14    proof
    1.15      fix x show "P x"
    1.16      proof (rule classical)
    1.17        assume "\<not> P x"
    1.18        then have "\<exists>x. \<not> P x" ..
    1.19 -      with a show ?thesis by contradiction
    1.20 +      with `\<not> (\<exists>x. \<not> P x)` show ?thesis by contradiction
    1.21      qed
    1.22    qed
    1.23 +  with `\<not> (\<forall>x. P x)` show ?thesis ..
    1.24  qed
    1.25  
    1.26  theorem Drinker's_Principle: "\<exists>x. drunk x \<longrightarrow> (\<forall>x. drunk x)"