--- a/src/Doc/Datatypes/Datatypes.thy Fri Jan 17 18:58:58 2020 +0100
+++ b/src/Doc/Datatypes/Datatypes.thy Sun Jan 19 07:50:35 2020 +0100
@@ -2996,7 +2996,9 @@
text \<open>The @{command lift_bnf} command also supports quotient types. Here is an example
that defines the option type as a quotient of the sum type. The proof obligations
-generated by @{command lift_bnf} for quotients are different from the ones for typedefs.\<close>
+generated by @{command lift_bnf} for quotients are different from the ones for typedefs.
+You can find additional examples of usages of @{command lift_bnf} for both quotients and subtypes
+in the session \emph{HOL-Datatype_Examples}.\<close>
inductive ignore_Inl :: "'a + 'a \<Rightarrow> 'a + 'a \<Rightarrow> bool" where
"ignore_Inl (Inl x) (Inl y)"