# HG changeset patch
# User nipkow
# Date 1709576056 -3600
# Node ID feec445a82c3470ded0c63db3dd9b336c3910de2
# Parent  a478fc5cd5bde9f746558fc69f37830f9656d144
tuned

diff -r a478fc5cd5bd -r feec445a82c3 src/Doc/Main/Main_Doc.thy
--- 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>\\
diff -r a478fc5cd5bd -r feec445a82c3 src/Doc/Prog_Prove/document/intro-isabelle.tex
--- 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}