author | traytel |
Wed, 03 Nov 2021 11:02:36 +0100 | |
changeset 74666 | 432b3605933d |
parent 74665 | d4a812e4f041 |
child 74667 | 0b3dc8c5fb32 |
--- 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]}