Re: [isabelle] translations/macros



On Wed, 30 Aug 2006, Christian Sternagel wrote:

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

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

You can omit the second one by using => instead of == above.  This will at 
least provide the input syntax.  The other direction can be done by 
low-level ML translations (cf. parse_translation), although I do not 
recommend this.


> Is there another way to define abbreviations like above?

In future versions of Isabelle, using 'abbreviation'.


	Makarius





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