1signature DiskFilesHeader =
2sig
3
4type id = {Thy:string,Name:string}
5
6datatype pretype = ptv of string | ptop of int * int list
7datatype pre_vc = ptm_v of string * int | ptm_c of int * int
8datatype preterm = app of preterm * preterm | abs of int * preterm
9                 | atom of int
10type prethm = preterm list * preterm
11type 'a array = (int,'a)Binarymap.dict
12type parse_result =
13     id array * pretype array * pre_vc array * (string * prethm) list
14
15val convert_prethms : parse_result -> (string * HolKernel.thm) list
16
17end
18