Email Gateway (Aug 18 2022 at 14:44): Email Gateway (Aug 18 2022 at 14:44):From: Viorel Preoteasa <viorel.preoteasa@abo.fi>
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
Email Gateway (Aug 18 2022 at 14:44):From: Tobias Nipkow <nipkow@in.tum.de>
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.
Tobias
Viorel Preoteasa wrote:
Last updated: Apr 19 2024 at 20:15 UTC