src/HOL/Lifting_Set.thy
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"