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