| changeset 7740 | 2fbe5ce9845f |
| parent 7448 | 3ee96dccdd39 |
| child 7748 | 5b9c45b21782 |
--- a/src/HOL/Isar_examples/Peirce.thy Tue Oct 05 18:16:26 1999 +0200 +++ b/src/HOL/Isar_examples/Peirce.thy Tue Oct 05 18:16:41 1999 +0200 @@ -5,7 +5,7 @@ theory Peirce = Main:; -text {* Peirce's law: examples of classical proof. *}; +section {* Examples of classical proof --- Peirce's law. *}; theorem "((A --> B) --> A) --> A"; proof;