On 15/07/16 11:49, Lawrence Paulson wrote:
> It’s great, but can I pester you about my pet wish? It would be some sort of
> “auto-complete” e.g. I type “proof (cases blah)” and somehow automatically
> the full “case True show … next case False show … qed” skeleton could be
> generated? The same for induction? I know this is far from easy, given the
> amount of contextual information involved.
It is probably rather trivial. I will come back to variations on
sendback information eventually. One reason it was not done very often
so far is rather profane: lack of indentation for the inserted text.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
