1structure github130Lib = 2struct 3 4open HolKernel 5val _ = Feedback.WARNINGs_as_ERRs := true; 6val _ = Globals.print_thy_loads := true; 7 8val ghdata = ref [] : thm list ref 9fun add_ghdata (_, th) = (ghdata := th :: !ghdata) 10 11val {export = export_gh130, dest, mk} = ThmSetData.new_exporter "gh130" (K (List.app add_ghdata)) 12 13end 14