1open HolKernel Parse boolLib
2
3val _ = new_theory "github234a";
4
5val _ = Globals.max_print_depth := 5;
6val _ = overload_on("foo",``\t1 t2. !t. (t1 ==> t2 ==> t) ==> t``);
7
8val _ = export_theory();
9