1open HolKernel Parse boolLib bossLib
2open arm_progTheory
3
4val () = new_theory "arm_decomp"
5
6val arm_OK_def = Define `arm_OK mode = arm_CONFIG (VFPv3, ARMv7_A, F, F, mode)`
7
8val () = export_theory()
9