1signature Gen_arith = 2sig 3 4 val non_presburger_subterms : Term.term -> Term.term list 5 val is_presburger : Term.term -> bool 6 val ARITH_CONV : Abbrev.conv 7end 8