Structure CooperThms


Source File Identifier index Theory binding index

signature CooperThms = sig

  include Abbrev
  val elim_le : thm
  val elim_gt : thm
  val elim_ge : thm
  val move_add : thm

  val T_and_l : thm
  val T_and_r : thm
  val F_and_l : thm
  val F_and_r : thm
  val T_or_l : thm
  val T_or_r : thm
  val F_or_l : thm
  val F_or_r : thm

  val NOT_NOT_P : thm
  val NOT_OR : thm
  val NOT_AND : thm

  val NOT_AND_IMP : thm

  val DISJ_NEQ_ELIM : thm
  val cpEU_THM : thm

  val simple_disj_congruence : thm
  val simple_conj_congruence : thm

end


Source File Identifier index Theory binding index

HOL 4, Kananaskis-14