Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/HOL.thy
changeset 18697 86b3f73e3fd5
parent 18689 a50587cd8414
child 18702 7dc7dcd63224 
--- 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)
isabelle