# HG changeset patch # User blanchet # Date 1426521719 -3600 # Node ID 5fc2870bd23673486a528dcf95ea1d03b50a2622 # Parent f893472fff31ee1a3bcef3df697b33849fb6fe2e clarified documentation diff -r f893472fff31 -r 5fc2870bd236 src/Doc/Datatypes/Datatypes.thy --- a/src/Doc/Datatypes/Datatypes.thy Mon Mar 16 16:59:59 2015 +0100 +++ b/src/Doc/Datatypes/Datatypes.thy Mon Mar 16 17:01:59 2015 +0100 @@ -3115,9 +3115,9 @@ \label{ssec:lifting} *} text {* -For each (co)datatype with live type arguments and each manually registered BNF, -the \hthm{lifting} plugin generates properties and attributes that guide the -Lifting tool. +For each (co)datatype and each manually registered BNF with at least one live +type argument and no dead type arguments, the \hthm{lifting} plugin generates +properties and attributes that guide the Lifting tool. The plugin derives the following property: