# HG changeset patch
# User kuncar
# Date 1358170433 -3600
# Node ID fc394c83e490f89b6ae94a9b20ea3d32a59686d8
# Parent  2840522a936dd257dac52213ebef024f6c799b7e
more update on Lifting in isar-ref

diff -r 2840522a936d -r fc394c83e490 src/Doc/IsarRef/HOL_Specific.thy
--- a/src/Doc/IsarRef/HOL_Specific.thy	Mon Jan 14 14:03:24 2013 +0100
+++ b/src/Doc/IsarRef/HOL_Specific.thy	Mon Jan 14 14:33:53 2013 +0100
@@ -1570,10 +1570,21 @@
     @{text f.tranfer} for the Transfer package are generated by the
     package.
 
-    Integration with code_abstype: For typedefs (e.g. subtypes
+    For each constant defined through trivial quotients (type copies or
+    subtypes) @{text f.rep_eq} is generated. The equation is a code certificate
+    that defines @{text f} using the representation function.
+
+    For each constant @{text f.abs_eq} is generated. The equation is unconditional
+    for total quotients. The equation defines @{text f} using
+    the abstraction function.
+
+    Integration with code_abstype: For subtypes (e.g.,
     corresponding to a datatype invariant, such as dlist), @{command
-    (HOL) "lift_definition"} generates a code certificate theorem
-    @{text f.rep_eq} and sets up code generation for each constant.
+    (HOL) "lift_definition"} uses a code certificate theorem
+    @{text f.rep_eq} as a code equation.
+
+    Integration with code: For total quotients, @{command
+    (HOL) "lift_definition"} uses @{text f.abs_eq} as a code equation.
 
   \item @{command (HOL) "print_quotmaps"} prints stored quotient map
     theorems.