src/HOL/TPTP/TPTP_Parser/tptp_syntax.ML
changeset 47514 0a870584145f
parent 47454 479b4d6b9562
child 47569 fce9d97a3258