src/HOL/Transfer.thy
changeset 80932 261cd8722677
parent 75669 43f5dfb7fa35
child 81100 6ae3d0b2b8ad
--- a/src/HOL/Transfer.thy	Mon Sep 23 12:59:10 2024 +0200
+++ b/src/HOL/Transfer.thy	Mon Sep 23 13:32:38 2024 +0200
@@ -13,8 +13,8 @@
 
 bundle lifting_syntax
 begin
-  notation rel_fun  (infixr "===>" 55)
-  notation map_fun  (infixr "--->" 55)
+  notation rel_fun  (infixr \<open>===>\<close> 55)
+  notation map_fun  (infixr \<open>--->\<close> 55)
 end
 
 context includes lifting_syntax