1open HolKernel Parse boolLib bossLib; 2 3open emitrecordTheory emitRecordTestML 4 5val _ = new_theory "useEmitRecord"; 6 7val _ = save_thm("T", TRUTH) 8 9 10val _ = export_theory(); 11