1structure HolKernel =
2struct
3  open HolKernel Logging
4  fun new_theory s = let
5    val _ = HolKernel.new_theory s
6    val _ = start_logging()
7    fun th {Thy,Tyop} = (["HOL4",Thy],Tyop)
8    fun ch {Thy,Name} = (["HOL4",Thy],Name)
9    val _ = set_tyop_name_handler th
10    val _ = set_const_name_handler ch
11  in () end
12  val donotdefines = ["K","I","S","W","C"]
13  structure Q =
14  struct
15    open Q
16    fun new_definition (a as (name,q)) =
17      if List.exists (equal name)
18          (List.map (fn d => d^"_DEF") donotdefines)
19      then
20        let
21          val tm = rand(Parse.Term q)
22          val c = (String.extract(name,0,SOME 1),type_of tm)
23          val () = new_constant c
24          val th = mk_thm([],boolSyntax.mk_eq(mk_const c,tm))
25        in
26          save_thm(name,th)
27        end
28      else Q.new_definition a
29    (* for o_DEF *)
30    fun new_infixr_definition (name,q,prec) =
31      let
32        val _ = Parse.add_infix("o",prec,Parse.RIGHT)
33        val eq = Parse.Term q
34        val ty = eq |> boolSyntax.lhs
35                 |> boolSyntax.strip_comb |> #1 |> type_of
36        val c = ("o",ty)
37        val () = new_constant c
38        val th = Q.GENL[`g`,`f`](mk_thm([],Parse.Term q))
39      in
40        save_thm(name,th)
41      end
42  end
43  fun export_theory() = let open Lib Theory
44    val _ = map (export_thm o snd) (current_theorems())
45    val _ = map (export_thm o snd) (current_definitions())
46    val _ = map (export_thm o snd) (current_axioms())
47    val _ = stop_logging()
48  in () end
49end
50