[isabelle-dev] Document preparation failure

Brian Huffman brianh at cs.pdx.edu
Fri Feb 19 17:31:17 CET 2010

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

More information about the isabelle-dev mailing list