1open HolKernel Parse boolLib bossLib; 2 3open ATheory 4 5val _ = new_theory "B"; 6 7val bar_def = Define`bar x = foo x * 2`; 8 9 10val _ = export_theory(); 11