src/HOL/TPTP/TPTP_Parser/tptp_syntax.ML
changeset 56812 baef1c110f12
parent 56467 8d7d6f17c6a7
child 57808 cf72aed038c8