--- a/src/HOL/Power.thy Wed Oct 23 16:09:23 2019 +0000
+++ b/src/HOL/Power.thy Wed Oct 23 16:09:24 2019 +0000
@@ -28,6 +28,19 @@
end
+context
+ includes lifting_syntax
+begin
+
+lemma power_transfer [transfer_rule]:
+ \<open>(R ===> (=) ===> R) (^) (^)\<close>
+ if [transfer_rule]: \<open>R 1 1\<close>
+ \<open>(R ===> R ===> R) (*) (*)\<close>
+ for R :: \<open>'a::power \<Rightarrow> 'b::power \<Rightarrow> bool\<close>
+ by (simp only: power_def [abs_def]) transfer_prover
+
+end
+
context monoid_mult
begin