--- 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)"