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

[Brian Huffman]

On Fri, Nov 19, 2010 at 2:40 PM, Joachim Breitner
<mail at joachim-breitner.de> wrote:
> Hi everyone,
[...]
> 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.

Hi Joachim,

Don't worry about any of this document-generation trouble; none of it
was your fault. Fancy report-quality LaTeX syntax is supposed to be a
supported feature of Isabelle document generation. The incompatibility
between the ulem package and the development version of Isabelle is
unfortunate, and hopefully workarounds can be found so that users can
continue to use ulem and other LaTeX packages in the future.

> 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.

I went ahead and changed the \isactrlps command (defined in your
root.tex) to use \underline instead of \uline. (Other uses of \uline
apparently don't cause problems.)

http://afp.hg.sourceforge.net/hgweb/afp/afp/rev/2423a888e2e7

I also took the liberty of replacing all the unicode quotes with ascii
ones (otherwise the quotes don't appear in the pdf at all) and fixing
various typos and misspellings that I found along the way. Hopefully I
haven't introduced any errors; you might want to inspect the changeset
to make sure:

http://afp.hg.sourceforge.net/hgweb/afp/afp/rev/531cf578b0d7

> 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

Thanks for deciding to stick with HOLCF, even despite the initial
advice of your advisors. Having more users makes all my work on
improving HOLCF seem worthwhile! And if the way HOLCF is presented in
the Isabelle documentation and website was the reason for your
advisors' reluctance, that is more motivation for me to move HOLCF
into a more logical place. I will make sure this is done before the
next release.

- Brian