Structure Cooper


Source File Identifier index Theory binding index

signature Cooper =
sig
  include Abbrev

  val pure_goal                   : conv
  val COOPER_CONV                 : conv
  val COOPER_PROVE                : conv
  val COOPER_TAC                  : tactic
  val is_presburger               : term -> bool
  val non_presburger_subterms     : term -> term list
  val decide_pure_presburger_term : term -> thm
end


Source File Identifier index Theory binding index

HOL 4, Trindemossen-1