[isabelle-dev] src/Doc/Corec fails

[Jasmin Blanchette]

> 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