# HG changeset patch
# User wenzelm
# Date 1436211412 -7200
# Node ID 7109b66ba151d9daae401ff5956a03ddd65f779b
# Parent  92fd47ae2a67c67e544edda046a6a321dba141bd
tuned;

diff -r 92fd47ae2a67 -r 7109b66ba151 src/Doc/Isar_Ref/HOL_Specific.thy
--- a/src/Doc/Isar_Ref/HOL_Specific.thy	Mon Jul 06 21:20:28 2015 +0200
+++ b/src/Doc/Isar_Ref/HOL_Specific.thy	Mon Jul 06 21:36:52 2015 +0200
@@ -1387,28 +1387,33 @@
   \begin{description}
 
   \item @{command (HOL) "setup_lifting"} Sets up the Lifting package to work
-  with a user-defined type. The command supports two modes. The first one is
-  a low-level mode when the user must provide as a first argument of
-  @{command (HOL) "setup_lifting"} a quotient theorem @{term "Quotient R Abs
-  Rep T"}. The package configures a transfer rule for equality, a domain
-  transfer rules and sets up the @{command_def (HOL) "lift_definition"}
-  command to work with the abstract type. An optional theorem @{term "reflp
-  R"}, which certifies that the equivalence relation R is total, can be
-  provided as a second argument. This allows the package to generate
-  stronger transfer rules. And finally, the parametricity theorem for @{term
-  R} can be provided as a third argument. This allows the package to
-  generate a stronger transfer rule for equality.
+  with a user-defined type. The command supports two modes.
+
+  \begin{enumerate}
+
+  \item The first one is a low-level mode when the user must provide as a
+  first argument of @{command (HOL) "setup_lifting"} a quotient theorem
+  @{term "Quotient R Abs Rep T"}. The package configures a transfer rule for
+  equality, a domain transfer rules and sets up the @{command_def (HOL)
+  "lift_definition"} command to work with the abstract type. An optional
+  theorem @{term "reflp R"}, which certifies that the equivalence relation R
+  is total, can be provided as a second argument. This allows the package to
+  generate stronger transfer rules. And finally, the parametricity theorem
+  for @{term R} can be provided as a third argument. This allows the package
+  to generate a stronger transfer rule for equality.
 
   Users generally will not prove the @{text Quotient} theorem manually for
   new types, as special commands exist to automate the process.
 
-  \medskip When a new subtype is defined by @{command (HOL) typedef},
-  @{command (HOL) "lift_definition"} can be used in its second mode, where
-  only the @{term type_definition} theorem @{term "type_definition Rep Abs
-  A"} is used as an argument of the command. The command internally proves
-  the corresponding @{term Quotient} theorem and registers it with @{command
+  \item When a new subtype is defined by @{command (HOL) typedef}, @{command
+  (HOL) "lift_definition"} can be used in its second mode, where only the
+  @{term type_definition} theorem @{term "type_definition Rep Abs A"} is
+  used as an argument of the command. The command internally proves the
+  corresponding @{term Quotient} theorem and registers it with @{command
   (HOL) setup_lifting} using its first mode.
 
+  \end{enumerate}
+
   For quotients, the command @{command (HOL) quotient_type} can be used. The
   command defines a new quotient type and similarly to the previous case,
   the corresponding Quotient theorem is proved and registered by @{command