Structure fcpLib

Source File	Identifier index	Theory binding index

signature fcpLib =
sig
    include Abbrev

    val index_type    : Arbnum.num -> hol_type
    val index_to_num  : hol_type -> Arbnum.num

    val INDEX_CONV    : conv
    val DIMINDEX      : Arbnum.num -> thm
    val FINITE        : Arbnum.num -> thm
    val SIZE          : Arbnum.num -> thm
    val FCP_ss        : simpLib.ssfrag

    val inst_fcp_lengths : term -> term
end

Source File	Identifier index	Theory binding index

HOL 4, Kananaskis-13