On Thu, 7 Apr 2016, Makarius wrote: > Maybe some other big applications of Poly/ML should be made > PIDE-compliant as well, e.g. HOL4 or even Poly/ML itself. Or maybe even this one: https://bitbucket.org/lcpaulson/metitarski Makarius