src/HOL/Groups_List.thy
changeset 63343 fb5d8a50c641
parent 63317 ca187a9f66da
child 63882 018998c00003
     1.1 --- a/src/HOL/Groups_List.thy	Tue Jun 21 17:35:45 2016 +0200
     1.2 +++ b/src/HOL/Groups_List.thy	Wed Jun 22 10:09:20 2016 +0200
     1.3 @@ -308,20 +308,14 @@
     1.4    "setsum f (set [m..<n]) = listsum (map f [m..<n])"
     1.5    by (simp add: interv_listsum_conv_setsum_set_nat)
     1.6  
     1.7 -context
     1.8 -begin
     1.9 -
    1.10 -interpretation lifting_syntax .
    1.11 -
    1.12  lemma listsum_transfer[transfer_rule]:
    1.13 +  includes lifting_syntax
    1.14    assumes [transfer_rule]: "A 0 0"
    1.15    assumes [transfer_rule]: "(A ===> A ===> A) op + op +"
    1.16    shows "(list_all2 A ===> A) listsum listsum"
    1.17    unfolding listsum.eq_foldr [abs_def]
    1.18    by transfer_prover
    1.19  
    1.20 -end
    1.21 -
    1.22  
    1.23  subsection \<open>List product\<close>
    1.24