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