Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
declare the1_equality [elim?];
authorwenzelm
Mon, 16 Jan 2006 21:55:14 +0100
changeset 18697 86b3f73e3fd5
parent 18696 60ca2c749782
child 18698 a95c2adc8900
declare the1_equality [elim?];
src/HOL/HOL.thy file | annotate | diff | comparison | revisions 
--- 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