[isabelle] question about building HOL on cygwin



Dear Sirs

I tried to install Isabelle/HOL to my cygwin. 
I first installed SML/NJ which seems working well.
I then installed Isabelle and tried to build HOL.
But I got the following error message. I am afraid something is
wrong in the HOL source. I think so because

1) The build of FOL and ZF was successful and seems working well.
2) I tried the same thing with Linux and FreeBSD, and I got the
   same error message at the same place.

I thought that a heap file made with SML/NJ for Linux would work,
but I could not find any. The Isabelle Home Site presents only 
one build with PolyML, but I could  not install PolyML to my
cygwin. It seems that the Windows binary of PolyML distributed by
the site does not work with Isabelle.

Could you give me an adequate suggestion?

=================================================================
HOL FAILED
(see also /usr/local/Isabelle2005/heaps/smlnj-110_x86-cygwin/log/HOL)

lemma diff_def: ?x - ?y == ?x + - ?y
lemma add_minus_cancel: ?a + (- ?a + ?b) = ?b
lemma minus_add_cancel: - ?a + (?a + ?b) = ?b
lemma le_add_right_mono:
 [| ?a <= ?b + ?c; ?c <= ?d |] ==> ?a <= ?b + ?d
lemma estimate_by_abs: ?a + ?b <= ?c ==> ?a <= ?c + abs ?b
[opening /usr/local/Isabelle2005/src/HOL/OrderedGroup.ML]
*** exception Fail raised: stuck state
*** At command "use".
ExnDuringExecution
====================================================================





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.