Structure minisatProve

Source File	Identifier index	Theory binding index


signature minisatProve = sig
  exception SAT_cex of Thm.thm
  val GEN_SAT : satConfig.sat_config -> Thm.thm
  val SAT_PROVE : Term.term -> Thm.thm
  val SAT_ORACLE : Term.term -> Thm.thm
  val ZSAT_PROVE : Term.term -> Thm.thm
  val ZSAT_ORACLE : Term.term -> Thm.thm
end

Source File	Identifier index	Theory binding index

HOL 4, Kananaskis-13