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