[isabelle-dev] \nexists

[Lars Hupel]

> Latex tests add very little information for the extra time. It is
> usually easy to figure out what needs to be done to make a broken
> document work again. Moreover, the test often fails because of bad latex
> installations, not because of bad documents.

I disagree. 0% of LaTeX failures observed on the new infrastructure are
spurious, so I'm inclined to keep them running.

Even more so because I will flip the switch to have Jenkins generate
devel.isa-afp.org including browser_info and documents this weekend.

Cheers
Lars