| 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 |
|---|