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

Florian Haftmann florian.haftmann at informatik.tu-muenchen.de
Fri Mar 22 08:41:13 CET 2019

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.


More information about the isabelle-dev mailing list