1open HolKernel Parse boolLib 2 3val _ = new_theory "mid"; 4 5val base1_theorem = save_thm("mid_theorem", 6 CONJUNCT1 base1Theory.base1_theorem); 7 8val _ = export_theory(); 9