1open HolKernel Parse boolLib 2 3val _ = new_theory "base"; 4 5val base = store_thm("base", ``x:'a = x``, REWRITE_TAC[]); 6 7 8val _ = export_theory(); 9