# HG changeset patch
# User nipkow
# Date 1515256772 -3600
# Node ID 4c4db8687e50a8a74c8a4c7bc6b40ccbb8dc6d7f
# Parent  bf269672c203a78df602b4a4331759e3466d0d29
tuned op

diff -r bf269672c203 -r 4c4db8687e50 src/Doc/Isar_Ref/HOL_Specific.thy
--- a/src/Doc/Isar_Ref/HOL_Specific.thy	Sat Jan 06 17:34:41 2018 +0100
+++ b/src/Doc/Isar_Ref/HOL_Specific.thy	Sat Jan 06 17:39:32 2018 +0100
@@ -1555,8 +1555,8 @@
   quantifiers are transferred.
 
   \<^descr> @{attribute (HOL) relator_eq} attribute collects identity laws for
-  relators of various type constructors, e.g. @{term "rel_set (op =) = (op
-  =)"}. The @{method (HOL) transfer} method uses these lemmas to infer
+  relators of various type constructors, e.g. @{term "rel_set (op =) = (op =)"}.
+  The @{method (HOL) transfer} method uses these lemmas to infer
   transfer rules for non-polymorphic constants on the fly. For examples see
   \<^file>\<open>~~/src/HOL/Lifting_Set.thy\<close> or \<^file>\<open>~~/src/HOL/Lifting.thy\<close>. This property
   is proved automatically if the involved type is BNF without dead variables.