equal
deleted
inserted
replaced
1 (* Title: HOL/Isar_examples/Peirce.thy |
1 (* Title: HOL/Isar_examples/Peirce.thy |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Markus Wenzel, TU Muenchen |
3 Author: Markus Wenzel, TU Muenchen |
4 |
|
5 Peirce's law: examples of classical proof. |
|
6 *) |
4 *) |
7 |
5 |
8 theory Peirce = Main:; |
6 theory Peirce = Main:; |
9 |
7 |
|
8 text {* Peirce's law: examples of classical proof. *}; |
10 |
9 |
11 theorem "((A --> B) --> A) --> A"; |
10 theorem "((A --> B) --> A) --> A"; |
12 proof; |
11 proof; |
13 assume ABA: "(A --> B) --> A"; |
12 assume ABA: "(A --> B) --> A"; |
14 show A; |
13 show A; |