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