[isabelle] recdef tuple for 2 args, infix syntax possible?



Due to it's structure, I need to use recdef for the matchE function (signature below). Since recdef takes one argument only, I had to present it with a tuple (expr \<times> expr).

Is there any way for me to still be able to create an infix syntax? Ideally I'd like to write "x \<subseteq>E y" as if I had been able to use primrec.

I've scanned the tutorial, google and the reference manual, but was unable to locate a relevant example.

Thanks,
- Reto

consts matchE :: "expr \<times> expr \<Rightarrow> bool" ("\<subseteq>E" 500) <-- prefix ok, infix though?
recdef matchE "measure (\<lambda>(e1,e2). depthE e1 + depthE e2)"
...






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.