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