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!


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.