MP_CONV : conv -> thm -> thm
# let th = MESON[LE_REFL] `(!e. &0 < e / &2 <=> &0 < e) /\ (!a x y e. abs(x - a) < e / &2 /\ abs(y - a) < e / &2 ==> abs(x - y) < e) ==> (!e. &0 < e ==> ?n. !m. n <= m ==> abs(x m - a) < e) ==> (!e. &0 < e ==> ?n. !m. n <= m ==> abs(x m - x n) < e)`;;
# MP_CONV REAL_ARITH th;; val it : thm = |- (!e. &0 < e ==> (?n. !m. n <= m ==> abs (x m - a) < e)) ==> (!e. &0 < e ==> (?n. !m. n <= m ==> abs (x m - x n) < e))