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