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