Re: [isabelle-dev] Relations vs. Predicates

2012-04-03 Thread Florian Haftmann
Hi Christian, Sorry, I'm not familiar with the developer workflow. I do have a cloned hg repo of Isabelle (from http://isabelle.in.tum.de/repos/isabelle), but I don't see an IsaMakefile (which would be required for isabelle make all). Where is this IsaMakefile located? it is »isabelle makeall

Re: [isabelle-dev] isabelle test failed -- HOL-Library-Codegenerator_Test

2012-04-03 Thread Florian Haftmann
Am 02.04.2012 13:36, schrieb Florian Haftmann: /mnt/home/isatest/isadist/Isabelle_02-Apr-2012/lib/scripts/run-polyml: line 77: 27590 Killed $POLY -q $ML_OPTIONS *** Code check failed for SML: $ISABELLE_PROCESS -r -q -u Pure *** At command export_code (line 17 of

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

2012-04-03 Thread 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