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.
