[isabelle-dev] AFP/Shivers-CFA latex document problem

[Joachim Breitner]

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: mail at joachim-breitner.de | ICQ# 74513189 | GPG-Key: 4743206C
  JID: nomeata at joachim-breitner.de | http://www.joachim-breitner.de/
  Debian Developer: nomeata at debian.org
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 198 bytes
Desc: This is a digitally signed message part
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20101119/67591e41/attachment.sig>