author wenzelm Mon, 06 Jul 2015 21:36:52 +0200 changeset 60677 7109b66ba151 parent 60676 92fd47ae2a67 child 60678 17ba2df56dee
tuned;
--- 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