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).