[isabelle-dev] src/Doc/Corec fails

Jasmin Blanchette jasmin.blanchette at inria.fr
Sat Apr 2 17:14:46 CEST 2016


> The problem is a missing macro \textsubscript

Thanks for the heads-up. I added the "subscript" package, which is supposed to help (d0fc75798baf); then I reverted that and gave up the idea of having bold subscripts (19387866eace), since there was another issue with \textsubscript (spurious underscores).

> In the last 10 years, Isabelle documentation has used fewer and fewer LaTeX specialities. There is still hope that we can produce HTML + CSS at some point.
> 
> This works as long as only Isabelle antiquotations or control symbols are used.

I don't know any good way of putting Isabelle text as produced by antiquotations in bold. Do you?

Jasmin




More information about the isabelle-dev mailing list