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