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