src/HOL/Nat_Transfer.thy
changeset 39302 d7728f65b353
parent 39198 f967a16dfcdd
child 42870 36abaf4cce1f
     1.1 --- a/src/HOL/Nat_Transfer.thy	Mon Sep 13 08:43:48 2010 +0200
     1.2 +++ b/src/HOL/Nat_Transfer.thy	Mon Sep 13 11:13:15 2010 +0200
     1.3 @@ -170,7 +170,7 @@
     1.4    apply (rule iffI)
     1.5    apply (erule finite_imageI)
     1.6    apply (erule finite_imageD)
     1.7 -  apply (auto simp add: image_def set_ext_iff inj_on_def)
     1.8 +  apply (auto simp add: image_def set_eq_iff inj_on_def)
     1.9    apply (drule_tac x = "int x" in spec, auto)
    1.10    apply (drule_tac x = "int x" in spec, auto)
    1.11    apply (drule_tac x = "int x" in spec, auto)