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.