# HG changeset patch
# User wenzelm
# Date 1137444914 -3600
# Node ID 86b3f73e3fd552f174a833f07804a6528aa1761b
# Parent  60ca2c74978234a87228b2c93cf159a98a0b3a40
declare the1_equality [elim?];

diff -r 60ca2c749782 -r 86b3f73e3fd5 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Sun Jan 15 20:04:05 2006 +0100
+++ b/src/HOL/HOL.thy	Mon Jan 16 21:55:14 2006 +0100
@@ -606,7 +606,7 @@
   shows "Q (THE x. P x)"
 by (iprover intro: prems theI)
 
-lemma the1_equality: "[| EX!x. P x; P a |] ==> (THE x. P x) = a"
+lemma the1_equality [elim?]: "[| EX!x. P x; P a |] ==> (THE x. P x) = a"
 apply (rule the_equality)
 apply  assumption
 apply (erule ex1E)