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