# HG changeset patch
# User traytel
# Date 1635933756 -3600
# Node ID 432b3605933d055ddff0011882fadc195e052bcc
# Parent  d4a812e4f041f89d76e3c052af0984d90a50cf82
add documentation for pred_mono

diff -r d4a812e4f041 -r 432b3605933d src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Wed Nov 03 10:44:54 2021 +0100
+++ b/src/Doc/Datatypes/Datatypes.thy	Wed Nov 03 11:02:36 2021 +0100
@@ -996,6 +996,9 @@
 \item[\<open>t.\<close>\hthm{pred_map}\rm:] ~ \\
 @{thm list.pred_map[no_vars]}
 
+\item[\<open>t.\<close>\hthm{pred_mono} \<open>[mono]\<close>\rm:] ~ \\
+@{thm list.pred_mono[no_vars]}
+
 \item[\<open>t.\<close>\hthm{pred_mono_strong}\rm:] ~ \\
 @{thm list.pred_mono_strong[no_vars]}