1signature arm_rulesLib =
2sig
3    include Abbrev
4
5    val SORT_REG_WRITEL_CONV : conv
6    val REG_READ_WRITEL_CONV : conv
7    val REG_WRITEL_CONV      : conv
8    val PSR_CONV             : conv
9
10    val arm_rules     : (string * thm) list
11
12    val RULE_GET      : term -> thm list -> thm list
13    val RULE_GET_ARM  : term -> thm
14
15    val GET_ARM       : string -> thm
16end
17