src/HOL/Fun.thy
changeset 44928 7ef6505bde7f
parent 44921 58eef4843641
child 45174 10c3597f92f0
     1.1 --- a/src/HOL/Fun.thy	Wed Sep 14 10:55:07 2011 +0200
     1.2 +++ b/src/HOL/Fun.thy	Wed Sep 14 10:08:52 2011 -0400
     1.3 @@ -181,7 +181,7 @@
     1.4    assumes CH: "\<And> i j. \<lbrakk>i \<in> I; j \<in> I\<rbrakk> \<Longrightarrow> A i \<le> A j \<or> A j \<le> A i" and
     1.5           INJ: "\<And> i. i \<in> I \<Longrightarrow> inj_on f (A i)"
     1.6    shows "inj_on f (\<Union> i \<in> I. A i)"
     1.7 -proof(unfold inj_on_def UNION_def, auto)
     1.8 +proof(unfold inj_on_def UNION_eq, auto)
     1.9    fix i j x y
    1.10    assume *: "i \<in> I" "j \<in> I" and **: "x \<in> A i" "y \<in> A j"
    1.11           and ***: "f x = f y"