1open HolKernel Parse boolLib bossLib;
2
3open proj1BTheory
4val _ = new_theory "proj2A";
5
6val bar_def = Define���bar x = 2 * x - 1���;
7
8val thm2A = Q.store_thm(
9 "thm2A",
10 ������n. 0 < n ��� (bar n = foo n - 2)���,
11 simp[bar_def, proj1ATheory.foo_def]);
12
13val _ = export_theory();
14