1open HolKernel Parse boolLib
2
3val _ = new_theory "base";
4
5val base = store_thm("base", ``x:'a = x``, REWRITE_TAC[]);
6
7
8val _ = export_theory();
9