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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
