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

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

translations
    "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.