[isabelle-dev] Sketch and explore [was: performance problems]

[Florian Haftmann]

Hi Mathias,

>   * I don't like the idea that sketch and explore require an additional argument. I often use (a variant of) it on goals generated by refine_vcg (from Refine_Imperative_HOL). I guess I could call "sketch (tactic ‹all_tac›)", but I would prefer that no argument means no tactic call. On the other hand, I might have a strange use-case.

»sketch -« and »explore -« work as expected, although the latter does
not make much sense.

Cheers,
	Florian