[isabelle-dev] HOL-ex.Sketch_and_Explore

[Lawrence Paulson]

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