163212Sabialopen HolKernel Parse boolLib 263212Sabial 363212Sabialopen nextTheory 463212Sabial 563212Sabialval _ = new_theory "last"; 663212Sabial 763212Sabialval _ = save_thm("last", TRUTH) 863212Sabial 963212Sabial 1063212Sabialval _ = export_theory(); 1163212Sabial