src/Doc/Main/Main_Doc.thy

 \<^const>\<open>List.lexord\<close> & @{term_type_only List.lexord "('a*'a)set\<Rightarrow>('a list * 'a list)set"}\\
 \<^const>\<open>List.listrel\<close> & @{term_type_only List.listrel "('a*'b)set\<Rightarrow>('a list * 'b list)set"}\\
 \<^const>\<open>List.listrel1\<close> & @{term_type_only List.listrel1 "('a*'a)set\<Rightarrow>('a list * 'a list)set"}\\
 \<^const>\<open>List.lists\<close> & @{term_type_only List.lists "'a set\<Rightarrow>'a list set"}\\
 \<^const>\<open>List.listset\<close> & @{term_type_only List.listset "'a set list \<Rightarrow> 'a list set"}\\
-\<^const>\<open>Groups_List.sum_list\<close> & \<^typeof>\<open>Groups_List.sum_list\<close>\\
-\<^const>\<open>Groups_List.prod_list\<close> & \<^typeof>\<open>Groups_List.prod_list\<close>\\
 \<^const>\<open>List.list_all2\<close> & \<^typeof>\<open>List.list_all2\<close>\\
 \<^const>\<open>List.list_update\<close> & \<^typeof>\<open>List.list_update\<close>\\
 \<^const>\<open>List.map\<close> & \<^typeof>\<open>List.map\<close>\\
 \<^const>\<open>List.measures\<close> & @{term_type_only List.measures "('a\<Rightarrow>nat)list\<Rightarrow>('a*'a)set"}\\
 \<^const>\<open>List.nth\<close> & \<^typeof>\<open>List.nth\<close>\\
 \<^const>\<open>List.nths\<close> & \<^typeof>\<open>List.nths\<close>\\
+\<^const>\<open>Groups_List.prod_list\<close> & \<^typeof>\<open>Groups_List.prod_list\<close>\\
 \<^const>\<open>List.remdups\<close> & \<^typeof>\<open>List.remdups\<close>\\
 \<^const>\<open>List.removeAll\<close> & \<^typeof>\<open>List.removeAll\<close>\\
 \<^const>\<open>List.remove1\<close> & \<^typeof>\<open>List.remove1\<close>\\
 \<^const>\<open>List.replicate\<close> & \<^typeof>\<open>List.replicate\<close>\\
 \<^const>\<open>List.rev\<close> & \<^typeof>\<open>List.rev\<close>\\

 \<^const>\<open>List.shuffles\<close> & \<^typeof>\<open>List.shuffles\<close>\\
 \<^const>\<open>List.sort\<close> & \<^typeof>\<open>List.sort\<close>\\
 \<^const>\<open>List.sorted\<close> & \<^typeof>\<open>List.sorted\<close>\\
 \<^const>\<open>List.sorted_wrt\<close> & \<^typeof>\<open>List.sorted_wrt\<close>\\
 \<^const>\<open>List.splice\<close> & \<^typeof>\<open>List.splice\<close>\\
+\<^const>\<open>Groups_List.sum_list\<close> & \<^typeof>\<open>Groups_List.sum_list\<close>\\
 \<^const>\<open>List.take\<close> & \<^typeof>\<open>List.take\<close>\\
 \<^const>\<open>List.takeWhile\<close> & \<^typeof>\<open>List.takeWhile\<close>\\
 \<^const>\<open>List.tl\<close> & \<^typeof>\<open>List.tl\<close>\\
 \<^const>\<open>List.upt\<close> & \<^typeof>\<open>List.upt\<close>\\
 \<^const>\<open>List.upto\<close> & \<^typeof>\<open>List.upto\<close>\\