1signature TexTokenMap = 2sig 3 4 val TeX_notation : {hol: string, TeX : string * int} -> unit 5 val temp_TeX_notation : {hol: string, TeX : string * int} -> unit 6 7 val the_map : unit -> (string,string * int)Binarymap.dict 8 9end 10