1open HolKernel boolLib bossLib OpenTheoryMap OpenTheoryFunctionTheory 2 3val Thy = "HOL4combin" 4val _ = new_theory Thy 5 6val n = ref 0; 7fun export (tm,tac) = 8 store_thm(("th"^Int.toString(!n)),tm,tac) 9 before n := !n+1 10 11val res0 = export(``I = S K (K:'a->'a->'a)``, 12 PURE_REWRITE_TAC[th18] >> REFL_TAC) 13 (* DB.match["OpenTheoryFunction"]``I`` *) 14val res1 = export(``$o f g = \x. f ( g x)``, 15 PURE_REWRITE_TAC[th22] >> 16 CONV_TAC (DEPTH_CONV BETA_CONV) >> 17 REFL_TAC) 18 (* DB.match["OpenTheoryFunction"]``$o`` *) 19 20val _ = export_theory() 21