1open HolKernel boolLib Parse
2
3open fooTheory
4
5val _ = new_theory "bar"
6
7val f_def = new_definition(
8  "f_def",
9  ``f x = x + 1``);
10
11val _ = export_theory()
12