Re: [isabelle] Status of HOL/Import

On 12.07.2011, at 09:56, Cezary Kaliszyk wrote:

> Dear all,
> After some struggling I succeeded running HOL/Import for HOLLight.
> (I wanted to port some of my older HOL-Light developments)
> The files present in the current repository version of Isabelle
> seem not to have been updated for quite a while (they still use
> the syntax "theory = ... + ..." which doesn't work for a while).
> Also the generation script refers to HOLLight constants not present
> at least since early 2005.
> Is anyone using HOL/Import or the theorems translated from HOLLight
> or can I update the generation and compatibility scripts to work
> with current Isabelle and svn HOLLight, add some constant maps
> and update the generated theorems?

It would be great if you manage to update this stuff. Let me know in case you get stuck somewhere.

- Steven

> Cezary

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