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