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 44921 58eef4843641
parent 44277 bcb696533579
child 45014 0e847655b2d8 
--- a/src/HOL/HOL.thy	Tue Sep 13 08:21:51 2011 -0700
+++ b/src/HOL/HOL.thy	Tue Sep 13 17:07:33 2011 -0700
@@ -1635,7 +1635,7 @@
   apply (rule iffI)
   apply (rule_tac a = "%x. THE y. P x y" in ex1I)
   apply (fast dest!: theI')
-  apply (fast intro: ext the1_equality [symmetric])
+  apply (fast intro: the1_equality [symmetric])
   apply (erule ex1E)
   apply (rule allI)
   apply (rule ex1I)
isabelle