1open HolKernel Parse boolLib bossLib;
2
3open proj1ATheory
4
5val _ = new_theory "proj1B";
6
7val Bthm = Q.store_thm(
8  "Bthm",
9  ���SUC o foo = BIT2���,
10  REWRITE_TAC[FUN_EQ_THM, combinTheory.o_THM, arithmeticTheory.BIT2] >>
11  simp[foo_def]);
12
13val _ = export_theory();
14