[isabelle-dev] HOL-ex.Sketch_and_Explore

[Simon Wimmer]

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
>:

> 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
> 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/20240315/1d81e657/attachment.htm>