Merged requested to merge ralf/rename_op_core into master
_op etc should be a suffix.
What this MR does not fix is the inconsistency between the
f_op lemmas on the one side and the
f_included lemmas on the other side: the former have the "operation at the result type of
f" (so, e.g. the composition of gmaps, for the
singleton_ lemmas) on the right-hand side, while the latter have it on the left-hand side.
Cc @iris-users because this is a breaking change, but should be fairly easy to fix.