1signature fracLib = 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 type simpset = simpLib.simpset 9 10 (* equivalence *) 11 val FRAC_EQ_CONV : conv 12 val FRAC_NOTEQ_CONV : conv 13 val FRAC_EQ_TAC : tactic 14 15 (* positive and non-zero *) 16 val FRAC_POS_CONV : conv 17 val FRAC_NOT0_CONV : conv 18 val FRAC_POS_TAC : term -> tactic 19 val FRAC_NOT0_TAC : term -> tactic 20 21 (* numerator and denominator extraction *) 22 val FRAC_NMR_CONV : conv 23 val FRAC_DNM_CONV : conv 24 val FRAC_NMRDNM_TAC : tactic 25 26 (* calculation *) 27 val FRAC_CALC_CONV : conv 28 val FRAC_STRICT_CALC_TAC : tactic 29 val FRAC_CALCTERM_TAC : term -> tactic 30 val FRAC_CALC_TAC : tactic 31 32 val FRAC_STRICT_CALCEQ_TAC : tactic 33 val FRAC_CALCEQ_TAC : tactic 34 35 val FRAC_SAVE_CONV : conv 36 val FRAC_SAVE_TAC : tactic 37 38end 39