src/HOL/TPTP/TPTP_Parser/tptp_syntax.ML
changeset 64716 473793d52d97
parent 64560 c48becd96398
child 69593 3dda49e08b9d