--- 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.