[MLton-devel] Re: Question

[Stephen Weeks]

> (although I have no idea if you can compile HOL out of the box with
> MLton).

We had an email exchange with Larry Paulson back in summer 2000 (I
would have thought you were on the list by then) where he pointed out
that Isabelle uses "use" in many places and hence cannot be compiled
by MLton.  Since HOL is based on Isabelle, I assume it suffers from
the same problem.  I have no idea if the situation is better in HOL4.
Back in 2000, I took a look into Isabelle and it didn't seem that many
of the uses of "use" were that fundamental, but it looked like a lot
of work to rip them out.


-------------------------------------------------------
This sf.net email is sponsored by:ThinkGeek
Welcome to geek heaven.
http://thinkgeek.com/sf
_______________________________________________
MLton-devel mailing list
MLton-devel@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/mlton-devel