src/HOL/Nat_Transfer.thy
changeset 39198 f967a16dfcdd
parent 35821 ee34f03a7d26
child 39302 d7728f65b353
     1.1 --- a/src/HOL/Nat_Transfer.thy	Mon Sep 06 22:58:06 2010 +0200
     1.2 +++ b/src/HOL/Nat_Transfer.thy	Tue Sep 07 10:05:19 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 expand_set_eq inj_on_def)
     1.8 +  apply (auto simp add: image_def set_ext_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)