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