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