Hi Rob, > http://www.gilith.com/research/opentheory/faq.html#export-from-hol-light > > That's very useful. Are there any analogous instructions for exporting from > HOL4? Ramana: you're the expert on this. If you put together a few notes I'll gladly add them as a new FAQ. Cheers, Joe