This repository adds an explore_subgoal
command to Mathias Fleury's Explorer.thy.
The original theory can be found here:
https://bitbucket.org/isafol/isafol/src/master/lib/Explorer.thy.
The commands provided in this theory allow one to generate templates for Isar proofs from the
current goal state.
The new command generates a template in a form of a number of subgoal
commands for an apply-style
proof.
Import the theory and type explore_subgoal
during a proof
(or try explore
, explore_have
, explore_lemma
, or explore_context
).