Re: [isabelle] Using Isabelle on Intel Macintosh?

I have a great respect and admiration for the Isabelle system, and wish to learn more about it, in addition to HOL4.  One area of possible application is a port of my higher order quotients project from HOL4 to Isabelle/HOL.  I believe this would be a good learning experience for me, and possibly useful to others.  When speaking with Christian Urban during FLoC about his nominal datatypes package, he shared that having higher order quotients available might have made his project easier.


-----Original Message-----
>From: Lawrence Paulson <lp15 at>
>Sent: Sep 1, 2006 1:23 AM
>To: "Peter V. Homeier" <palantir at>
>Cc: David Matthews <David.Matthews at>, Cl-isabelle-users at
>Subject: Re: Using Isabelle on Intel Macintosh?
>Poly/ML gives better performance than SML/NJ, probably because of its  
>better garbage collector. However, SML/NJ is quite usable.
>I'm interested to hear that you are using Isabelle rather than HOL.  
>Are there any interesting details you can share?
>On 31 Aug 2006, at 21:39, Peter V. Homeier wrote:
>> How would you compare Poly/ML and SMLNJ with respect to supporting  
>> Isabelle?

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