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