1open HolKernel boolSyntax Opentheory 2val Thy = "OpenTheoryFunction" 3val pkg = "function-1.55" 4val _ = new_theory Thy 5val file = pkg^".art" 6 7val ERR=mk_HOL_ERR Thy 8 9val _ = new_constant("dummy",alpha) 10val _ = OpenTheoryMap.OpenTheory_const_name{const={Thy=Thy,Name="dummy"},name=([],pkg)} 11 12val (reader:reader) = { 13 const_name = const_name_in_map, 14 tyop_name = tyop_name_in_map, 15 define_tyop = define_tyop_in_thy, 16 define_const = fn {Name,Thy} => fn tm => mk_thm([],(mk_eq(mk_thy_const {Name=Name,Thy=Thy,Ty=type_of tm},tm))), 17 axiom = K mk_thm 18}; 19val thms = read_article file reader; 20val _ = Net.itnet (fn th => fn n => (save_thm("th"^Int.toString(n),th); n+1)) thms 0; 21 22val _ = export_theory() 23