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