[isabelle] translations/macros



As far as I figured out, it is not possible to
define a translation like

--------------------------------------------------------------------------------
syntax
 "_common_rewrite_step" :: "['a, 'a, 'a] => bool" ("_ ---> _ <--- _" 100)

translations
 "a ---> c <--- b" == "(a,c) : r & (b,c) : r"
--------------------------------------------------------------------------------

because internally two rewrite rules are established and
one of it is not left-linear.

Is there another way to define abbreviations like above?

mfG

Christian Sternagel





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