--- a/src/Doc/Main/Main_Doc.thy Mon Mar 04 16:20:57 2024 +0100
+++ b/src/Doc/Main/Main_Doc.thy Mon Mar 04 19:14:16 2024 +0100
@@ -538,14 +538,13 @@
\<^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>\\
@@ -559,6 +558,7 @@
\<^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>\\
--- a/src/Doc/Prog_Prove/document/intro-isabelle.tex Mon Mar 04 16:20:57 2024 +0100
+++ b/src/Doc/Prog_Prove/document/intro-isabelle.tex Mon Mar 04 19:14:16 2024 +0100
@@ -84,7 +84,7 @@
download and read the book
\href{http://www.concrete-semantics.org}{Concrete
Semantics}~\cite{ConcreteSemantics}, a guided tour of the wonderful world of
-programming langage semantics formalised in Isabelle. In fact,
+programming language semantics formalized in Isabelle. In fact,
\emph{Programming and Proving in Isabelle/HOL} constitutes part~I of
\href{http://www.concrete-semantics.org}{Concrete Semantics}. The web
pages for \href{http://www.concrete-semantics.org}{Concrete Semantics}