1open HolKernel Parse boolLib bossLib; 2 3val _ = new_theory "dupop20171208a"; 4 5val _ = Datatype `testtype = <| fld1 : 'a ; fld2 : num -> bool |>`; 6 7 8val _ = export_theory(); 9