1structure type_grammar_dtype = 2struct 3 4datatype grammar_rule = 5 INFIX of {opname : string, parse_string : string} list * 6 HOLgrammars.associativity 7 8datatype type_structure = 9 TYOP of {Thy : string, Tyop : string, Args : type_structure list} 10 | PARAM of int 11 12datatype delta = 13 NEW_TYPE of KernelSig.kernelname 14 | NEW_INFIX of {Name : string, ParseName : string, 15 Assoc : HOLgrammars.associativity, Prec : int} 16 | TYABBREV of KernelSig.kernelname * Type.hol_type * bool 17 | DISABLE_TYPRINT of string 18 | RM_KNM_TYABBREV of KernelSig.kernelname 19 | RM_TYABBREV of string 20 21end 22