# 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: