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