diff -r b4564de51fa7 -r cc204e10385c src/HOL/Code_Numeral.thy
--- a/src/HOL/Code_Numeral.thy	Tue Oct 22 19:07:12 2019 +0000
+++ b/src/HOL/Code_Numeral.thy	Wed Oct 23 16:09:23 2019 +0000
@@ -77,38 +77,45 @@
 
 instance integer :: Rings.dvd ..
 
-lemma [transfer_rule]:
-  "rel_fun pcr_integer (rel_fun pcr_integer HOL.iff) Rings.dvd Rings.dvd"
-  unfolding dvd_def by transfer_prover
+context
+  includes lifting_syntax
+  notes transfer_rule_numeral [transfer_rule]
+begin
 
 lemma [transfer_rule]:
-  "rel_fun (=) pcr_integer (of_bool :: bool \<Rightarrow> int) (of_bool :: bool \<Rightarrow> integer)"
+  "(pcr_integer ===> pcr_integer ===> (\<longleftrightarrow>)) (dvd) (dvd)"
+  by (unfold dvd_def) transfer_prover
+
+lemma [transfer_rule]:
+  "((\<longleftrightarrow>) ===> pcr_integer) of_bool of_bool"
   by (unfold of_bool_def [abs_def]) transfer_prover
 
 lemma [transfer_rule]:
-  "rel_fun (=) pcr_integer (of_nat :: nat \<Rightarrow> int) (of_nat :: nat \<Rightarrow> integer)"
+  "((=) ===> pcr_integer) int of_nat"
   by (rule transfer_rule_of_nat) transfer_prover+
 
 lemma [transfer_rule]:
-  "rel_fun (=) pcr_integer (\<lambda>k :: int. k :: int) (of_int :: int \<Rightarrow> integer)"
+  "((=) ===> pcr_integer) (\<lambda>k. k) of_int"
 proof -
-  have "rel_fun HOL.eq pcr_integer (of_int :: int \<Rightarrow> int) (of_int :: int \<Rightarrow> integer)"
+  have "((=) ===> pcr_integer) of_int of_int"
     by (rule transfer_rule_of_int) transfer_prover+
   then show ?thesis by (simp add: id_def)
 qed
 
 lemma [transfer_rule]:
-  "rel_fun HOL.eq pcr_integer (numeral :: num \<Rightarrow> int) (numeral :: num \<Rightarrow> integer)"
-  by (rule transfer_rule_numeral) transfer_prover+
+  "((=) ===> pcr_integer) numeral numeral"
+  by transfer_prover
 
 lemma [transfer_rule]:
-  "rel_fun HOL.eq (rel_fun HOL.eq pcr_integer) (Num.sub :: _ \<Rightarrow> _ \<Rightarrow> int) (Num.sub :: _ \<Rightarrow> _ \<Rightarrow> integer)"
+  "((=) ===> (=) ===> pcr_integer) Num.sub Num.sub"
   by (unfold Num.sub_def [abs_def]) transfer_prover
 
 lemma [transfer_rule]:
-  "rel_fun pcr_integer (rel_fun (=) pcr_integer) (power :: _ \<Rightarrow> _ \<Rightarrow> int) (power :: _ \<Rightarrow> _ \<Rightarrow> integer)"
+  "(pcr_integer ===> (=) ===> pcr_integer) (^) (^)"
   by (unfold power_def [abs_def]) transfer_prover
 
+end
+
 lemma int_of_integer_of_nat [simp]:
   "int_of_integer (of_nat n) = of_nat n"
   by transfer rule