Does anyone know if there's an article reader for HOL4? Or, in fact, which theorem provers have article readers, and where can they be found? I'm thinking if there is none for HOL4 I should write it, and then put it with the HOL4 sources - or should it come with the opentheory?