1signature iclass_compLib = 2sig 3 include Abbrev 4 5 val BARM_ss : simpLib.ssfrag 6 val ALU_ss : simpLib.ssfrag 7 val Cases_on_arm6inp : term frag list -> tactic 8 val Cases_on_arm6 : term frag list -> tactic 9 val Cases_arm6 : tactic 10 val UNEXEC_ss : simpLib.ssfrag 11 val SWP_ss : simpLib.ssfrag 12 val MRS_MSR_ss : simpLib.ssfrag 13 val DATA_PROC_ss : simpLib.ssfrag 14 val REG_SHIFT_ss : simpLib.ssfrag 15 val LDR_ss : simpLib.ssfrag 16 val STR_ss : simpLib.ssfrag 17 val BR_ss : simpLib.ssfrag 18 val SWI_EX_ss : simpLib.ssfrag 19 val CDP_UND_ss : simpLib.ssfrag 20 val MRC_ss : simpLib.ssfrag 21 val MCR_ss : simpLib.ssfrag 22 val LDC_ss : simpLib.ssfrag 23 val STC_ss : simpLib.ssfrag 24 val LDM_ss : simpLib.ssfrag 25 val STM_ss : simpLib.ssfrag 26 val MLA_MUL_ss : simpLib.ssfrag 27 val UNEXEC_TAC : tactic 28 val SWP_TAC : tactic 29 val MRS_MSR_TAC : tactic 30 val DATA_PROC_TAC : tactic 31 val REG_SHIFT_TAC : tactic 32 val LDR_TAC : tactic 33 val STR_TAC : tactic 34 val BR_TAC : tactic 35 val SWI_EX_TAC : tactic 36 val CDP_UND_TAC : tactic 37 val MRC_TAC : tactic 38 val MCR_TAC : tactic 39 val LDC_TAC : tactic 40 val STC_TAC : tactic 41 val LDM_TAC : tactic 42 val STM_TAC : tactic 43 val MLA_MUL_TAC : tactic 44 val LDM_ITER_CONV : conv 45 val STM_ITER_CONV : conv 46 val MLA_MUL_CONV : conv 47end 48