Stefan> package: polyml Stefan> Description: Poly/ML is a full implementation Stefan> of Standard ML available as open-source (more in [3]).
I wanted to do this myself a few weeks ago, but the opinion on -legal is unanimous: PolyML is non-free. Stefan> Isabelle: As far as I understand (I haven't asked about this one), it is also non-free (note restriction to non-commercial use). Yes, it stinks - these are great tools. -- Ian Zimmerman, Oakland, California, U.S.A. GPG: 433BA087 9C0F 194F 203A 63F7 B1B8 6E5A 8CA3 27DB 433B A087 EngSoc adopts market economy: cheap is wasteful, efficient is expensive.

