CONV_TAC : conv -> tactic
A ?- g =============== CONV_TAC c A ?- g'
# g `abs(pi - &22 / &7) <= abs(&355 / &113 - &22 / &7)`;;
# e(CONV_TAC REAL_RAT_REDUCE_CONV);; val it : goalstack = 1 subgoal (1 total) `abs (pi - &22 / &7) <= &1 / &791`
# g `!x:real. &0 < x ==> &1 / x - &1 / (x + &1) = &1 / (x * (x + &1))`;;
# e(CONV_TAC REAL_FIELD);; ... val it : goalstack = No subgoals