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