On Fri, 17 Dec 2010, Tjark Weber wrote:
One could think about (tool support for) formally checked hyperlinks
from ML sources into LaTeX (and other) documents.
We have been moving towards that for several years. At least the manuals
maintained by myself contain many formally checked entities. It is just a
matter of a bit more technical support in doc browsing to get a whole lot
of links. I have also thought about links to formal "concepts", too.
Does jEdit offer useful functionality? But that would be a major move.
There is nothing for free on the JVM. It is a platform where people make
a lot of money. There is a decent HTML free browser ("Lobo/Cobra"), but
no reasonable PDF viewer.
Perhaps Jasmin has some experience.
His manuals are not even formally checked by Isabelle, so this is two
steps backwards.
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
