1open HolKernel Parse boolLib 2 3val _ = new_theory "base2"; 4 5val base1_theorem = save_thm("base2_theorem", 6 SPEC ���q:bool��� AND_CLAUSES); 7 8val _ = export_theory(); 9