1open HolKernel Parse boolLib
2
3open gh179aTheory
4
5val _ = new_theory "gh179b";
6
7val foo_tydef = new_type_definition("foo", tyexists)
8
9
10val _ = export_theory();
11