src/HOL/TPTP/TPTP_Parser/tptp_syntax.ML
changeset 55987 52c22561996d
parent 55594 eb291b215c73
child 56265 785569927666