src/HOL/UNITY/Extend.thy
changeset 61424 c3658c18b7bc
parent 58889 5b7a9633cfa8
child 61941 31f2105521ee
     1.1 --- a/src/HOL/UNITY/Extend.thy	Tue Oct 13 09:21:14 2015 +0200
     1.2 +++ b/src/HOL/UNITY/Extend.thy	Tue Oct 13 09:21:15 2015 +0200
     1.3 @@ -127,7 +127,7 @@
     1.4       assumes surj_h: "surj h"
     1.5           and prem:   "!! x y. g (h(x,y)) = x"
     1.6       shows "fst (inv h z) = g z"
     1.7 -by (metis UNIV_I f_inv_into_f pair_collapse prem surj_h)
     1.8 +by (metis UNIV_I f_inv_into_f prod.collapse prem surj_h)
     1.9  
    1.10  
    1.11  subsection{*Trivial properties of f, g, h*}