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