src/HOL/TPTP/TPTP_Parser/tptp_syntax.ML
changeset 55411 27de2c976d90
parent 53394 f26f00cbd573
child 55587 5d3db2c626e3