1open HolKernel Parse boolLib ; 2 3open dir2Theory 4 5val _ = new_theory "ultimate"; 6 7val ultimate = save_thm("ultimate", TRUTH) 8 9 10val _ = export_theory(); 11