diff -r 5eb932e604a2 -r eab6ce8368fa src/HOL/Lifting.thy
--- a/src/HOL/Lifting.thy	Wed Jan 10 15:21:49 2018 +0100
+++ b/src/HOL/Lifting.thy	Wed Jan 10 15:25:09 2018 +0100
@@ -78,7 +78,7 @@
   using a unfolding Quotient_def
   by blast
 
-lemma Quotient_rep_abs_eq: "R t t \<Longrightarrow> R \<le> op= \<Longrightarrow> Rep (Abs t) = t"
+lemma Quotient_rep_abs_eq: "R t t \<Longrightarrow> R \<le> (=) \<Longrightarrow> Rep (Abs t) = t"
   using a unfolding Quotient_def
   by blast
 
@@ -118,7 +118,7 @@
 
 end
 
-lemma identity_quotient: "Quotient (op =) id id (op =)"
+lemma identity_quotient: "Quotient (=) id id (=)"
 unfolding Quotient_def by simp
 
 text \<open>TODO: Use one of these alternatives as the real definition.\<close>
@@ -217,7 +217,7 @@
 lemma UNIV_typedef_to_Quotient:
   assumes "type_definition Rep Abs UNIV"
   and T_def: "T \<equiv> (\<lambda>x y. x = Rep y)"
-  shows "Quotient (op =) Abs Rep T"
+  shows "Quotient (=) Abs Rep T"
 proof -
   interpret type_definition Rep Abs UNIV by fact
   from Abs_inject Rep_inverse Abs_inverse T_def show ?thesis
@@ -228,7 +228,7 @@
   fixes Abs :: "'a \<Rightarrow> 'b"
   and Rep :: "'b \<Rightarrow> 'a"
   assumes "type_definition Rep Abs (UNIV::'a set)"
-  shows "equivp (op= ::'a\<Rightarrow>'a\<Rightarrow>bool)"
+  shows "equivp ((=) ::'a\<Rightarrow>'a\<Rightarrow>bool)"
 by (rule identity_equivp)
 
 lemma typedef_to_Quotient:
@@ -284,7 +284,7 @@
 lemma Quotient_right_total: "right_total T"
   using 1 unfolding Quotient_alt_def right_total_def by metis
 
-lemma Quotient_rel_eq_transfer: "(T ===> T ===> op =) R (op =)"
+lemma Quotient_rel_eq_transfer: "(T ===> T ===> (=)) R (=)"
   using 1 unfolding Quotient_alt_def rel_fun_def by simp
 
 lemma Quotient_abs_induct:
@@ -306,7 +306,7 @@
 lemma Quotient_bi_total: "bi_total T"
   using 1 2 unfolding Quotient_alt_def bi_total_def reflp_def by auto
 
-lemma Quotient_id_abs_transfer: "(op = ===> T) (\<lambda>x. x) Abs"
+lemma Quotient_id_abs_transfer: "((=) ===> T) (\<lambda>x. x) Abs"
   using 1 2 unfolding Quotient_alt_def reflp_def rel_fun_def by simp
 
 lemma Quotient_total_abs_induct: "(\<And>y. P (Abs y)) \<Longrightarrow> P x"
@@ -343,7 +343,7 @@
   using T_def type Quotient_right_total typedef_to_Quotient
   by blast
 
-lemma typedef_rep_transfer: "(T ===> op =) (\<lambda>x. x) Rep"
+lemma typedef_rep_transfer: "(T ===> (=)) (\<lambda>x. x) Rep"
   unfolding rel_fun_def T_def by simp
 
 end
@@ -366,21 +366,21 @@
 
 lemma Quotient_composition_ge_eq:
   assumes "left_total T"
-  assumes "R \<ge> op="
-  shows "(T OO R OO T\<inverse>\<inverse>) \<ge> op="
+  assumes "R \<ge> (=)"
+  shows "(T OO R OO T\<inverse>\<inverse>) \<ge> (=)"
 using assms unfolding left_total_def by fast
 
 lemma Quotient_composition_le_eq:
   assumes "left_unique T"
-  assumes "R \<le> op="
-  shows "(T OO R OO T\<inverse>\<inverse>) \<le> op="
+  assumes "R \<le> (=)"
+  shows "(T OO R OO T\<inverse>\<inverse>) \<le> (=)"
 using assms unfolding left_unique_def by blast
 
 lemma eq_onp_le_eq:
-  "eq_onp P \<le> op=" unfolding eq_onp_def by blast
+  "eq_onp P \<le> (=)" unfolding eq_onp_def by blast
 
 lemma reflp_ge_eq:
-  "reflp R \<Longrightarrow> R \<ge> op=" unfolding reflp_def by blast
+  "reflp R \<Longrightarrow> R \<ge> (=)" unfolding reflp_def by blast
 
 text \<open>Proving a parametrized correspondence relation\<close>
 
@@ -391,19 +391,19 @@
 "NEG A B \<equiv> B \<le> A"
 
 lemma pos_OO_eq:
-  shows "POS (A OO op=) A"
+  shows "POS (A OO (=)) A"
 unfolding POS_def OO_def by blast
 
 lemma pos_eq_OO:
-  shows "POS (op= OO A) A"
+  shows "POS ((=) OO A) A"
 unfolding POS_def OO_def by blast
 
 lemma neg_OO_eq:
-  shows "NEG (A OO op=) A"
+  shows "NEG (A OO (=)) A"
 unfolding NEG_def OO_def by auto
 
 lemma neg_eq_OO:
-  shows "NEG (op= OO A) A"
+  shows "NEG ((=) OO A) A"
 unfolding NEG_def OO_def by blast
 
 lemma POS_trans:
@@ -487,7 +487,7 @@
 
 lemma composed_equiv_rel_eq_onp:
   assumes "left_unique R"
-  assumes "(R ===> op=) P P'"
+  assumes "(R ===> (=)) P P'"
   assumes "Domainp R = P''"
   shows "(R OO eq_onp P' OO R\<inverse>\<inverse>) = eq_onp (inf P'' P)"
 using assms unfolding OO_def conversep_iff Domainp_iff[abs_def] left_unique_def rel_fun_def eq_onp_def
@@ -496,14 +496,14 @@
 lemma composed_equiv_rel_eq_eq_onp:
   assumes "left_unique R"
   assumes "Domainp R = P"
-  shows "(R OO op= OO R\<inverse>\<inverse>) = eq_onp P"
+  shows "(R OO (=) OO R\<inverse>\<inverse>) = eq_onp P"
 using assms unfolding OO_def conversep_iff Domainp_iff[abs_def] left_unique_def eq_onp_def
 fun_eq_iff is_equality_def by metis
 
 lemma pcr_Domainp_par_left_total:
   assumes "Domainp B = P"
   assumes "left_total A"
-  assumes "(A ===> op=) P' P"
+  assumes "(A ===> (=)) P' P"
   shows "Domainp (A OO B) = P'"
 using assms
 unfolding Domainp_iff[abs_def] OO_def bi_unique_def left_total_def rel_fun_def
@@ -512,7 +512,7 @@
 lemma pcr_Domainp_par:
 assumes "Domainp B = P2"
 assumes "Domainp A = P1"
-assumes "(A ===> op=) P2' P2"
+assumes "(A ===> (=)) P2' P2"
 shows "Domainp (A OO B) = (inf P1 P2')"
 using assms unfolding rel_fun_def Domainp_iff[abs_def] OO_def
 by (fast intro: fun_eq_iff)