[isabelle-dev] HOL-ex.Sketch_and_Explore

[Lawrence Paulson]

Many thanks for making those improvements!

It's so useful, I wonder why more people do not use it.

Larry
On 15 Mar 2024 at 18:00 +0000, Simon Wimmer <wimmersimon at gmail.com>, wrote:
Hi Larry,

in consultation with Fabian and Florian, I made a few changes that hopefully improve this further:

* Replaced `sketch` by `nxsketch` (and named it `sketch`)
* Reduced printing of superfluous type constraints
* Added configuration option `atp_proof_cartouches`, which allows to switch between cartouches and quotes for printing in sketch, explore, and Isar proofs generated by sledgehammer.
* Preserve indentation of generated proofs. However, keywords `sketch` and `explore` do not disappear anymore when the sketch is clicked on. The technical reason is that now `Active.sendback_markup_command` is used instead of `Active.sendback_markup_properties` .

Simon

Am Mo., 23. Okt. 2023 um 17:24 Uhr schrieb Lawrence Paulson <lp15 at cam.ac.uk<mailto:lp15 at cam.ac.uk>>:
Some of you will be aware of this theory, which provides commands “sketch” and “explore” to create Isar skeletons derived from the current set of subgoals. It can save a lot of time, a lot of typing, a lot of copying and pasting from the displayed proof state.

One thing I disliked was that it always introduced variables via “for” and local assumptions the “if”, even when there was only a single subgoal, increasing the nesting depth for no reason. So I have added a new command, currently called “nxsketch”, which fills in the context using “fix” and “assume”. I have also modified the sketch command to do the same thing if there is only one subgoal.

Perhaps people could try this out and see what they think. The name nxsketch could certainly be improved.

Larry

_______________________________________________
isabelle-dev mailing list
isabelle-dev at in.tum.de<mailto:isabelle-dev at in.tum.de>
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20240318/ba46d598/attachment.htm>