Structure PairedLambda


Source File Identifier index Theory binding index

signature PairedLambda =
sig
  include Abbrev

  val PAIRED_BETA_CONV : conv
  val PAIRED_ETA_CONV  : conv
  val GEN_BETA_CONV    : conv
  val let_CONV         : conv
  val GEN_LET_CONV     : conv
  val LET_SIMP_CONV    : bool -> conv

  val GEN_BETA_RULE    : thm -> thm
  val GEN_BETA_TAC     : tactic
end


Source File Identifier index Theory binding index

HOL 4, Kananaskis-14