Structure RealArith

signature RealArith =
sig
   type term = Term.term
   type thm = Thm.thm
   type tactic = Abbrev.tactic

  val PURE_REAL_ARITH_TAC : tactic

  val REAL_ARITH_TAC      : tactic
  val REAL_ASM_ARITH_TAC  : tactic

 (* PURE_REAL_ARITH_TAC doesn't throw away assumptions, but requires
    them to be pre-normalised in order to work.  There also must not
    be any non-Presburger terms lurking amongst them.

    REAL_ASM_ARITH_TAC moves all assumptions into the goal, and then
    proceeds.  It thus gets around the two restrictions above.  *)

  val REAL_ARITH          : term -> thm
end

HOL 4, Kananaskis-13