diff -r 6d4fb57eb66c -r a4b47c684445 src/Doc/Main/Main_Doc.thy
--- a/src/Doc/Main/Main_Doc.thy	Tue Jul 05 09:44:38 2022 +0200
+++ b/src/Doc/Main/Main_Doc.thy	Sat Jun 25 13:21:27 2022 +0200
@@ -58,8 +58,6 @@
 \<^const>\<open>Orderings.max\<close> & \<^typeof>\<open>Orderings.max\<close>\\
 @{const[source] top} & \<^typeof>\<open>Orderings.top\<close>\\
 @{const[source] bot} & \<^typeof>\<open>Orderings.bot\<close>\\
-\<^const>\<open>Orderings.mono\<close> & \<^typeof>\<open>Orderings.mono\<close>\\
-\<^const>\<open>Orderings.strict_mono\<close> & \<^typeof>\<open>Orderings.strict_mono\<close>\\
 \end{tabular}
 
 \subsubsection*{Syntax}
@@ -152,6 +150,12 @@
 \<^const>\<open>Fun.surj\<close> & \<^typeof>\<open>Fun.surj\<close>\\
 \<^const>\<open>Fun.bij\<close> & \<^typeof>\<open>Fun.bij\<close>\\
 \<^const>\<open>Fun.bij_betw\<close> & @{term_type_only Fun.bij_betw "('a\<Rightarrow>'b)\<Rightarrow>'a set\<Rightarrow>'b set\<Rightarrow>bool"}\\
+\<^const>\<open>Fun.monotone_on\<close> & \<^typeof>\<open>Fun.monotone_on\<close>\\
+\<^const>\<open>Fun.monotone\<close> & \<^typeof>\<open>Fun.monotone\<close>\\
+\<^const>\<open>Fun.mono_on\<close> & \<^typeof>\<open>Fun.mono_on\<close>\\
+\<^const>\<open>Fun.mono\<close> & \<^typeof>\<open>Fun.mono\<close>\\
+\<^const>\<open>Fun.strict_mono_on\<close> & \<^typeof>\<open>Fun.strict_mono_on\<close>\\
+\<^const>\<open>Fun.strict_mono\<close> & \<^typeof>\<open>Fun.strict_mono\<close>\\
 \<^const>\<open>Fun.fun_upd\<close> & \<^typeof>\<open>Fun.fun_upd\<close>\\
 \end{tabular}