[isabelle-dev] Local Specification Mechanisms: Brief Experience Report

[Makarius]

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