伊莎贝尔：如何I位置固定的论点mixfix符号？

Question

说我有一个关系，其中关系由二元谓词表示的自反传递闭包的定义如下：

inductive
  closure :: "(['a, 'a] ⇒ bool) ⇒ (['a, 'a] ⇒ bool)"
  for ℛ (infix "→" 50)
where
  gen:
    "x → y ⟹ closure (→) x y" |
  refl:
    "closure (→) x x" |
  trans:
    "⟦closure (→) x y; closure (→) y z⟧ ⟹ closure (→) x z"

我想为closure的应用程序更好的语法。说我希望能够写x *(→)* y为closure (→) x y。问题是，在这个符号的参数顺序不匹配功能closure的参数顺序。

我想也许使用\<index>的可能会有帮助。不幸的是，在\<index> Isabelle/Isar Reference Manual的文档是非常简洁的，我真的无法理解它。我打得有点与\<index>，但没有发现任何可行的解决方案。

令我困惑的是，显然\<index>被翻译成⇘some_index⇙，从我得到了一些错误信息判断。我试图用⇘ℛ⇙来标记的基本关系应该去的位置，但是这也不能工作。