1open HolKernel Parse boolLib bossLib;
2
3open comp_delbinding1Theory
4
5val _ = new_theory "comp_delbinding2";
6
7Theorem th = EVAL ���foo 2���
8val _ = rhs (concl th) ~~ lhs (concl th) orelse raise Fail "foo was evaluated!"
9
10val _ = export_theory();
11