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 afp.sf.net
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
> 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