1open HolKernel Parse boolLib bossLib; 2 3open proj1ATheory 4 5val _ = new_theory "pp"; 6 7val _ = overload_on ("quux", ``foo``) 8 9 10val _ = export_theory(); 11