Re: [isabelle] Status of HOL/Import



Alas, nobody has been using this for some time and it has fallen into
disrepair. If you can get it to work again, you are very welcome!

Tobias

Am 12/07/2011 09:56, schrieb Cezary Kaliszyk:
> 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?
> 
> Cezary





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