1open HolKernel Parse boolLib 2 3open baseLib 4 5val _ = new_theory "next"; 6 7val _ = save_thm("B" ^ Int.toString (do_base_thing 3), TRUTH); 8 9val _ = export_theory(); 10