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