1open HolKernel Parse boolLib
2
3open thy1Theory
4
5val _ = new_theory "thy2";
6
7val g_def = new_definition("g_def",
8  ``g x y = y /\ f x``);
9
10
11val _ = export_theory();
12