# HG changeset patch
# User nipkow
# Date 1473960677 -7200
# Node ID d588f684ccaf1e5a93175b31cd8e5b11f3644419
# Parent  41b5d9f3778a6ca0ddb1560f7001e0a424ab6c02
adapted to listsum -> sum_list

diff -r 41b5d9f3778a -r d588f684ccaf src/Doc/Main/Main_Doc.thy
--- a/src/Doc/Main/Main_Doc.thy	Thu Sep 15 17:05:34 2016 +0200
+++ b/src/Doc/Main/Main_Doc.thy	Thu Sep 15 19:31:17 2016 +0200
@@ -516,7 +516,8 @@
 @{const List.listrel1} & @{term_type_only List.listrel1 "('a*'a)set\<Rightarrow>('a list * 'a list)set"}\\
 @{const List.lists} & @{term_type_only List.lists "'a set\<Rightarrow>'a list set"}\\
 @{const List.listset} & @{term_type_only List.listset "'a set list \<Rightarrow> 'a list set"}\\
-@{const Groups_List.listsum} & @{typeof Groups_List.listsum}\\
+@{const Groups_List.sum_list} & @{typeof Groups_List.sum_list}\\
+@{const Groups_List.prod_list} & @{typeof Groups_List.prod_list}\\
 @{const List.list_all2} & @{typeof List.list_all2}\\
 @{const List.list_update} & @{typeof List.list_update}\\
 @{const List.map} & @{typeof List.map}\\