1open HolKernel Parse boolLib bossLib;
2
3open dupop20171208aTheory
4
5val _ = new_theory "dupop20171208b";
6
7val _ = Datatype `testtype = <| fld0 : num ; fld1 : 'c ; fld3 : 'dd -> bool ;
8 fld4 : num ; fld5 : num -> num ; fld6 : num -> bool |>`;
9
10val _ = export_theory();
11