1signature intExtensionLib = 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 (* tactics *) 11 val INT_SGN_CASES_TAC: term -> tactic 12 val INT_CALCEQ_TAC: tactic 13end 14