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