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