Email Gateway (Oct 23 2023 at 15:24): Email Gateway (Oct 23 2023 at 15:24):From: Lawrence Paulson <lp15@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@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Mar 15 2024 at 18:01):From: Simon Wimmer <wimmersimon@gmail.com>
Hi Larry,
in consultation with Fabian and Florian, I made a few changes that
hopefully improve this further:
sketch by nxsketch (and named it sketch)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
Email Gateway (Mar 18 2024 at 15:12):From: Lawrence Paulson <lp15@cam.ac.uk>
Many thanks for making those improvements!
It's so useful, I wonder why more people do not use it.
Larry
Email Gateway (Mar 20 2024 at 09:57):From: Makarius <makarius@sketis.net>
So how about an entry in NEWS for the coming release?
Makarius
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
Email Gateway (Mar 20 2024 at 10:47):From: Lawrence Paulson <lp15@cam.ac.uk>
Happy to, but I can't do a thing until somebody restores my account at TUM, which apparently was deleted last week
Larry
Last updated: Apr 28 2024 at 16:17 UTC