Structure countable_typesLib


Source File Identifier index Theory binding index

signature countable_typesLib =
sig
  include Abbrev

  val mk_countable : hol_type -> thm

end


Source File Identifier index Theory binding index

HOL 4, Trindemossen-1