1open HolKernel Parse boolLib bossLib; 2open m0_progTheory 3 4val _ = new_theory "m0_decomp"; 5 6val m0_COUNT_def = Define `m0_COUNT count = m0_count count * m0_CONFIG (F, F)` 7 8val _ = export_theory() 9