[isabelle-dev] Document preparation failure

Cezary Kaliszyk cezarykaliszyk at gmail.com
Fri Feb 19 17:40:30 CET 2010


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 <brianh at cs.pdx.edu> wrote:
> 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
> _______________________________________________
> Isabelle-dev mailing list
> Isabelle-dev at mailbroy.informatik.tu-muenchen.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>



-- 
Cezary Kaliszyk kaliszyk at in.tum.de
Nominal Methods Group, Technische Universität München
http://www4.in.tum.de/~kaliszyk/



More information about the isabelle-dev mailing list