[isabelle-dev] HOLCF problem

Alexander Krauss krauss at in.tum.de
Sun Nov 28 12:13:26 CET 2010


Tobias Nipkow wrote:
> Brian's latest patch "remove HOLCF from build script, since it no longer
> works" has an unfortunate effect: the isabelle script now terminates
> immediately with
> Bad Isabelle component: "/Users/nipkow/isabelle/src/HOLCF"
> Which is annoying, given that I do not want to use HOLCF at all.
> Can I do something to avoid this?

The root /etc/components still mentions src/HOLCF. This should either be 
removed or changed to src/HOL/HOLCF. I removed it for now in 04d44a20fccf.

Alex



More information about the isabelle-dev mailing list