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