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