[isabelle] Status of HOL/Import

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?


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