replace simp with the rewrites it used

Stream: new members

[Ariel Fridman]

Sometimes I use simp in the middle of a proof, which I know is a bad thing but it can be very useful in certain situations.

Is there an easy way to replace it with the rewrites it ran, except of setting trace.simplify.rewrite to true and copying the steps manually?

[Ruben Van de Velde]

squeeze_simp

[Ariel Fridman]

Ruben Van de Velde said:

squeeze_simp

ooh, that's useful. Thank you! ^^