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