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