1open HolKernel Parse boolLib
2
3open github130Lib
4val _ = new_theory "github130a";
5
6val foo_def = new_definition("foo_def", ``foo f x = f x``)
7val _ = export_gh130 "foo_def"
8val _ = Feedback.WARNINGs_as_ERRs := false
9val _ = delete_const "foo"
10
11
12val _ = export_theory();
13