| changeset 55932 | 68c5104d2204 |
| parent 55027 | a74ea6d75571 |
| child 56166 | 9a241bc276cd |
--- a/src/HOL/Wellfounded.thy Thu Mar 06 13:36:15 2014 +0100 +++ b/src/HOL/Wellfounded.thy Thu Mar 06 13:36:48 2014 +0100 @@ -240,7 +240,7 @@ text{*Well-foundedness of image*} -lemma wf_map_pair_image: "[| wf r; inj f |] ==> wf(map_pair f f ` r)" +lemma wf_map_prod_image: "[| wf r; inj f |] ==> wf (map_prod f f ` r)" apply (simp only: wf_eq_minimal, clarify) apply (case_tac "EX p. f p : Q") apply (erule_tac x = "{p. f p : Q}" in allE)