Structure fracUtils


Source File Identifier index Theory binding index

signature fracUtils =
sig
        type term = Term.term
        type thm = Thm.thm
        type goal = Abbrev.goal
        type conv = Abbrev.conv
        type tactic = Abbrev.tactic

        val dest_frac : term -> term * term list
        val extract_frac : term -> term list
        val extract_abs_frac : term -> term list
        val extract_frac_fun : term list -> term -> (term * term * term) list

        val INT_GT0_CONV : term -> thm
end


Source File Identifier index Theory binding index

HOL 4, Kananaskis-14