1open HolKernel Parse boolLib bossLib; 2 3open proj2ATheory 4val _ = new_theory "proj2B"; 5 6val thm2B = Q.store_thm( 7 "thm2B", 8 ���ODD (bar n) ��� 0 < n���, 9 simp[bar_def] >> Cases_on ���n��� >> simp[] >> 10 simp[arithmeticTheory.MULT_CLAUSES, arithmeticTheory.ODD_ADD, 11 arithmeticTheory.ODD_MULT]); 12 13val _ = export_theory(); 14