1signature fracUtils = 2sig 3 type term = Term.term 4 type thm = Thm.thm 5 type goal = Abbrev.goal 6 type conv = Abbrev.conv 7 type tactic = Abbrev.tactic 8 9 val dest_frac : term -> term * term list 10 val extract_frac : term -> term list 11 val extract_abs_frac : term -> term list 12 val extract_frac_fun : term list -> term -> (term * term * term) list 13 14 val INT_GT0_CONV : term -> thm 15end 16