src/HOL/TPTP/TPTP_Parser/tptp_syntax.ML
changeset 54715 a13aa1cac0e8
parent 53394 f26f00cbd573
child 55587 5d3db2c626e3