src/HOL/TPTP/TPTP_Parser/tptp_syntax.ML
changeset 65007 b6a1a1d42f5d
parent 64560 c48becd96398
child 69593 3dda49e08b9d