changeset 913 | b1f55dd64481 |
parent 867 | 9e247b9505f0 |
child 922 | a2589b4bc442 |
--- a/Quot/QuotProd.thy Thu Jan 21 12:50:43 2010 +0100 +++ b/Quot/QuotProd.thy Thu Jan 21 19:52:46 2010 +0100 @@ -46,7 +46,7 @@ assumes q1: "Quotient R1 Abs1 Rep1" assumes q2: "Quotient R2 Abs2 Rep2" shows "(Rep1 ---> Rep2 ---> (prod_fun Abs1 Abs2)) Pair = Pair" -apply(simp only: expand_fun_eq fun_map.simps pair_prs_aux[OF q1 q2]) +apply(simp only: expand_fun_eq fun_map_def pair_prs_aux[OF q1 q2]) apply(simp) done