1signature ratLib = 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 ssfrag = simpLib.ssfrag 9 type simpset = simpLib.simpset 10 11 (* conversions *) 12 val RAT_EQ_CONV : conv 13 val RAT_CALC_CONV : conv 14 val RAT_ADDAC_CONV :conv 15 val RAT_MULAC_CONV :conv 16 17 (* tactics *) 18 val RAT_EQ_TAC : tactic 19 val RAT_ADDAC_TAC : term -> tactic 20 val RAT_MULAC_TAC : term -> tactic 21 val RAT_EQ_LMUL_TAC : term -> tactic 22 val RAT_EQ_RMUL_TAC : term -> tactic 23 val RAT_ADDSUB_TAC : term -> term -> tactic 24 val RAT_CALCTERM_TAC : term -> tactic 25 val RAT_STRICT_CALC_TAC : tactic 26 val RAT_CALC_TAC : tactic 27 val RAT_CALCEQ_TAC : tactic 28 29 (* conversions *) 30 val RAT_PRECALC_CONV : conv 31 val RAT_POSTCALC_CONV : conv 32 val RAT_BASIC_ARITH_CONV : conv 33 val RAT_ELIMINATE_MINV_EQ_CONV : conv 34 val RAT_ELIMINATE_MINV_CONV : conv 35 36 (* tactics *) 37 val RAT_SAVE_TAC : term -> tactic 38 val RAT_SAVE_ALLVARS_TAC : tactic 39 val RAT_BASIC_ARITH_TAC : tactic 40 val RAT_ELIMINATE_MINV_TAC : tactic 41 42 val int_rewrites : thm list 43 val rat_basic_rewrites : thm list 44 val rat_rewrites : thm list 45 val rat_num_rewrites : thm list 46 47end 48