src/HOL/Wellfounded.thy
changeset 40607 30d512bf47a7
parent 39302 d7728f65b353
child 41075 4bed56dc95fb
     1.1 --- a/src/HOL/Wellfounded.thy	Thu Nov 18 17:01:16 2010 +0100
     1.2 +++ b/src/HOL/Wellfounded.thy	Thu Nov 18 17:01:16 2010 +0100
     1.3 @@ -240,7 +240,7 @@
     1.4  
     1.5  text{*Well-foundedness of image*}
     1.6  
     1.7 -lemma wf_prod_fun_image: "[| wf r; inj f |] ==> wf(prod_fun f f ` r)"
     1.8 +lemma wf_map_pair_image: "[| wf r; inj f |] ==> wf(map_pair 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)