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