1open OpenTheoryIO 2exception D 3fun main() = let 4 val t = article_to_term TextIO.stdIn 5 val _ = thm_to_article TextIO.stdOut (fn () => numLib.DECIDE t) 6in () end 7handle Feedback.HOL_ERR e => (print (Feedback.format_ERR e); raise D) 8 | e => (PolyML.print e; raise D) 9val _ = PolyML.export("holdecide",main) 10