[isabelle-dev] HTML output

Haslbeck, Maximilian Maximilian.Haslbeck at uibk.ac.at
Mon Mar 18 13:25:19 CET 2019


In one of our recent papers we provided direct links to the corresponding Isabelle definitions, lemmas, etc (for example [1]). The anchors inside Isabelle’s HTML output were added with a very crude shell script with multiple invocations of sed.

So it would be great if the necessary id tags (and other semantic information) could be added by Isabelle itself. I’m willing to implement this myself but I would need some general pointers in the right direction. I’m guessing I can implement this with Isabelle/Scala, right?


[1] <http://cl-informatik.uibk.ac.at/isafor/experiments/lll/browser_info/AFP/LLL_Basis_Reduction/LLL_GSO_Impl.html#def:basis_reduction_main>

More information about the isabelle-dev mailing list