changeset 64272 | f76b6dda2e56 |
parent 64267 | b9a1486e79be |
child 67399 | eab6ce8368fa |
--- a/src/HOL/Lifting_Set.thy Mon Oct 17 14:37:32 2016 +0200 +++ b/src/HOL/Lifting_Set.thy Mon Oct 17 17:33:07 2016 +0200 @@ -286,7 +286,7 @@ qed lemmas sum_parametric = sum.F_parametric -lemmas setprod_parametric = setprod.F_parametric +lemmas prod_parametric = prod.F_parametric lemma rel_set_UNION: assumes [transfer_rule]: "rel_set Q A B" "rel_fun Q (rel_set R) f g"