author wenzelm Wed Jul 22 14:55:42 2015 +0200 (2015-07-22) changeset 60766 76560ce8dead parent 60765 e43e71a75838 child 60767 ad5b4771fc19
tuned proofs;
```     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
```