Re: [isabelle] quoting definitions in latex



>You cannot quote type abbreviations but definitions work: @{thm f_def}

I hadn't thought of that, but it destroys the line breaks and
indentation, so it looks like the only real option is to cut-and-paste
from the generated LaTeX :(   A crude but very useful thing we do in
Ott, which maybe could be done by Isabelle with minimal effort, is to
factor generated LaTeX into definitions of separate LaTeX commands
to generate each component of the output, with a predictable naming
convention - e.g. 

\newcommand{\myisadatatypeXXXdirn}{dirn\ {\isacharequal}\ R\ {\isacharbar}\ W}

in one file, with

\isanewline
\isacommand{datatype}\isamarkupfalse%
\ \myisadatatypeXXXdirn\ \ \ \isanewline
\isanewline

in another, instead of 

\isanewline
\isacommand{datatype}\isamarkupfalse%
\ dirn\ {\isacharequal}\ R\ {\isacharbar}\ W\ \ \ \isanewline
\isanewline

>You may also want to look at "LaTeX sugar for proof documents" 
>http://isabelle.in.tum.de/dist/Isabelle/doc/sugar.pdf

y - seen that, which looks useful indeed.

>There is no way to display "!" etc as \forall, you need to write it that 
>way in the first place - it's a subtle issue.


thanks,
Peter





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.