Hi, On Tue, Sep 05, 2006 at 09:21:54AM -0400, Ian Zimmerman wrote:
I added a bit of infrastructure to maintain the chain of child databases for libraries. I myself intend to package a couple of libraries from the net, such as FGL and FXP. Later I'll tackle
do you have FXP (I assume you mean the XML Parser, aren't you) runnign with PolyML. I thought PolyML still lacks the Word32 structure which is needed by FXP. At least for us, the workaround of using LargeWord instead of Word32 resulted in a non-functional fxp...
either Isabelle or ProofPower, but that will be a much bigger job.
Debian Packages for Isabelle 2005 (based on sml/nj) and Proof General are available from my website:
http://www.brucker.ch/projects/debian/
The packages should be easily rebuild-able with Polyml. At the moment I'm using sml/nj mainly because HOL-OCL depends on FXP. If FXP can be used with Polyml I will happily provide Polyml-based Isabelle packages. In that case, I would propaply used these packages for the next IsaMorph release (A linux live CD which includes Isabelle).
Achim