Lawrence Paulson wrote:
> Something is wrong with the markup in theory Quotient.thy:
>
> *** [819]) (./Quotient.tex [820] [821] [822] [823] [824]
> *** ! Missing $ inserted.
> ***
> *** $
> *** l.797 ...vable; which is why we need to use apply_
> ***
The constant name and theorem name should now be quoted properly
and the documentation builds for me now.
Cezary
On Fri, Feb 19, 2010 at 5:31 PM, Brian Huffman wrote:
> On Fri, Feb 19, 2010 at 8:18 AM, Rafal Kolanski
> wrote:
>> Looks like it should be @{const "apply_rsp"} or @{text "apply_rsp
Something is wrong with the markup in theory Quotient.thy:
*** [819]) (./Quotient.tex [820] [821] [822] [823] [824]
*** ! Missing $ inserted.
***
*** $
*** l.797 ...vable; which is why we need to use apply_
*** rsp and
*** ! Missi
On Fri, Feb 19, 2010 at 8:18 AM, Rafal Kolanski
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
