[isabelle-dev] Local Specification Mechanisms: Brief Experience Report
makarius at sketis.net
Fri Dec 17 23:36:44 CET 2010
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
More information about the isabelle-dev