1open HolKernel Parse boolLib bossLib;
2
3val _ = new_theory "proj1A";
4
5val foo_def = Define`foo x = x * 2 + 1`;
6
7val Athm = Q.store_thm(
8 "Athm",
9 `foo = BIT1`,
10 REWRITE_TAC [FUN_EQ_THM, arithmeticTheory.BIT1] >>
11 simp[foo_def]);
12
13
14
15val _ = export_theory();
16