diff -r ed47044ee6a6 -r 2e48182cc82c src/HOL/Isar_Examples/Drinker.thy
--- a/src/HOL/Isar_Examples/Drinker.thy	Sat Dec 26 15:03:41 2015 +0100
+++ b/src/HOL/Isar_Examples/Drinker.thy	Sat Dec 26 15:44:14 2015 +0100
@@ -8,11 +8,12 @@
 imports Main
 begin
 
-text \<open>Here is another example of classical reasoning: the Drinker's
-  Principle says that for some person, if he is drunk, everybody else is
-  drunk!
+text \<open>
+  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.\<close>
+  We first prove a classical part of de-Morgan's law.
+\<close>
 
 lemma de_Morgan:
   assumes "\<not> (\<forall>x. P x)"