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