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