diff -r 74e8f703f5f2 -r cf6ad8d22793 src/HOL/Isar_examples/Peirce.thy
--- a/src/HOL/Isar_examples/Peirce.thy	Fri May 28 11:42:07 1999 +0200
+++ b/src/HOL/Isar_examples/Peirce.thy	Fri May 28 13:30:59 1999 +0200
@@ -1,12 +1,11 @@
 (*  Title:      HOL/Isar_examples/Peirce.thy
     ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
-
-Peirce's law: examples of classical proof.
 *)
 
 theory Peirce = Main:;
 
+text {* Peirce's law: examples of classical proof. *};
 
 theorem "((A --> B) --> A) --> A";
 proof;