Consider requireing `redef` even if implementing an `abstract` feature

[fridis]

Since a redefinition inherits the pre- and post-conditions, not requiring redef when implementing an abstract feature is a little confusing. Maybe a different keyword override, implement, etc. would help?

[maxteufel]

I like this idea, and I don't think redef is a bad name for this. It makes perfect sense to me to redefine the abstract feature to a non-abstract one in the first place.