On Mon, 24 Feb 2014, Lawrence Paulson wrote:

What I’d love to see is completion of theorem names...

Definitely. I continue to work through the sediments, to expose the required markup information.

In Isabelle/e5128a9c4311 proof methods already work. Next will be attributes and facts, but that is a bit more convoluted for historical reasons.


        Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Reply via email to