[isabelle-dev] Sketch and explore [was: performance problems]
florian.haftmann at informatik.tu-muenchen.de
Fri Mar 22 08:41:13 CET 2019
> * 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.
More information about the isabelle-dev