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