src/HOL/HOL.thy
changeset 44921 58eef4843641
parent 44277 bcb696533579
child 45014 0e847655b2d8
     1.1 --- a/src/HOL/HOL.thy	Tue Sep 13 08:21:51 2011 -0700
     1.2 +++ b/src/HOL/HOL.thy	Tue Sep 13 17:07:33 2011 -0700
     1.3 @@ -1635,7 +1635,7 @@
     1.4    apply (rule iffI)
     1.5    apply (rule_tac a = "%x. THE y. P x y" in ex1I)
     1.6    apply (fast dest!: theI')
     1.7 -  apply (fast intro: ext the1_equality [symmetric])
     1.8 +  apply (fast intro: the1_equality [symmetric])
     1.9    apply (erule ex1E)
    1.10    apply (rule allI)
    1.11    apply (rule ex1I)