equal
deleted
inserted
replaced
7 theory Drinker |
7 theory Drinker |
8 imports Main |
8 imports Main |
9 begin |
9 begin |
10 |
10 |
11 text \<open>Here is another example of classical reasoning: the Drinker's |
11 text \<open>Here is another example of classical reasoning: the Drinker's |
12 Principle says that for some person, if he is drunk, everybody else |
12 Principle says that for some person, if he is drunk, everybody else is |
13 is drunk! |
13 drunk! |
14 |
14 |
15 We first prove a classical part of de-Morgan's law.\<close> |
15 We first prove a classical part of de-Morgan's law.\<close> |
16 |
16 |
17 lemma de_Morgan: |
17 lemma de_Morgan: |
18 assumes "\<not> (\<forall>x. P x)" |
18 assumes "\<not> (\<forall>x. P x)" |