Re: [isabelle] relation composition

You can define your own abbreviation, eg

abbreviation rel_comp2 (infixr "O''" 75) where "r O' s == s O r"

Now you just need to replace O by O' (unfortunately OO is already taken).

You might also consider submitting your theories to the AFP
where they are updated by us when we modify Isabelle.


Viorel Preoteasa wrote:
> I am trying to port some old theories to the latest version of Isabelle,
> and I discovered that the relation composition has changed.
> I am writing to ask if there is a different symbol for the relation
> composition
> which matches the old definition? I would rather change the symbol than
> to swap the relational terms because they are long and swapping them
> is more error prone.
> Best regards,
> Viorel Preoteasa

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