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