A suggestion and some compliments... Larry Begin forwarded message:
> From: James Frank <s...@gmx.com> > Subject: Needed ghostscript package to build PDF in Cygwin > Date: 5 October 2011 15:54:30 GMT+01:00 > To: l...@cam.ac.uk > > Dear Dr. Paulson, > > The problem I had with building the Isabelle PDF documents under Cygwin is > actually an excuse to thank you for producing Isabelle. > > You might consider adding ghostscript as a Cygwin package requirement on: > http://www.cl.cam.ac.uk/research/hvg/Isabelle/download.html > > I built the HOL, ZF, and IsarMathLib document.pdf files several times, but > then it started complaining about not piping to ghostscript, although it > would build the FOL document.pdf. I installed the Cygwin ghostscript package, > and then it started working again. > > I was tempted to go with Coq, since I wasn't set up with a Unix environment, > but now, the more I learn about Isabelle, the happier I get about it. > > With the choice between HOL and ZF, and the combination of all the tools, > Isabelle is incredible. I run jEdit under Cygwin to get the benefits of the > tree view and continuous proving, and I run Proof General under Ubuntu in > VirtualBox to get the extra information it gives me, along with the ATPs > running better under Linux. > > I could go on. The integration with Latex is super cool. I live and die by > tree views, particularly in IDE's and using the bookmarks of a PDF. With the > Isabelle sectioning commands, along with jEdit sidekick, and the ability to > create PDFs using LaTeX, it's all good. Documentation is a huge part of being > able to use a software tool. > > Thanks again. Proof assistants open a whole new dimension in regards to > finding opportunity in math. > > -- James Frank _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev