src/HOL/TPTP/TPTP_Parser/tptp_syntax.ML
changeset 67872 39b27d38a54c
parent 64560 c48becd96398
child 69593 3dda49e08b9d