Re: [isabelle] syntax translation

On 29.11.2012 08:00, Tobias Nipkow wrote:
Dear expert:
    I want to define a syntax abbreaviation as follows:
     In latex source  $n1\rightarrow_{SP}n2 \equiv (n1,n2) \in casual SP$
(please see the figures in attachment),
If I replace "node", "strand_space", "member" and "casual" (which I don't have)
and just define

   "_casual1" :: " ['a,'b,'a]\<Rightarrow>bool" ("_\<rightarrow>_/ _")

    "n1\<rightarrow>SP n2" ==  "(n1,n2) : SP"

Actually, what is the advantage of using syntax/translations here instead of mixfix annotations?

  -- Lars

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