Structure cv_miscLib

signature cv_miscLib =
sig

  include Abbrev

  val cv_rep_cv_tm : term -> term
  val cv_rep_cv_tm_conv : conv -> conv
  val cv_rep_from : term -> term
  val cv_rep_from_conv : conv -> conv
  val cv_rep_hol_tm : term -> term
  val cv_rep_hol_tm_conv : conv -> conv
  val cv_rep_pre : term -> term
  val cv_rep_pre_conv : conv -> conv
  val mk_cv_rep : term -> term -> term -> term -> term
  val is_cv_rep : term -> bool
  val is_cv_proj : term -> bool
  val dest_cv_proj : term -> term * term
  val cv_size_tm : term
  val mk_cv_size : term -> term

  val contains_fun_ty : hol_type -> bool

  val remove_fupd_conv : conv

end

HOL 4, Trindemossen-1