--- a/src/HOL/Nonstandard_Analysis/HLog.thy Fri Sep 20 19:07:10 2024 +0200
+++ b/src/HOL/Nonstandard_Analysis/HLog.thy Fri Sep 20 19:51:08 2024 +0200
@@ -9,7 +9,7 @@
imports HTranscendental
begin
-definition powhr :: "hypreal \<Rightarrow> hypreal \<Rightarrow> hypreal" (infixr "powhr" 80)
+definition powhr :: "hypreal \<Rightarrow> hypreal \<Rightarrow> hypreal" (infixr \<open>powhr\<close> 80)
where [transfer_unfold]: "x powhr a = starfun2 (powr) x a"
definition hlog :: "hypreal \<Rightarrow> hypreal \<Rightarrow> hypreal"