src/HOL/Lifting_Set.thy
changeset 64267 b9a1486e79be
parent 63343 fb5d8a50c641
child 64272 f76b6dda2e56
     1.1 --- a/src/HOL/Lifting_Set.thy	Sun Oct 16 22:43:51 2016 +0200
     1.2 +++ b/src/HOL/Lifting_Set.thy	Mon Oct 17 11:46:22 2016 +0200
     1.3 @@ -285,7 +285,7 @@
     1.4      by (simp add: reindex_bij_betw)
     1.5  qed
     1.6  
     1.7 -lemmas setsum_parametric = setsum.F_parametric
     1.8 +lemmas sum_parametric = sum.F_parametric
     1.9  lemmas setprod_parametric = setprod.F_parametric
    1.10  
    1.11  lemma rel_set_UNION: