rw / rewrite

Stream: lean4

[Ruben Van de Velde]

I just noticed this, and maybe some of you may be interested as well: in lean 4, rw and rewrite are no longer synonyms; only rw tries the (reducible) rflat the end