# HG changeset patch
# User wenzelm
# Date 1436205917 -7200
# Node ID ac02ff182f46822c75cd28d6c0e6a432bd27a535
# Parent  294ba3f479135a888a7d3c8de212701105efc2d5
tuned;

diff -r 294ba3f47913 -r ac02ff182f46 src/Doc/Isar_Ref/HOL_Specific.thy
--- a/src/Doc/Isar_Ref/HOL_Specific.thy	Mon Jul 06 20:00:42 2015 +0200
+++ b/src/Doc/Isar_Ref/HOL_Specific.thy	Mon Jul 06 20:05:17 2015 +0200
@@ -1506,7 +1506,7 @@
   \item @{command (HOL) "print_quotients"} prints stored quotient theorems.
 
   \item @{attribute (HOL) quot_map} registers a quotient map theorem, a
-  theorem showing how to "lift" quotients over type constructors. E.g.\
+  theorem showing how to ``lift'' quotients over type constructors. E.g.\
   @{term "Quotient R Abs Rep T \<Longrightarrow> Quotient (rel_set R) (image Abs) (image
   Rep) (rel_set T)"}. For examples see @{file "~~/src/HOL/Lifting_Set.thy"}
   or @{file "~~/src/HOL/Lifting.thy"}. This property is proved automatically
@@ -1559,11 +1559,11 @@
   @{text pcr_def} and @{text pcr_cr_eq_thm} can be specified to register the
   parametrized correspondence relation for @{text \<tau>}. E.g.\ for @{typ "'a
   dlist"}, @{text pcr_def} is @{text "pcr_dlist A \<equiv> list_all2 A \<circ>\<circ>
-  cr_dlist"} and @{text pcr_cr_eq_thm} is @{text "pcr_dlist op= = op="}.
-  This attribute is rather used for low-level manipulation with set-up of
-  the Lifting package because using of the bundle @{text \<tau>.lifting} together
-  with the commands @{command (HOL) lifting_forget} and @{command (HOL)
-  lifting_update} is preferred for normal usage.
+  cr_dlist"} and @{text pcr_cr_eq_thm} is @{text "pcr_dlist (op =) = (op
+  =)"}. This attribute is rather used for low-level manipulation with set-up
+  of the Lifting package because using of the bundle @{text \<tau>.lifting}
+  together with the commands @{command (HOL) lifting_forget} and @{command
+  (HOL) lifting_update} is preferred for normal usage.
 
   \item Integration with the BNF package @{cite "isabelle-datatypes"}: As
   already mentioned, the theorems that are registered by the following