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