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