[isabelle-dev] Document preparation failure

[Brian Huffman]

On Fri, Feb 19, 2010 at 8:18 AM, Rafal Kolanski <rafalk at cse.unsw.edu.au> wrote:
> Looks like it should be @{const "apply_rsp"} or @{text "apply_rsp"} or
> something. The underscore is throwing it.

That's exactly it. There's actually a second problem of the same kind
later on, in a subsection heading. I have a fix on my local
repository, and I'll push it as soon as I can rebuild the HOL-Main
image (assuming it works!)

- Brian