equal
deleted
inserted
replaced
1 (* Title: HOL/Isar_examples/Drinker.thy |
1 (* Title: HOL/Isar_examples/Drinker.thy |
2 ID: $Id$ |
|
3 Author: Makarius |
2 Author: Makarius |
4 *) |
3 *) |
5 |
4 |
6 header {* The Drinker's Principle *} |
5 header {* The Drinker's Principle *} |
7 |
6 |
8 theory Drinker imports Main begin |
7 theory Drinker |
|
8 imports Main |
|
9 begin |
9 |
10 |
10 text {* |
11 text {* |
11 Here is another example of classical reasoning: the Drinker's |
12 Here is another example of classical reasoning: the Drinker's |
12 Principle says that for some person, if he is drunk, everybody else |
13 Principle says that for some person, if he is drunk, everybody else |
13 is drunk! |
14 is drunk! |