extract_goal

Stream: general

[Johan Commelin]

Can we "Try this"-ify extract_goal? We can't use "Try this" immediately, I think, because we want to put the generated lemma before the current lemma and replace extract_goal foobar with apply foobar.

[Johan Commelin]

So we would need to do 2 replacements in one go.