[isabelle-dev] Document preparation failure

[Rafal Kolanski]

Lawrence Paulson wrote:
> Something is wrong with the markup in theory Quotient.thy:
> 
> *** [819]) (./Quotient.tex [820] [821] [822] [823] [824]
> *** ! Missing $ inserted.
> *** <inserted text> 
> ***                 $
> *** l.797 ...vable; which is why we need to use apply_
> ***                                                   rsp and
> *** ! Missing $ inserted.

Looks like it should be @{const "apply_rsp"} or @{text "apply_rsp"} or 
something. The underscore is throwing it.

Sincerely,

Rafal Kolanski.