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