diff --git a/src/api/api_rcf.cpp b/src/api/api_rcf.cpp
index b325c4397..42558ba9e 100644
--- a/src/api/api_rcf.cpp
+++ b/src/api/api_rcf.cpp
@@ -98,13 +98,13 @@ extern "C" {
         Z3_CATCH_RETURN(0);
     }
 
-    Z3_rcf_num Z3_API Z3_rcf_mk_infinitesimal(Z3_context c, Z3_string name) {
+    Z3_rcf_num Z3_API Z3_rcf_mk_infinitesimal(Z3_context c) {
         Z3_TRY;
-        LOG_Z3_rcf_mk_infinitesimal(c, name);
+        LOG_Z3_rcf_mk_infinitesimal(c);
         RESET_ERROR_CODE();
         reset_rcf_cancel(c);
         rcnumeral r;
-        rcfm(c).mk_infinitesimal(name, r);
+        rcfm(c).mk_infinitesimal(r);
         RETURN_Z3(from_rcnumeral(r));
         Z3_CATCH_RETURN(0);
     }
@@ -268,13 +268,13 @@ extern "C" {
         Z3_CATCH_RETURN(Z3_FALSE);
     }
 
-    Z3_string Z3_API Z3_rcf_num_to_string(Z3_context c, Z3_rcf_num a, Z3_bool compact) {
+    Z3_string Z3_API Z3_rcf_num_to_string(Z3_context c, Z3_rcf_num a, Z3_bool compact, Z3_bool html) {
         Z3_TRY;
-        LOG_Z3_rcf_num_to_string(c, a, compact);
+        LOG_Z3_rcf_num_to_string(c, a, compact, html);
         RESET_ERROR_CODE();
         reset_rcf_cancel(c);
         std::ostringstream buffer;
-        rcfm(c).display(buffer, to_rcnumeral(a), compact != 0);
+        rcfm(c).display(buffer, to_rcnumeral(a), compact != 0, html != 0);
         return mk_c(c)->mk_external_string(buffer.str());
         Z3_CATCH_RETURN("");
     }
diff --git a/src/api/python/z3rcf.py b/src/api/python/z3rcf.py
index b9c947b9f..66a6890c3 100644
--- a/src/api/python/z3rcf.py
+++ b/src/api/python/z3rcf.py
@@ -29,8 +29,10 @@ def E(ctx=None):
     return RCFNum(Z3_rcf_mk_e(ctx.ref()), ctx)
 
 def MkInfinitesimal(name="eps", ctx=None):
+    # Todo: remove parameter name.
+    # For now, we keep it for backward compatibility.
     ctx = z3._get_ctx(ctx)
-    return RCFNum(Z3_rcf_mk_infinitesimal(ctx.ref(), name), ctx)
+    return RCFNum(Z3_rcf_mk_infinitesimal(ctx.ref()), ctx)
 
 def MkRoots(p, ctx=None):
     ctx = z3._get_ctx(ctx)
@@ -49,6 +51,7 @@ def MkRoots(p, ctx=None):
     return r
 
 class RCFNum:
+    html = False
     def __init__(self, num, ctx=None):
         # TODO: add support for converting AST numeral values into RCFNum
         if isinstance(num, RCFNumObj):
@@ -65,10 +68,10 @@ class RCFNum:
         return self.ctx.ref()
                   
     def __repr__(self):
-        return Z3_rcf_num_to_string(self.ctx_ref(), self.num, False)
+        return Z3_rcf_num_to_string(self.ctx_ref(), self.num, False, RCFNum.html)
 
     def compact_str(self):
-        return Z3_rcf_num_to_string(self.ctx_ref(), self.num, True)
+        return Z3_rcf_num_to_string(self.ctx_ref(), self.num, True, RCFNum.html)
 
     def __add__(self, other):
         v = _to_rcfnum(other, self.ctx)
diff --git a/src/api/z3_rcf.h b/src/api/z3_rcf.h
index 305033690..e2b4b7e05 100644
--- a/src/api/z3_rcf.h
+++ b/src/api/z3_rcf.h
@@ -64,9 +64,9 @@ extern "C" {
     /**
        \brief Return a new infinitesimal that is smaller than all elements in the Z3 field.
 
-       def_API('Z3_rcf_mk_infinitesimal', RCF_NUM, (_in(CONTEXT), _in(STRING)))
+       def_API('Z3_rcf_mk_infinitesimal', RCF_NUM, (_in(CONTEXT),))
     */
-    Z3_rcf_num Z3_API Z3_rcf_mk_infinitesimal(__in Z3_context c, __in Z3_string name);
+    Z3_rcf_num Z3_API Z3_rcf_mk_infinitesimal(__in Z3_context c);
 
     /**
        \brief Store in roots the roots of the polynomial <tt>a[n-1]*x^{n-1} + ... + a[0]</tt>.
@@ -173,9 +173,9 @@ extern "C" {
     /**
        \brief Convert the RCF numeral into a string.
 
-       def_API('Z3_rcf_num_to_string', STRING, (_in(CONTEXT), _in(RCF_NUM), _in(BOOL)))
+       def_API('Z3_rcf_num_to_string', STRING, (_in(CONTEXT), _in(RCF_NUM), _in(BOOL), _in(BOOL)))
     */
-    Z3_string Z3_API Z3_rcf_num_to_string(__in Z3_context c, __in Z3_rcf_num a, __in Z3_bool compact);
+    Z3_string Z3_API Z3_rcf_num_to_string(__in Z3_context c, __in Z3_rcf_num a, __in Z3_bool compact, __in Z3_bool html);
 
     /**
        \brief Convert the RCF numeral into a string in decimal notation.
diff --git a/src/math/interval/interval.h b/src/math/interval/interval.h
index 1fe797861..ed7654f01 100644
--- a/src/math/interval/interval.h
+++ b/src/math/interval/interval.h
@@ -231,6 +231,7 @@ public:
     bool contains(interval const & n, numeral const & v) const;
     
     void display(std::ostream & out, interval const & n) const;
+    void display_pp(std::ostream & out, interval const & n) const;
 
     bool check_invariant(interval const & n) const;
 
diff --git a/src/math/interval/interval_def.h b/src/math/interval/interval_def.h
index 51c1652d7..89d699f1f 100644
--- a/src/math/interval/interval_def.h
+++ b/src/math/interval/interval_def.h
@@ -643,6 +643,15 @@ void interval_manager<C>::display(std::ostream & out, interval const & n) const
     out << (upper_is_open(n) ? ")" : "]");
 }
 
+template<typename C>
+void interval_manager<C>::display_pp(std::ostream & out, interval const & n) const {
+    out << (lower_is_open(n) ? "(" : "[");
+    ::display_pp(out, m(), lower(n), lower_kind(n));
+    out << ", ";
+    ::display_pp(out, m(), upper(n), upper_kind(n));
+    out << (upper_is_open(n) ? ")" : "]");
+}
+
 template<typename C>
 bool interval_manager<C>::check_invariant(interval const & n) const {
     if (::eq(m(), lower(n), lower_kind(n), upper(n), upper_kind(n))) {
diff --git a/src/math/realclosure/realclosure.cpp b/src/math/realclosure/realclosure.cpp
index dac4c8e09..8c6a1d232 100644
--- a/src/math/realclosure/realclosure.cpp
+++ b/src/math/realclosure/realclosure.cpp
@@ -298,26 +298,41 @@ namespace realclosure {
 
     struct transcendental : public extension {
         symbol        m_name;
+        symbol        m_pp_name;
         unsigned      m_k;
         mk_interval & m_proc;
         
-        transcendental(unsigned idx, symbol const & n, mk_interval & p):extension(TRANSCENDENTAL, idx), m_name(n), m_k(0), m_proc(p) {}
+        transcendental(unsigned idx, symbol const & n, symbol const & pp_n, mk_interval & p):
+            extension(TRANSCENDENTAL, idx), m_name(n), m_pp_name(pp_n), m_k(0), m_proc(p) {}
 
-        void display(std::ostream & out) const {
-            out << m_name;
+        void display(std::ostream & out, bool pp = false) const {
+            if (pp) 
+                out << m_pp_name;
+            else
+                out << m_name;
         }
     };
     
     struct infinitesimal : public extension {
         symbol        m_name;
+        symbol        m_pp_name;
  
-        infinitesimal(unsigned idx, symbol const & n):extension(INFINITESIMAL, idx), m_name(n) {}
+        infinitesimal(unsigned idx, symbol const & n, symbol const & pp_n):extension(INFINITESIMAL, idx), m_name(n), m_pp_name(pp_n) {}
 
-        void display(std::ostream & out) const {
-            if (m_name.is_numerical())
-                out << "eps!" << m_name.get_num();
-            else
-                out << m_name;
+        void display(std::ostream & out, bool pp = false) const {
+            if (pp) {
+                if (m_pp_name.is_numerical())
+                    out << "&epsilon;<sub>" << m_pp_name.get_num() << "</sub>";
+                else
+                    out << m_pp_name;
+                
+            }
+            else {
+                if (m_name.is_numerical())
+                    out << "eps!" << m_name.get_num();
+                else
+                    out << m_name;
+            }
         }
     };
 
@@ -1266,9 +1281,9 @@ namespace realclosure {
         /**
            \brief Create a new infinitesimal.
         */
-        void mk_infinitesimal(symbol const & n, numeral & r) {
+        void mk_infinitesimal(symbol const & n, symbol const & pp_n, numeral & r) {
             unsigned idx = next_infinitesimal_idx();
-            infinitesimal * eps = alloc(infinitesimal, idx, n);
+            infinitesimal * eps = alloc(infinitesimal, idx, n, pp_n);
             m_extensions[extension::INFINITESIMAL].push_back(eps);
 
             set_lower(eps->interval(), mpbq(0));
@@ -1280,12 +1295,12 @@ namespace realclosure {
             SASSERT(depends_on_infinitesimals(r));
         }
 
-        void mk_infinitesimal(char const * n, numeral & r) {
-            mk_infinitesimal(symbol(n), r);
+        void mk_infinitesimal(char const * n, char const * pp_n, numeral & r) {
+            mk_infinitesimal(symbol(n), symbol(pp_n), r);
         }
 
         void mk_infinitesimal(numeral & r) {
-            mk_infinitesimal(symbol(next_infinitesimal_idx()), r);
+            mk_infinitesimal(symbol(next_infinitesimal_idx()), symbol(next_infinitesimal_idx()), r);
         }
 
         void refine_transcendental_interval(transcendental * t) {
@@ -1318,9 +1333,9 @@ namespace realclosure {
             }
         }
 
-        void mk_transcendental(symbol const & n, mk_interval & proc, numeral & r) {
+        void mk_transcendental(symbol const & n, symbol const & pp_n, mk_interval & proc, numeral & r) {
             unsigned idx = next_transcendental_idx();
-            transcendental * t = alloc(transcendental, idx, n, proc);
+            transcendental * t = alloc(transcendental, idx, n, pp_n, proc);
             m_extensions[extension::TRANSCENDENTAL].push_back(t);
             
             while (contains_zero(t->interval())) {
@@ -1332,12 +1347,12 @@ namespace realclosure {
             SASSERT(!depends_on_infinitesimals(r));
         }
         
-        void mk_transcendental(char const * p, mk_interval & proc, numeral & r) {
-            mk_transcendental(symbol(p), proc, r);
+        void mk_transcendental(char const * p, char const * pp_n, mk_interval & proc, numeral & r) {
+            mk_transcendental(symbol(p), symbol(pp_n), proc, r);
         }
 
         void mk_transcendental(mk_interval & proc, numeral & r) {
-            mk_transcendental(symbol(next_transcendental_idx()), proc, r);
+            mk_transcendental(symbol(next_transcendental_idx()), symbol(next_transcendental_idx()), proc, r);
         }
 
         void mk_pi(numeral & r) {
@@ -1345,7 +1360,7 @@ namespace realclosure {
                 set(r, m_pi);
             }
             else {
-                mk_transcendental(symbol("pi"), m_mk_pi_interval, r);
+                mk_transcendental(symbol("pi"), symbol("&pi;"), m_mk_pi_interval, r);
                 m_pi = r.m_value;
                 inc_ref(m_pi);
             }
@@ -1356,7 +1371,7 @@ namespace realclosure {
                 set(r, m_e);
             }
             else {
-                mk_transcendental(symbol("e"), m_mk_e_interval, r);
+                mk_transcendental(symbol("e"), symbol("e"), m_mk_e_interval, r);
                 m_e = r.m_value;
                 inc_ref(m_e);
             }
@@ -5762,7 +5777,7 @@ namespace realclosure {
         }
 
         template<typename DisplayVar>
-        void display_polynomial(std::ostream & out, unsigned sz, value * const * p, DisplayVar const & display_var, bool compact) const {
+        void display_polynomial(std::ostream & out, unsigned sz, value * const * p, DisplayVar const & display_var, bool compact, bool pp) const {
             if (sz == 0) {
                 out << "0";
                 return;
@@ -5778,33 +5793,44 @@ namespace realclosure {
                 else
                     out << " + ";
                 if (i == 0)
-                    display(out, p[i], compact);
+                    display(out, p[i], compact, pp);
                 else {
                     if (!is_rational_one(p[i])) {
                         if (use_parenthesis(p[i])) {
                             out << "(";
-                            display(out, p[i], compact);
-                            out << ")*";
+                            display(out, p[i], compact, pp);
+                            out << ")";
+                            if (pp)
+                                out << " ";
+                            else
+                                out << "*";
                         }
                         else {
-                            display(out, p[i], compact);
-                            out << "*";
+                            display(out, p[i], compact, pp);
+                            if (pp)
+                                out << " ";
+                            else
+                                out << "*";
                         }
                     }
-                    display_var(out, compact);
-                    if (i > 1)
-                        out << "^" << i;
+                    display_var(out, compact, pp);
+                    if (i > 1) {
+                        if (pp)
+                            out << "<sup>" << i << "</sup>";
+                        else
+                            out << "^" << i;
+                    }
                 }
             }
         }
 
         template<typename DisplayVar>
-        void display_polynomial(std::ostream & out, polynomial const & p, DisplayVar const & display_var, bool compact) const {
-            display_polynomial(out, p.size(), p.c_ptr(), display_var, compact);
+        void display_polynomial(std::ostream & out, polynomial const & p, DisplayVar const & display_var, bool compact, bool pp) const {
+            display_polynomial(out, p.size(), p.c_ptr(), display_var, compact, pp);
         }
 
         struct display_free_var_proc {
-            void operator()(std::ostream & out, bool compact) const {
+            void operator()(std::ostream & out, bool compact, bool pp) const {
                 out << "x";
             }
         };
@@ -5813,13 +5839,13 @@ namespace realclosure {
             imp const &  m;
             extension *  m_ref;    
             display_ext_proc(imp const & _m, extension * r):m(_m), m_ref(r) {}
-            void operator()(std::ostream & out, bool compact) const {
-                m.display_ext(out, m_ref, compact);
+            void operator()(std::ostream & out, bool compact, bool pp) const {
+                m.display_ext(out, m_ref, compact, pp);
             }
         };
 
-        void display_polynomial_expr(std::ostream & out, polynomial const & p, extension * ext, bool compact) const {
-            display_polynomial(out, p, display_ext_proc(*this, ext), compact);
+        void display_polynomial_expr(std::ostream & out, polynomial const & p, extension * ext, bool compact, bool pp) const {
+            display_polynomial(out, p, display_ext_proc(*this, ext), compact, pp);
         }
 
         static void display_poly_sign(std::ostream & out, int s) {
@@ -5846,7 +5872,7 @@ namespace realclosure {
             out << "}";
         }
 
-        void display_sign_conditions(std::ostream & out, sign_condition * sc, array<polynomial> const & qs, bool compact) const {
+        void display_sign_conditions(std::ostream & out, sign_condition * sc, array<polynomial> const & qs, bool compact, bool pp) const {
             bool first = true;
             out << "{";
             while (sc) {
@@ -5854,21 +5880,28 @@ namespace realclosure {
                     first = false;
                 else
                     out << ", ";
-                display_polynomial(out, qs[sc->qidx()], display_free_var_proc(), compact);
+                display_polynomial(out, qs[sc->qidx()], display_free_var_proc(), compact, pp);
                 display_poly_sign(out, sc->sign());
                 sc = sc->prev();
             }
             out << "}";
         }
 
-        void display_algebraic_def(std::ostream & out, algebraic * a, bool compact) const {
+        void display_interval(std::ostream & out, mpbqi const & i, bool pp) const {
+            if (pp)
+                bqim().display_pp(out, i);
+            else
+                bqim().display(out, i);
+        }
+
+        void display_algebraic_def(std::ostream & out, algebraic * a, bool compact, bool pp) const {
             out << "root(";
-            display_polynomial(out, a->p(), display_free_var_proc(), compact);
+            display_polynomial(out, a->p(), display_free_var_proc(), compact, pp);
             out << ", ";
-            bqim().display(out, a->iso_interval());
+            display_interval(out, a->iso_interval(), pp);
             out << ", ";
             if (a->sdt() != 0) 
-                display_sign_conditions(out, a->sdt()->sc(a->sc_idx()), a->sdt()->qs(), compact);
+                display_sign_conditions(out, a->sdt()->sc(a->sc_idx()), a->sdt()->qs(), compact, pp);
             else
                 out << "{}";
             out << ")";
@@ -5878,28 +5911,33 @@ namespace realclosure {
             collect_algebraic_refs c;
             for (unsigned i = 0; i < n; i++)
                 c.mark(p[i]);
-            display_polynomial(out, n, p, display_free_var_proc(), true);
+            display_polynomial(out, n, p, display_free_var_proc(), true, false);
             std::sort(c.m_found.begin(), c.m_found.end(), rank_lt_proc());
             for (unsigned i = 0; i < c.m_found.size(); i++) {
                 algebraic * ext = c.m_found[i];
                 out << "\n   r!" << ext->idx() << " := ";
-                display_algebraic_def(out, ext, true);
+                display_algebraic_def(out, ext, true, false);
             }
         }
 
-        void display_ext(std::ostream & out, extension * r, bool compact) const {
+        void display_ext(std::ostream & out, extension * r, bool compact, bool pp) const {
             switch (r->knd()) {
-            case extension::TRANSCENDENTAL: to_transcendental(r)->display(out); break;
-            case extension::INFINITESIMAL:  to_infinitesimal(r)->display(out); break;
+            case extension::TRANSCENDENTAL: to_transcendental(r)->display(out, pp); break;
+            case extension::INFINITESIMAL:  to_infinitesimal(r)->display(out, pp); break;
             case extension::ALGEBRAIC: 
-                if (compact)
-                    out << "r!" << r->idx();
-                else
-                    display_algebraic_def(out, to_algebraic(r), compact);
+                if (compact) {
+                    if (pp) 
+                        out << "&alpha;<sub>" << r->idx() << "</sub>";
+                    else
+                        out << "r!" << r->idx();
+                }
+                else {
+                    display_algebraic_def(out, to_algebraic(r), compact, pp);
+                }
             }
         }
 
-        void display(std::ostream & out, value * v, bool compact) const {
+        void display(std::ostream & out, value * v, bool compact, bool pp=false) const {
             if (v == 0)
                 out << "0";
             else if (is_nz_rational(v)) 
@@ -5907,51 +5945,50 @@ namespace realclosure {
             else {
                 rational_function_value * rf = to_rational_function(v);
                 if (is_denominator_one(rf)) {
-                    display_polynomial_expr(out, rf->num(), rf->ext(), compact);
+                    display_polynomial_expr(out, rf->num(), rf->ext(), compact, pp);
                 }
                 else if (is_rational_one(rf->num())) {
                     out << "1/(";
-                    display_polynomial_expr(out, rf->den(), rf->ext(), compact);
+                    display_polynomial_expr(out, rf->den(), rf->ext(), compact, pp);
                     out << ")";
                 }
                 else {
                     out << "(";
-                    display_polynomial_expr(out, rf->num(), rf->ext(), compact);
+                    display_polynomial_expr(out, rf->num(), rf->ext(), compact, pp);
                     out << ")/(";
-                    display_polynomial_expr(out, rf->den(), rf->ext(), compact);
+                    display_polynomial_expr(out, rf->den(), rf->ext(), compact, pp);
                     out << ")";
                 }
             }
         }
 
-        void display_compact(std::ostream & out, value * a) const {
+        void display_compact(std::ostream & out, value * a, bool pp=false) const {
             collect_algebraic_refs c;
             c.mark(a);
             if (c.m_found.empty()) {
-                display(out, a, true);
+                display(out, a, true, pp);
             }
             else {
                 std::sort(c.m_found.begin(), c.m_found.end(), rank_lt_proc());
                 out << "[";
-                display(out, a, true);
+                display(out, a, true, pp);
                 for (unsigned i = 0; i < c.m_found.size(); i++) {
                     algebraic * ext = c.m_found[i];
-                    out << "; r!" << ext->idx() << " := ";
-                    display_algebraic_def(out, ext, true);
+                    if (pp)
+                        out << "; &alpha;<sub>" << ext->idx() << "</sub> := ";
+                    else
+                        out << "; r!" << ext->idx() << " := ";
+                    display_algebraic_def(out, ext, true, pp);
                 }
                 out << "]";
             }
         }
 
-        void display_compact(std::ostream & out, numeral const & a) const {
-            display_compact(out, a.m_value);
-        }
-
-        void display(std::ostream & out, numeral const & a, bool compact=false) const {
+        void display(std::ostream & out, numeral const & a, bool compact=false, bool pp=false) const {
             if (compact)
-                display_compact(out, a);
+                display_compact(out, a.m_value, pp);
             else
-                display(out, a.m_value, false);
+                display(out, a.m_value, false, pp);
         }
 
         void display_non_rational_in_decimal(std::ostream & out, numeral const & a, unsigned precision) {
@@ -5989,7 +6026,7 @@ namespace realclosure {
             if (is_zero(a))
                 out << "[0, 0]";
             else
-                bqim().display(out, interval(a.m_value));
+                display_interval(out, interval(a.m_value), false);
         }
     };
 
@@ -6029,16 +6066,16 @@ namespace realclosure {
         m_imp->del(a);
     }
 
-    void manager::mk_infinitesimal(char const * n, numeral & r) {
-        m_imp->mk_infinitesimal(n, r);
+    void manager::mk_infinitesimal(char const * n, char const * pp_n, numeral & r) {
+        m_imp->mk_infinitesimal(n, pp_n, r);
     }
 
     void manager::mk_infinitesimal(numeral & r) {
         m_imp->mk_infinitesimal(r);
     }
         
-    void manager::mk_transcendental(char const * n, mk_interval & proc, numeral & r) {
-        m_imp->mk_transcendental(n, proc, r);
+    void manager::mk_transcendental(char const * n, char const * pp_n, mk_interval & proc, numeral & r) {
+        m_imp->mk_transcendental(n, pp_n, proc, r);
     }
 
     void manager::mk_transcendental(mk_interval & proc, numeral & r) {
@@ -6212,9 +6249,9 @@ namespace realclosure {
         return gt(a, _b);
     }
 
-    void manager::display(std::ostream & out, numeral const & a, bool compact) const {
+    void manager::display(std::ostream & out, numeral const & a, bool compact, bool pp) const {
         save_interval_ctx ctx(this);
-        m_imp->display(out, a, compact);
+        m_imp->display(out, a, compact, pp);
     }
 
     void manager::display_decimal(std::ostream & out, numeral const & a, unsigned precision) const {
@@ -6234,7 +6271,7 @@ namespace realclosure {
 };
 
 void pp(realclosure::manager::imp * imp, realclosure::polynomial const & p, realclosure::extension * ext) {
-    imp->display_polynomial_expr(std::cout, p, ext, false);
+    imp->display_polynomial_expr(std::cout, p, ext, false, false);
     std::cout << std::endl;
 }
 
@@ -6278,6 +6315,6 @@ void pp(realclosure::manager::imp * imp, mpq const & n) {
 }
 
 void pp(realclosure::manager::imp * imp, realclosure::extension * x) {
-    imp->display_ext(std::cout, x, false);
+    imp->display_ext(std::cout, x, false, false);
     std::cout << std::endl;
 }
diff --git a/src/math/realclosure/realclosure.h b/src/math/realclosure/realclosure.h
index 2b70d3be0..2a1b0dc20 100644
--- a/src/math/realclosure/realclosure.h
+++ b/src/math/realclosure/realclosure.h
@@ -70,7 +70,7 @@ namespace realclosure {
         /**
            \brief Add a new infinitesimal to the current field. The new infinitesimal is smaller than any positive element in the field.
         */
-        void mk_infinitesimal(char const * name, numeral & r);
+        void mk_infinitesimal(char const * name, char const * pp_name, numeral & r);
         void mk_infinitesimal(numeral & r);
         
         /**
@@ -83,7 +83,7 @@ namespace realclosure {
            Then, we extend the field F with 1 - Pi. 1 - Pi is transcendental with respect to algebraic real numbers, but it is NOT transcendental
            with respect to F, since F contains Pi.
         */
-        void mk_transcendental(char const * name, mk_interval & proc, numeral & r);
+        void mk_transcendental(char const * name, char const * pp_name, mk_interval & proc, numeral & r);
         void mk_transcendental(mk_interval & proc, numeral & r);
 
         /**
@@ -252,7 +252,7 @@ namespace realclosure {
         bool ge(numeral const & a, mpq const & b) { return !lt(a, b); }
         bool ge(numeral const & a, mpz const & b) { return !lt(a, b); }
         
-        void display(std::ostream & out, numeral const & a, bool compact=false) const;
+        void display(std::ostream & out, numeral const & a, bool compact=false, bool pp=false) const;
 
         /**
            \brief Display a real number in decimal notation.
diff --git a/src/util/ext_numeral.h b/src/util/ext_numeral.h
index af4b7ac10..83d326243 100644
--- a/src/util/ext_numeral.h
+++ b/src/util/ext_numeral.h
@@ -332,4 +332,16 @@ void display(std::ostream & out,
     }
 }
 
+template<typename numeral_manager>
+void display_pp(std::ostream & out,
+                numeral_manager & m, 
+                typename numeral_manager::numeral const & a,
+                ext_numeral_kind ak) {
+    switch (ak) {
+    case EN_MINUS_INFINITY: out << "-&infin;"; break;
+    case EN_NUMERAL: m.display(out, a); break;
+    case EN_PLUS_INFINITY: out << "+&infin;"; break;
+    }
+}
+
 #endif