Stream: general

Topic: extract_goal

Johan Commelin (May 29 2020 at 18:07):

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 (May 29 2020 at 18:07):

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

Last updated: May 13 2021 at 17:42 UTC