1open HolKernel Parse boolLib
2
3val _ = new_theory "final";
4
5val final_theorem = save_thm("final_theorem",
6  CONJ base2Theory.base2_theorem midTheory.mid_theorem);
7
8val _ = export_theory();
9