adapted to listsum -> sum_list
authornipkow
Thu, 15 Sep 2016 19:31:17 +0200
changeset 63884 d588f684ccaf
parent 63883 41b5d9f3778a
child 63885 a6cd18af8bf9
adapted to listsum -> sum_list
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}\\