Structure cv_repLib

Source File	Identifier index	Theory binding index

signature cv_repLib =
sig
  include Abbrev

  val cv_rep_for         : (term * thm) list -> term -> thm

  exception NeedsTranslation of term list * term;

end

Source File	Identifier index	Theory binding index

HOL 4, Trindemossen-1