1signature armLib =
2sig
3    include Abbrev
4
5    val fcp_ss       : simpLib.simpset
6    val ICLASS_ss    : simpLib.ssfrag
7    val PBETA_ss     : simpLib.ssfrag
8
9    val combCases    : conv
10    val tupleCases   : conv
11
12    val RES_MP1_TAC  : (term frag list, term frag list) subst -> thm -> tactic
13    val RES_MP_TAC   : (term frag list, term frag list) subst -> thm -> tactic
14
15    val UNABBREV_RULE : term frag list -> rule
16end
17