# HG changeset patch
# User wenzelm
# Date 1436185608 -7200
# Node ID deaf10a6bdad51a98edef378cbb9c468e9226c3e
# Parent  402aafa3d9cc4cafd87a250c924cf27dc84f7db1
tuned;

diff -r 402aafa3d9cc -r deaf10a6bdad src/Doc/Isar_Ref/HOL_Specific.thy
--- a/src/Doc/Isar_Ref/HOL_Specific.thy	Mon Jul 06 11:54:53 2015 +0200
+++ b/src/Doc/Isar_Ref/HOL_Specific.thy	Mon Jul 06 14:26:48 2015 +0200
@@ -1449,9 +1449,9 @@
   The Lifting package allows users to lift terms of the raw type to the
   abstract type, which is a necessary step in building a library for an
   abstract type. Lifting defines a new constant by combining coercion
-  functions (Abs and Rep) with the raw term. It also proves an appropriate
-  transfer rule for the Transfer package and, if possible, an equation for
-  the code generator.
+  functions (@{term Abs} and @{term Rep}) with the raw term. It also proves
+  an appropriate transfer rule for the Transfer (\secref{sec:transfer})
+  package and, if possible, an equation for the code generator.
 
   The Lifting package provides two main commands: @{command (HOL)
   "setup_lifting"} for initializing the package to work with a new type, and