Hi everyone,
Am Freitag, den 19.11.2010, 20:38 +0100 schrieb Makarius:
> The underlined " is crashing here due to the extra markup that tells that
> it is a literal quote.
>
> In the default setup, this is defined as follows:
>
> \newcommand{\isaliteral}[2]{#2}
>
> I have also tried \DeclareRobustCommand but \uline still crashes.
>
> This one seems to work:
>
> \newcommand{\isactrlps}[1]{\underline{#1}}
>
>
> Is there anything special about ulem.sty that is required here?
>
> In any case, \<^ps> can only treat a single Isabelle symbol (letter etc.).
> If more text should be marked up reliably, it would have to be done via
> slightly more awkward \<^bps>...\<^eps> that act like parentheses in
> LaTeX (\bgroup ... \egroup or similar).I’m sorry for the trouble my submission causes. When writing the theories I had planned to actually use the proof document as my project report, therefore the trouble I went through to have the syntax as similar to Shivers’s dissertation as possible. In the end I was asked to not use the proof document as the report, so these syntax are not really required any more. If you want I can completely get rid of them in the developer repository of the AFP. Same with unicode apostrophes. I used \ulem because I recently worked on a project that required well-typeset text, where it has advantages over \underline, such that it stills allows hyphenation. In this case, these extra features are unnecessary and \underline can be used as well. My version of ulem.sty has a header % U L E M . S T Y [2000-05-26] and is part of the texlive-latex-base package in Debian unstable, version 2009-11. And while I am at it: Although I knew that technically, HOLCF is but an conservative extension to HOL, I concluded from its listing on the homepage parallel to HOL that it should be “considered” an alternative, and not just a library. Maybe this was also the reasons for my advisors to initially advice against the use of it. If that is not the intention I support Brian’s suggestions to move it next to other HOL libraries. Greetings, Joachim -- Joachim "nomeata" Breitner mail: [email protected] | ICQ# 74513189 | GPG-Key: 4743206C JID: [email protected] | http://www.joachim-breitner.de/ Debian Developer: [email protected]
signature.asc
Description: This is a digitally signed message part
_______________________________________________ Isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
