1290001Sglebiusopen HolKernel Parse boolLib 2290001Sglebius 3290001Sglebiusopen gh225aTheory 4290001Sglebius 5290001Sglebiusval _ = new_theory "gh225b"; 6290001Sglebius 7290001Sglebiusval _ = save_thm("TRUTH", TRUTH); 8290001Sglebius 9290001Sglebiusval _ = export_theory(); 10290001Sglebius