[isabelle-dev] New manual Programming and Proving in Isabelle/HOL

Tobias Nipkow nipkow at in.tum.de
Wed Apr 4 09:40:24 CEST 2012


Am 03/04/2012 22:51, schrieb Florian Haftmann:
>>> I'm indedd quite curious, but unable to build the tex sources.  The
>>> first error complains about a missing »eulervm.sty«, with lot of
>>> further messages following.
>> 
>> You mean you couldn't run the tex sources? Unfortunately I can confirm
>> that. It appears that the tex installation on the macbroys does not have
>> eulervm (texlive on my mac does come with it). I will probably need to
>> add it to my sources.
> 
> I have resolved it by installing the eulervm package.

Which our sysadmins have also installed on (all?) the relevant relevant
machines now.

Tobias

> We do not have formally tracked tex dependencies in Isabelle.  But I have
> no idea how we would accomplish this if we wanted to.
> 
> Florian
> 



More information about the isabelle-dev mailing list