diff -r 0ce594837524 -r fa53d267dab3 src/HOL/Isar_Examples/Drinker.thy
--- a/src/HOL/Isar_Examples/Drinker.thy	Thu Jul 01 14:32:57 2010 +0200
+++ b/src/HOL/Isar_Examples/Drinker.thy	Thu Jul 01 18:31:46 2010 +0200
@@ -8,24 +8,21 @@
 imports Main
 begin
 
-text {*
-  Here is another example of classical reasoning: the Drinker's
+text {* Here is another example of classical reasoning: the Drinker's
   Principle says that for some person, if he is drunk, everybody else
   is drunk!
 
-  We first prove a classical part of de-Morgan's law.
-*}
+  We first prove a classical part of de-Morgan's law. *}
 
-lemma deMorgan:
+lemma de_Morgan:
   assumes "\<not> (\<forall>x. P x)"
   shows "\<exists>x. \<not> P x"
-  using prems
+  using assms
 proof (rule contrapos_np)
   assume a: "\<not> (\<exists>x. \<not> P x)"
   show "\<forall>x. P x"
   proof
-    fix x
-    show "P x"
+    fix x show "P x"
     proof (rule classical)
       assume "\<not> P x"
       then have "\<exists>x. \<not> P x" ..
@@ -41,12 +38,12 @@
   then show ?thesis ..
 next
   assume "\<not> (\<forall>x. drunk x)"
-  then have "\<exists>x. \<not> drunk x" by (rule deMorgan)
+  then have "\<exists>x. \<not> drunk x" by (rule de_Morgan)
   then obtain a where a: "\<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 a show "\<forall>x. drunk x" by contradiction
   qed
   then show ?thesis ..
 qed