| Source File | Identifier index | Theory binding index |
|---|
signature ratUtils =
sig
type term = Term.term
type thm = Thm.thm
type goal = Abbrev.goal
type conv = Abbrev.conv
type tactic = Abbrev.tactic
val dest_rat : term -> term * term list
val extract_rat : term -> term list
val extract_rat_vars : term -> term list
val extract_rat_equations : term -> term list
val extract_rat_minv : term -> term list
end
| Source File | Identifier index | Theory binding index |
|---|