Implement a pretty-printer to HOL-Light
To compare our work with the verified supremum norm of Chevillard et al (2011) we should implement a pretty-printer from HOL4 polynomials to HOL-Lights REAL_SOS_CONV
which is the closest still working tool to the approach presented in that paper. The code should be based on the code in realZeroLib.sml
.