1open HolKernel Parse boolLib
2
3open derivedTheory
4
5val _ = new_theory "final";
6
7val baz_def = new_definition("baz_def", ���baz x <=> (foo x ==> bar x)���);
8
9
10val _ = export_theory();
11