Structure Gen_arith

Source File	Identifier index	Theory binding index

signature Gen_arith =
sig

   val non_presburger_subterms : Term.term -> Term.term list
   val is_presburger : Term.term -> bool
   val ARITH_CONV : Abbrev.conv
end

Source File	Identifier index	Theory binding index

HOL 4, Trindemossen-1