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