# HG changeset patch
# User wenzelm
# Date 1437569742 -7200
# Node ID 76560ce8dead6f741fce0efdb1f2b4118ac8e285
# Parent  e43e71a75838644b369d80909762b33226c6341d
tuned proofs;

diff -r e43e71a75838 -r 76560ce8dead src/HOL/Isar_Examples/Drinker.thy
--- a/src/HOL/Isar_Examples/Drinker.thy	Tue Jul 21 19:04:36 2015 +0200
+++ b/src/HOL/Isar_Examples/Drinker.thy	Wed Jul 22 14:55:42 2015 +0200
@@ -33,17 +33,17 @@
 
 theorem Drinker's_Principle: "\<exists>x. drunk x \<longrightarrow> (\<forall>x. drunk x)"
 proof cases
-  fix a assume "\<forall>x. drunk x"
-  then have "drunk a \<longrightarrow> (\<forall>x. drunk x)" ..
+  assume "\<forall>x. drunk x"
+  then have "drunk a \<longrightarrow> (\<forall>x. drunk x)" for a ..
   then show ?thesis ..
 next
   assume "\<not> (\<forall>x. drunk x)"
   then have "\<exists>x. \<not> drunk x" by (rule de_Morgan)
-  then obtain a where a: "\<not> drunk a" ..
+  then obtain a where "\<not> drunk a" ..
   have "drunk a \<longrightarrow> (\<forall>x. drunk x)"
   proof
     assume "drunk a"
-    with a show "\<forall>x. drunk x" by contradiction
+    with \<open>\<not> drunk a\<close> show "\<forall>x. drunk x" by contradiction
   qed
   then show ?thesis ..
 qed