Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Isabelle2025-RC2 VSCode sendback markup

Email Gateway (Feb 13 2025 at 08:59):

From: Fabian Huch <huch@in.tum.de>

5. (More of a feature wish):
When sledgehammering one often gets a found proof every few seconds.
Since in vscode the "try this: ..." aren't clickable one needs to
select the text manually.

In Isabelle/VSCode, we have "code actions" for sendback markup such as
sledgehammer suggestions.

Fabian

Last updated: Mar 09 2025 at 12:28 UTC