tuned proofs;
authorwenzelm
Wed Jul 22 14:55:42 2015 +0200 (2015-07-22)
changeset 6076676560ce8dead
parent 60765 e43e71a75838
child 60767 ad5b4771fc19
tuned proofs;
src/HOL/Isar_Examples/Drinker.thy
     1.1 --- a/src/HOL/Isar_Examples/Drinker.thy	Tue Jul 21 19:04:36 2015 +0200
     1.2 +++ b/src/HOL/Isar_Examples/Drinker.thy	Wed Jul 22 14:55:42 2015 +0200
     1.3 @@ -33,17 +33,17 @@
     1.4  
     1.5  theorem Drinker's_Principle: "\<exists>x. drunk x \<longrightarrow> (\<forall>x. drunk x)"
     1.6  proof cases
     1.7 -  fix a assume "\<forall>x. drunk x"
     1.8 -  then have "drunk a \<longrightarrow> (\<forall>x. drunk x)" ..
     1.9 +  assume "\<forall>x. drunk x"
    1.10 +  then have "drunk a \<longrightarrow> (\<forall>x. drunk x)" for a ..
    1.11    then show ?thesis ..
    1.12  next
    1.13    assume "\<not> (\<forall>x. drunk x)"
    1.14    then have "\<exists>x. \<not> drunk x" by (rule de_Morgan)
    1.15 -  then obtain a where a: "\<not> drunk a" ..
    1.16 +  then obtain a where "\<not> drunk a" ..
    1.17    have "drunk a \<longrightarrow> (\<forall>x. drunk x)"
    1.18    proof
    1.19      assume "drunk a"
    1.20 -    with a show "\<forall>x. drunk x" by contradiction
    1.21 +    with \<open>\<not> drunk a\<close> show "\<forall>x. drunk x" by contradiction
    1.22    qed
    1.23    then show ?thesis ..
    1.24  qed