# HG changeset patch
# User wenzelm
# Date 924861017 -7200
# Node ID 3489490c948d069383beb2d6d6d725bab0f5d038
# Parent  937eb94b2aab8499e370ce92d623e8a13d964797
tuned;

diff -r 937eb94b2aab -r 3489490c948d src/HOL/Isar_examples/Peirce.thy
--- a/src/HOL/Isar_examples/Peirce.thy	Fri Apr 23 11:48:37 1999 +0200
+++ b/src/HOL/Isar_examples/Peirce.thy	Fri Apr 23 11:50:17 1999 +0200
@@ -2,15 +2,13 @@
     ID:         $Id$
     Author:     Markus Wenzel, TU Muenchen
 
-Peirce's law: some examples of classical proof.
+Peirce's law: examples of classical proof.
 *)
 
 theory Peirce = Main:;
 
-lemmas it[elim!] = mp notE;	(* FIXME elim!! *)
 
-
-lemma Peirce's_law: "((A --> B) --> A) --> A";
+theorem "((A --> B) --> A) --> A";
 proof;
   assume ABA: "(A --> B) --> A";
   show A;
@@ -28,7 +26,7 @@
 qed;
 
 
-lemma Peirce's_law: "((A --> B) --> A) --> A";
+theorem "((A --> B) --> A) --> A";
 proof;
   assume ABA: "(A --> B) --> A";
   show A;