src/HOL/TPTP/TPTP_Parser/tptp_syntax.ML
changeset 57070 6a8a01e6dcdf
parent 56467 8d7d6f17c6a7
child 57808 cf72aed038c8