diff -r 5eb932e604a2 -r eab6ce8368fa src/Doc/Isar_Ref/HOL_Specific.thy
--- a/src/Doc/Isar_Ref/HOL_Specific.thy	Wed Jan 10 15:21:49 2018 +0100
+++ b/src/Doc/Isar_Ref/HOL_Specific.thy	Wed Jan 10 15:25:09 2018 +0100
@@ -1452,7 +1452,7 @@
   \<open>Quotient_thm\<close>). Optional theorems \<open>pcr_def\<close> and \<open>pcr_cr_eq_thm\<close> can be
   specified to register the parametrized correspondence relation for \<open>\<tau>\<close>.
   E.g.\ for @{typ "'a dlist"}, \<open>pcr_def\<close> is \<open>pcr_dlist A \<equiv> list_all2 A \<circ>\<circ>
-  cr_dlist\<close> and \<open>pcr_cr_eq_thm\<close> is \<open>pcr_dlist (op =) = (op =)\<close>. This attribute
+  cr_dlist\<close> and \<open>pcr_cr_eq_thm\<close> is \<open>pcr_dlist (=) = (=)\<close>. This attribute
   is rather used for low-level manipulation with set-up of the Lifting package
   because using of the bundle \<open>\<tau>.lifting\<close> together with the commands @{command
   (HOL) lifting_forget} and @{command (HOL) lifting_update} is preferred for
@@ -1539,7 +1539,7 @@
   Lemmas involving predicates on relations can also be registered using the
   same attribute. For example:
 
-    \<open>bi_unique A \<Longrightarrow> (list_all2 A ===> op =) distinct distinct\<close> \\
+    \<open>bi_unique A \<Longrightarrow> (list_all2 A ===> (=)) distinct distinct\<close> \\
     \<open>\<lbrakk>bi_unique A; bi_unique B\<rbrakk> \<Longrightarrow> bi_unique (rel_prod A B)\<close>
 
   Preservation of predicates on relations (\<open>bi_unique, bi_total, right_unique,
@@ -1555,7 +1555,7 @@
   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 =)"}.
+  relators of various type constructors, e.g. @{term "rel_set (=) = (=)"}.
   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
@@ -1894,7 +1894,7 @@
     @{term "Quickcheck_Narrowing.sum (Quickcheck_Narrowing.cons [])
               (Quickcheck_Narrowing.apply
                 (Quickcheck_Narrowing.apply
-                  (Quickcheck_Narrowing.cons (op #))
+                  (Quickcheck_Narrowing.cons (#))
                   narrowing)
                 narrowing)"}.
     If a symbolic variable of type @{typ "_ list"} is evaluated, it is
@@ -1909,7 +1909,7 @@
     "Quickcheck_Narrowing.Narrowing_constructor i args"}, where @{term "i ::
     integer"} denotes the index in the sum of refinements. In the above
     example for lists, @{term "0"} corresponds to @{term "[]"} and @{term "1"}
-    to @{term "op #"}.
+    to @{term "(#)"}.
 
     The command @{command (HOL) "code_datatype"} sets up @{const
     partial_term_of} such that the @{term "i"}-th refinement is interpreted as